View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0001162 | Frama-C | Kernel > ACSL implementation | public | 2012-04-16 18:26 | 2012-09-19 17:16 | ||||
Reporter | nmuller | ||||||||
Assigned To | virgile | ||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C Nitrogen-20111001 | ||||||||
Target Version | Fixed in Version | Frama-C Oxygen-20120901 | |||||||
Summary | 0001162: "for" clause is refused | ||||||||
Description | The following annotation is refused : ensures \result == {s for a = (int)4 }; in the file StructTestPos.c | ||||||||
Additional Information | [kernel] preprocessing with "gcc -C -E -I. -dD StructTestPos.c" StructTestPos.c:38:[kernel] user error: unexpected token 'for' [kernel] user error: skipping file "StructTestPos.c" that has errors. [kernel] Frama-C aborted because of invalid user input. | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
virgile (developer) 2012-04-17 17:41 |
Correct syntax for functional update is { s \with .a = 4 } (see ACSL manual at http://frama-c.com/download/acsl_1.5.pdf). It is supported by Frama-C's kernel in Nitrogen (although the implementation manual does not reflect it). Not all plug-ins have support for it, though. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2012-04-16 18:26 | nmuller | New Issue | |
2012-04-16 18:26 | nmuller | Status | new => assigned |
2012-04-16 18:26 | nmuller | Assigned To | => virgile |
2012-04-16 18:26 | nmuller | File Added: StructTestPos.c | |
2012-04-17 17:41 | virgile | Note Added: 0002932 | |
2012-04-17 17:41 | virgile | Status | assigned => resolved |
2012-04-17 17:41 | virgile | Fixed in Version | => Frama-C Nitrogen-20111001 |
2012-04-17 17:41 | virgile | Resolution | open => fixed |
2012-09-19 17:15 | signoles | Fixed in Version | Frama-C Nitrogen-20111001 => Frama-C Oxygen-20120901 |
2012-09-19 17:16 | signoles | Status | resolved => closed |