Frama-C Bug Tracking System - Frama-C
View Issue Details
0000966Frama-CKernelpublic2011-09-19 10:522011-10-10 14:14
pherrmann 
virgile 
normalmajoralways
closedfixed 
Frama-C GIT, precise the release id 
Frama-C Nitrogen-20111001 
0000966: bad default assigns generation
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.
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.
No tags attached.
c bug_copy.c (756) 2011-09-19 10:52
https://bts.frama-c.com/file_download.php?file_id=277&type=bug
Issue History
2011-09-19 10:52pherrmannNew Issue
2011-09-19 10:52pherrmannFile Added: bug_copy.c
2011-09-19 11:50pherrmannDescription Updated
2011-09-20 07:44signolesStatusnew => assigned
2011-09-20 07:44signolesAssigned To => virgile
2011-09-20 22:03monateNote Added: 0002301
2011-09-21 09:10virgileNote Added: 0002302
2011-09-21 09:10virgileCategoryKernel => Plug-in > jessie
2011-09-21 10:40virgileNote Added: 0002305
2011-09-21 10:40virgileCategoryPlug-in > jessie => Kernel
2011-09-21 11:20svnCheckin
2011-09-21 11:20svnStatusassigned => resolved
2011-09-21 11:20svnResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed

Notes
(0002301)
monate   
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.
(0002302)
virgile   
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).
(0002305)
virgile   
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.