Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000966Frama-CKernelpublic2011-09-19 10:522011-10-10 14:14
Reporterpherrmann 
Assigned Tovirgile 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000966: bad default assigns generation
DescriptionIn 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 InformationThe 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.
TagsNo tags attached.
Attached Filesc file icon bug_copy.c [^] (756 bytes) 2011-09-19 10:52 [Show Content]

- Relationships

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

- Issue History
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 Checkin
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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker