View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|
0001154 | Frama-C | Plug-in > jessie | public | 2012-04-16 11:28 | 2012-04-17 17:31 | ||||||||
Reporter | nmuller | ||||||||||||
Assigned To | cmarche | ||||||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||||||
Status | assigned | Resolution | open | ||||||||||
Product Version | Frama-C GIT, precise the release id | ||||||||||||
Target Version | Fixed in Version | ||||||||||||
Summary | 0001154: erroneous left value (structure field) | ||||||||||||
Description | access to a structure field in a lemna does not seem to work typedef struct { int i; } T; /*@ lemma toto{L}: @ \forall T t; t.i == 0; @*/ | ||||||||||||
Additional Information | frama-c -jessie -jessie-atp alt-ergo unused.c [kernel] preprocessing with "gcc -C -E -I. -dD unused.c" [jessie] Starting Jessie translation unused.c:4:[jessie] failure: cannot handle this lvalue [jessie] warning: Unsupported feature(s). Jessie plugin can not be used on your code. rem : as soon as t is actually declared (of type T) prior to the lemna and an explicit access to t.i is done, this works | ||||||||||||
Tags | No tags attached. | ||||||||||||
Attached Files |
|
![]() |
|
nmuller (reporter) 2012-04-16 16:49 |
yes sure, I would have expected of course that t.i == 0 works, provided that we declare T t; in front of the lemna... |
nmuller (reporter) 2012-04-16 18:56 |
Under Nitrogen : frama-c -jessie file.c -> KO frama-c -jessie -jessie-atp file.c -> KO |
nmuller (reporter) 2012-04-17 13:47 |
it seems to work with wp on the gui |
virgile (developer) 2012-04-17 15:58 |
It seems like Jessie is not able to handle t.i when t is a logic variable (probably because it cannot transform it into &t->i like for a C lval). |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2012-04-16 11:28 | nmuller | New Issue | |
2012-04-16 11:28 | nmuller | Status | new => assigned |
2012-04-16 11:28 | nmuller | Assigned To | => virgile |
2012-04-16 11:28 | nmuller | File Added: unused.c | |
2012-04-16 12:44 | yakobowski | Relationship added | duplicate of 0001159 |
2012-04-16 16:49 | nmuller | Note Added: 0002885 | |
2012-04-16 18:56 | nmuller | Note Added: 0002897 | |
2012-04-17 13:47 | nmuller | Note Added: 0002915 | |
2012-04-17 15:58 | virgile | Note Added: 0002925 | |
2012-04-17 15:58 | virgile | Assigned To | virgile => cmarche |
2012-04-17 15:58 | virgile | Category | Kernel > ACSL implementation => Plug-in > jessie |
2012-04-17 15:58 | virgile | Product Version | Frama-C Carbon-20110201 => Frama-C GIT, precise the release id |
2012-04-17 17:31 | virgile | Relationship added | duplicate of 0001156 |
2012-04-17 17:43 | virgile | Relationship deleted | 0001159 |