Frama-C Bug Tracking System - Frama-C
View Issue Details
0000484Frama-CKernel > ACSL implementationpublic2010-05-18 09:322014-02-12 16:55
patrick 
patrick 
normalminoralways
closedfixed 
Frama-C Boron-20100401 
Frama-C Carbon-20101201-beta1 
0000484: function and statement behaviors
1) implements require clauses given into function and statement behaviors
2) changes the grammar of behavior-body-stmt:

behavior-body-stmt ::=
   assumes-clause* requires-clause* simple-clauses-stmt*
simple-clause-stmt ::=
   simple-clause | abrupt-clause-stmt
No tags attached.
Issue History
2010-05-18 09:32patrickNew Issue
2010-05-18 09:32patrickStatusnew => assigned
2010-05-18 09:32patrickAssigned To => virgile
2010-05-18 09:33patrickAssigned Tovirgile => patrick
2010-05-18 09:51patrickDescription Updated
2010-05-18 10:15patrickNote Added: 0000856
2010-05-18 16:14patrickNote Edited: 0000856
2010-05-18 16:20patrickNote Added: 0000860
2010-05-19 08:06patrickNote Edited: 0000860
2010-05-19 08:10patrickNote Added: 0000861
2010-05-19 08:10svnCheckin
2010-05-19 08:11svnCheckin
2010-05-19 08:42svnCheckin
2010-05-19 09:01patrickNote Added: 0000865
2010-05-19 10:26svnCheckin
2010-05-19 12:26svnCheckin
2010-05-19 13:18svnCheckin
2010-05-19 14:48svnCheckin
2010-05-19 19:27monateStatusassigned => resolved
2010-05-19 19:27monateResolutionopen => fixed
2010-05-20 08:07svnCheckin
2010-05-25 10:57svnCheckin
2010-06-04 08:30patrickNote Added: 0000903
2010-06-04 08:30patrickStatusresolved => feedback
2010-06-04 08:30patrickResolutionfixed => reopened
2010-06-04 08:31patrickStatusfeedback => assigned
2010-06-04 08:32patrickStatusassigned => confirmed
2010-06-04 09:03patrickNote Edited: 0000903
2010-06-04 09:24patrickStatusconfirmed => resolved
2010-06-04 09:24patrickResolutionreopened => fixed
2010-12-10 15:45signolesFixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:36signolesStatusresolved => closed

Notes
(0000856)
patrick   
2010-05-18 10:15   
(edited on: 2010-05-18 16:14)
1) A field [b_requires] will be added into [Cil_types.behavior]
2) So, the field [spec_requires] will be removed from [Cil_types.spec].
   Its value will be moved into the [b_requires] field of the "default" behavior
   which must have NO assumes clauses
3) So, the access to the [spec_requires] will be replaced
   by a call to the function [Cil.find_defauts_requires]

(0000860)
patrick   
2010-05-18 16:20   
(edited on: 2010-05-19 08:06)
Some functions have been moved from [src/kernel/Ast_info.ml] to [cil/src/Cil.ml]:
[Cil.is_default_behavior]
[Cil.find_default_behavior]

(0000861)
patrick   
2010-05-19 08:10   
The grammar of statement contract will allow requires into the default behavior (as function contract):

simple-behavior-stmt :==
  requires* (simple-clause | abrupt-clause-stmt)*
(0000865)
patrick   
2010-05-19 09:01   
The text "behavior default" is no more pretty printed when it has no assumes clause.
(0000903)
patrick   
2010-06-04 08:30   
(edited on: 2010-06-04 09:03)
Needs for behavior id checking: forbidden to define more than one behavior with same id into the whole function. (see bug 498)