| Anonymous | Login | Signup for a new account | This BTS is being migrated to Gitlab, consider using those issues instead |  |
| 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 | ||||||||
| 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 | ||||||||||
| Platform | OS | OS Version | |||||||||||
| 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 |  unused.c [^] (200 bytes) 2012-04-16 11:28 [Show Content]
| ||||||||||||
 Relationships |
 Notes |
|
|
(0002885) 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... |
|
(0002897) nmuller (reporter) 2012-04-16 18:56 |
Under Nitrogen : frama-c -jessie file.c -> KO frama-c -jessie -jessie-atp file.c -> KO |
|
(0002915) nmuller (reporter) 2012-04-17 13:47 |
it seems to work with wp on the gui |
|
(0002925) 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). |
|
Notes |
|
Issue History |
|||
| 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 |
|
Issue History |
| Copyright © 2000 - 2020 MantisBT Team |
|