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. ## Attachments - [bug_copy.c](/uploads/119b6505e6023e4857c557a9f07838c5/bug_copy.c)