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

Also available in: Atom PDF