bad default assigns generation
ID0000966: This issue was created automatically from Mantis Issue 966. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000966 | Frama-C | Kernel | public | 2011-09-19 | 2011-10-10 |
| Reporter | pherrmann | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | Frama-C Nitrogen-20111001 |
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.