Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000484Frama-CKernel > ACSL implementationpublic2010-05-18 09:322014-02-12 16:55
Reporterpatrick 
Assigned Topatrick 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000484: function and statement behaviors
Description1) 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
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000856)
patrick (developer)
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 (developer)
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 (developer)
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 (developer)
2010-05-19 09:01

The text "behavior default" is no more pretty printed when it has no assumes clause.
(0000903)
patrick (developer)
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)


- Issue History
Date Modified Username Field Change
2010-05-18 09:32 patrick New Issue
2010-05-18 09:32 patrick Status new => assigned
2010-05-18 09:32 patrick Assigned To => virgile
2010-05-18 09:33 patrick Assigned To virgile => patrick
2010-05-18 09:51 patrick Description Updated
2010-05-18 10:15 patrick Note Added: 0000856
2010-05-18 16:14 patrick Note Edited: 0000856
2010-05-18 16:20 patrick Note Added: 0000860
2010-05-19 08:06 patrick Note Edited: 0000860
2010-05-19 08:10 patrick Note Added: 0000861
2010-05-19 08:10 svn Checkin
2010-05-19 08:11 svn Checkin
2010-05-19 08:42 svn Checkin
2010-05-19 09:01 patrick Note Added: 0000865
2010-05-19 10:26 svn Checkin
2010-05-19 12:26 svn Checkin
2010-05-19 13:18 svn Checkin
2010-05-19 14:48 svn Checkin
2010-05-19 19:27 monate Status assigned => resolved
2010-05-19 19:27 monate Resolution open => fixed
2010-05-20 08:07 svn Checkin
2010-05-25 10:57 svn Checkin
2010-06-04 08:30 patrick Note Added: 0000903
2010-06-04 08:30 patrick Status resolved => feedback
2010-06-04 08:30 patrick Resolution fixed => reopened
2010-06-04 08:31 patrick Status feedback => assigned
2010-06-04 08:32 patrick Status assigned => confirmed
2010-06-04 09:03 patrick Note Edited: 0000903
2010-06-04 09:24 patrick Status confirmed => resolved
2010-06-04 09:24 patrick Resolution reopened => fixed
2010-12-10 15:45 signoles Fixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:36 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker