View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0000966 | Frama-C | Kernel | public | 2011-09-19 10:52 | 2011-10-10 14:14 | ||||
Reporter | pherrmann | ||||||||
Assigned To | virgile | ||||||||
Priority | normal | Severity | major | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C GIT, precise the release id | ||||||||
Target Version | Fixed in Version | Frama-C Nitrogen-20111001 | |||||||
Summary | 0000966: bad default assigns generation | ||||||||
Description | In the attached program "bug_copy.c", when calling frama-c -jessie bug_copy.c the kernel adds an "assigns \nothing" clause to the contract: [jessie] Starting Jessie translation [kernel] warning: No code for function copy, default assigns generated for default behavior This added clause makes the contract invalid (i.e. jessie proves "assert(0)" after a call to function "copy"), since the behavior "from_init" actually assigns two cells of the "auto_state" array. | ||||||||
Additional Information | The problem disappears when the "complete behaviors" clause is added. svn id around 15100 Try frama-c -jessie bug_copy.c -jessie-gen-only -print to see the "assigns \nothing" clause added by the kernel. | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
monate (reporter) 2011-09-20 22:03 |
Jessie seems to do something fancy here: other plugins do not suffer from this. The generated default assigns is assigns auto_states[Init], auto_states[copy] For example use "-val -print" or "-wp -print" Anyway, whenever the "no code for function ... default assigns generated" appears, you should complete your specification. The auto-generation is only here to prevent from failing completly and to point out where you may need to proof check your specification. |
virgile (developer) 2011-09-21 09:10 |
The assigns \nothing indeed comes from Jessie itself. Kernel does the right thing here. On the other hand, while I agree that auto-generation of assigns cannot be used reliably, it should at least be consistent with existing behavior-specific assigns when it generates a global assigns (i.e. take the union of location, as is the case for kernel, but apparently not for jessie). |
virgile (developer) 2011-09-21 10:40 |
My bad, this is indeed a kernel bug: the contribution of jessie is only that it adds a default behavior to each function, whose assigns is then dutifully filled by the default assigns generator. You can observe the same behavior if you add an ensures \true; at the beginning of the spec of copy, with -val -print. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2011-09-19 10:52 | pherrmann | New Issue | |
2011-09-19 10:52 | pherrmann | File Added: bug_copy.c | |
2011-09-19 11:50 | pherrmann | Description Updated | |
2011-09-20 07:44 | signoles | Status | new => assigned |
2011-09-20 07:44 | signoles | Assigned To | => virgile |
2011-09-20 22:03 | monate | Note Added: 0002301 | |
2011-09-21 09:10 | virgile | Note Added: 0002302 | |
2011-09-21 09:10 | virgile | Category | Kernel => Plug-in > jessie |
2011-09-21 10:40 | virgile | Note Added: 0002305 | |
2011-09-21 10:40 | virgile | Category | Plug-in > jessie => Kernel |
2011-09-21 11:20 | svn | ||
2011-09-21 11:20 | svn | Status | assigned => resolved |
2011-09-21 11:20 | svn | Resolution | open => fixed |
2011-10-10 14:13 | signoles | Fixed in Version | => Frama-C Nitrogen-20111001 |
2011-10-10 14:14 | signoles | Status | resolved => closed |