Frama-C Bug Tracking System - Frama-C
View Issue Details
0002131Frama-CKernelpublic2015-06-04 21:042016-01-26 13:38
Ian 
yakobowski 
normalminoralways
closedfixed 
Ubuntu
Frama-C Sodium 
Frama-C Magnesium 
0002131: Error with casted ternary statements
The following is a simplified version from an situation where macros created a statement (which had side effects, unlike this example). 1 void main() { 2 int p=0, i=0, j=0; 3 // (char)( p ? i : j ); // [kernel] user error: cannot cast from void to char 4 ( p ? i : j ); 5 } When line three is uncommented, frama-c fails with the error noted. Inspecting the normalized version reveals a potential problem (line 3 is commented out). > frama-c void_cast.c -then -print [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing void_cast.c (with preprocessing) /* Generated by Frama-C */ void main(void) { int p; int i; int j; p = 0; i = 0; j = 0; if (p) { if (i) ; } else if (j) ; return; } As seen above, line 4 is normalized to if (p) { if (i) ; } else if (j) ; Which has two potential problems. First, it is unclear why ‘i' and ‘j’ are wrapped in conditionals. Second, this structure may result in the ‘if’ statement being casted, instead of ‘i' or ‘j’, ultimately producing the observed error. Running just the gcc preprocessor on the initial source file does not cause these transformations. > gcc -E void_cast.c # 1 "void_cast.c" # 1 "" # 1 "" # 1 "void_cast.c" void main() { int p=0, i=0, j=0; (char)( p ? i : j ); ( p ? i : j ); } Interestingly, adding an assignment produces a reasonable transformation. The program: void main() { int p=0, i=0, j=0; char c = (char)( p ? i : j ); } Is normalized to: void main(void) { int p; int i; int j; char c; int tmp; p = 0; i = 0; j = 0; if (p) tmp = i; else tmp = j; c = (char)tmp; return; }
Create file void_cast.c: void main() { int p=0, i=0, j=0; (char)( p ? i : j ); } Run frama-c: > frama-c void_cast.c [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing void_cast.c (with preprocessing) void_cast.c:3:[kernel] user error: cannot cast from void to char [kernel] user error: stopping on file "void_cast.c" that has errors. Add '-kernel-msg-key pp' for preprocessing command. [kernel] Frama-C aborted: invalid user input. But expected frama-c to succeed since the program is accepted by gcc.
No tags attached.
related to 0002117closed yakobowski frama-c gets confused by comma operator inside ternary operator: cannot cast from void to char 
Issue History
2015-06-04 21:04IanNew Issue
2015-06-05 08:49signolesAssigned To => virgile
2015-06-05 08:49signolesStatusnew => assigned
2015-06-05 16:13yakobowskiAssigned Tovirgile => yakobowski
2015-06-05 16:15yakobowskiRelationship addedrelated to 0002117
2015-06-08 13:12yakobowskiNote Added: 0005933
2015-06-08 18:56IanNote Added: 0005934
2015-06-08 21:21yakobowskiNote Added: 0005935
2015-06-08 21:21yakobowskiStatusassigned => resolved
2015-06-08 21:21yakobowskiResolutionopen => fixed
2016-01-26 08:51signolesFixed in Version => Frama-C Magnesium
2016-01-26 08:52signolesStatusresolved => closed

Notes
(0005933)
yakobowski   
2015-06-08 13:12   
This problem has been solved at the same time as bug #2117. The fix will be part of the next open source release of Frama-C. Can you also upload the original code (with the side effects), so that we may check that our fix is good? Regarding the additional 'ifs': Frama-C preserves side effects that may cause undefined behavior (such as '1/x;') using a conditional with no 'then' or 'else' branch. This is why the two 'if(i)' and 'if(j)' are added. We use this construct because no other kind of statement is available to represent 'i;' or '1/x;'.
(0005934)
Ian   
2015-06-08 18:56   
The original code comes from the NASA Core Flight Executive framework 6.4.0, available at http://sourceforge.net/projects/coreflightexec/ The file cfe_fs_decompress.c uses the macro NEXTBYTE() as a statement which expands to (uint8)( gz_inptr
(0005935)
yakobowski   
2015-06-08 21:21   
I can confirm that the code the next version of Frama-C generates will be correct for this code pattern. An intermediate variable is introduce to represent gz_inbuf[gz_inptr++] or FS_gz_fill_inbuf() (typed as their smallest supertype). Then this variable is cast to uint8.