Anonymous | Login | Signup for a new account | 2019-02-21 12:00 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 | ||||
0002297 | Frama-C | Kernel | public | 2017-05-08 16:16 | 2017-12-06 09:10 | ||||
Reporter | Jochen | ||||||||
Assigned To | maroneze | ||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Platform | Phosphorus-20170501-beta1 | OS | xubuntu 16.04.1 | OS Version | |||||
Product Version | |||||||||
Target Version | Fixed in Version | Frama-C 16-Sulfur | |||||||
Summary | 0002297: syntax error before loop contract reported after loop contract | ||||||||
Description | Running "frama-c -wp synt.c" gives the output: [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing synt.c (with preprocessing) [kernel] syntax error at synt.c:7: 5 loop assigns i,s; 6 loop variant 9-i; 7 */ ^^^ 8 for (int i=0; i<9; ++i) 9 s += 2; [kernel] Frama-C aborted: invalid user input. This suggests that there is some syntax error within the loop contract (and it often takes a long time to check the contract byte by byte for correctness). However, the error is the missing semi-colon in line 3, immediately before the contract. | ||||||||
Tags | No tags attached. | ||||||||
Attached Files | ![]() | ||||||||
![]() |
|
(0006396) maroneze (developer) 2017-05-23 13:34 |
Thanks for the report. A patch has been devised that provides better error messages in this case, and in some other cases as well. However, this patch won't be available in Frama-C 15 (Phosphorus), only in Frama-C 16 (Sulfur). Here's what the new error message looks like: [kernel] syntax error at synt.c, between lines 3 and 7 1 2 int sum(void) { 3 int s = 0 4 /*@ 5 loop assigns i,s; 6 loop variant 9-i; 7 */ 8 for (int i=0; i<9; ++i) 9 s += 2; |
![]() |
|||
Date Modified | Username | Field | Change |
2017-05-08 16:16 | Jochen | New Issue | |
2017-05-08 16:16 | Jochen | File Added: synt.c | |
2017-05-09 10:21 | yakobowski | Assigned To | => maroneze |
2017-05-09 10:21 | yakobowski | Status | new => assigned |
2017-05-23 13:34 | maroneze | Note Added: 0006396 | |
2017-05-23 13:36 | maroneze | Status | assigned => resolved |
2017-05-23 13:36 | maroneze | Fixed in Version | => Frama-C GIT, precise the release id |
2017-05-23 13:36 | maroneze | Resolution | open => fixed |
2017-05-31 19:04 | signoles | Fixed in Version | Frama-C GIT, precise the release id => |
2017-05-31 19:04 | signoles | Fixed in Version | => Frama-C 15-Phosphorus |
2017-05-31 19:05 | signoles | Status | resolved => closed |
2017-05-31 19:19 | maroneze | Status | closed => resolved |
2017-05-31 19:19 | maroneze | Fixed in Version | Frama-C 15-Phosphorus => Frama-C 16-Sulfur |
2017-12-06 09:10 | signoles | Status | resolved => closed |
Copyright © 2000 - 2019 MantisBT Team |