| Anonymous | Login | Signup for a new account | 2019-02-17 03:49 CET |  |
| Main | My View | View Issues | Change Log | Roadmap | Repositories |
| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
| 0002131 | Frama-C | Kernel | public | 2015-06-04 21:04 | 2016-01-26 13:38 | ||||
| Reporter | Ian | ||||||||
| Assigned To | yakobowski | ||||||||
| Priority | normal | Severity | minor | Reproducibility | always | ||||
| Status | closed | Resolution | fixed | ||||||
| Platform | OS | Ubuntu | OS Version | ||||||
| Product Version | Frama-C Sodium | ||||||||
| Target Version | Fixed in Version | Frama-C Magnesium | |||||||
| Summary | 0002131: Error with casted ternary statements | ||||||||
| Description | 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 "<built-in>" # 1 "<command-line>" # 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; } | ||||||||
| Steps To Reproduce | 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. | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files | |||||||||
 Relationships |
||||||
|
||||||
 Relationships |
|
Notes |
|
|
(0005933) yakobowski (manager) 2015-06-08 13:12 |
This problem has been solved at the same time as bug 0002117. 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 (reporter) 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<gz_insize ? gz_inbuf[gz_inptr++] : FS_gz_fill_inbuf() ); |
|
(0005935) yakobowski (manager) 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. |
|
Notes |
|
Issue History |
|||
| Date Modified | Username | Field | Change |
| 2015-06-04 21:04 | Ian | New Issue | |
| 2015-06-05 08:49 | signoles | Assigned To | => virgile |
| 2015-06-05 08:49 | signoles | Status | new => assigned |
| 2015-06-05 16:13 | yakobowski | Assigned To | virgile => yakobowski |
| 2015-06-05 16:15 | yakobowski | Relationship added | related to 0002117 |
| 2015-06-08 13:12 | yakobowski | Note Added: 0005933 | |
| 2015-06-08 18:56 | Ian | Note Added: 0005934 | |
| 2015-06-08 21:21 | yakobowski | Note Added: 0005935 | |
| 2015-06-08 21:21 | yakobowski | Status | assigned => resolved |
| 2015-06-08 21:21 | yakobowski | Resolution | open => fixed |
| 2016-01-26 08:51 | signoles | Fixed in Version | => Frama-C Magnesium |
| 2016-01-26 08:52 | signoles | Status | resolved => closed |
|
Issue History |
| Copyright © 2000 - 2019 MantisBT Team |
|