Project

General

Profile

Actions
Copy link

Bug #10192

closed

Frama-C (CIL) issues invalid error "lvalue of type void: tmp"

Added by Evgeny Novikov about 4 years ago. Updated about 4 years ago.

Status:
Closed
Priority:
Urgent
Assignee:
Mikhail Mandrykin
Start date:
03/31/2020
Due date:
% Done:

0%

Estimated time:
Detected in build:
git
Platform:
Published in build:

Description

For the attached source file Frama-C (CIL) fails while GCC seems to eat it (there are errors but they are different). Command-line options are as follows:

toplevel.opt "-no-autoload-plugins" "-no-findlib" "-kernel-log" "e:problem desc.txt" "-machdep" "gcc_x86_64" "-c11" "-kernel-warn-key" "CERT:MSC:38=active" "-remove-unused-inline-functions" "-remove-unused-static-functions" "-no-annot" "-no-single-return" "-fold-temp-vars" "-shrink-initializers" "-keep-logical-operators" "-aggressive-merging" "-print" "-print-lines" "-no-print-annot" "-ocode" "cil.i"

Due to this issue 23 tasks from 56 fail. These tasks correspond to different USB Serial drivers from Linux 4.9-11.

Files

Download all files
ftdi_sio.c (4.03 MB) ftdi_sio.c Evgeny Novikov, 03/31/2020 09:19 PM
toplevel.tar.xz (3.3 MB) toplevel.tar.xz Frama-C 18.0 with this patch compiled for glibc 2.24 under Debian 9 Mikhail Mandrykin, 04/01/2020 10:48 PM
Actions
Copy link
 #1

Updated by Mikhail Mandrykin about 4 years ago

Fixed in framac|88b363dd, was caused by a too strict criterion for keeping the result (here void) of a GNU body construct ({...; e}).

Actions
Copy link
 #2

Updated by Mikhail Mandrykin about 4 years ago

  • Status changed from New to Resolved
Actions
Copy link
 #4

Updated by Evgeny Novikov about 4 years ago

  • Status changed from Resolved to Closed

I checked that the issue was fixed and that the attached binary works well even on Debian 9.

Actions
Copy link

Also available in: Atom PDF