Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000327Frama-CKernel > ACSL implementationpublic2009-11-10 09:342010-04-13 15:33
Reportercmarche 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Boron-20100401 
Summary0000327: order of 'decreases' and 'behavior' clauses
DescriptionThe ACSL grammar specifies that function contracts have the form

function-contract ::= simple-behavior named-behavior* decreases-clause?

however, Frama-C accepts the following without giving any errors nor warnings, and silently ignores the behaviors.

I think that the camlyacc parser should look for the "EOF" terminator of specs to prevent from silently ignore erroneous garbage.

By the way, I think that decreases clauses should be accepted also between requires and behaviors. The reason is that 'decreases t' refer to the value of t in the pre-state, and it seems more natural to me to put clauses realted to the pre-state before those related to the post-state.

/*@ decreases 101-n ;
  @ behavior less_than_101:
  @ assumes n <= 100;
  @ ensures \result == 91;
  @ behavior greater_than_100:
  @ assumes n >= 101;
  @ ensures \result == n - 10;
  @*/
int f91(int n) {
  if (n <= 100) {
    return f91(f91(n + 11));
  }
  else
    return n - 10;
}

Additional InformationPour preciser ma pensee concernant ocamlyacc et logic_parser.mly: l'entree "annot" a la forme

annot: annotation EOF

et je pense que les autres entrees de la grammaire, lexpr et spec, devraient subir le meme traitement.

TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2009-11-10 09:34 cmarche New Issue
2009-11-10 09:40 cmarche Assigned To => virgile
2009-11-10 09:40 cmarche Status new => assigned
2009-11-10 09:40 cmarche Description Updated
2009-11-10 09:40 cmarche Additional Information Updated
2009-11-10 10:10 virgile Relationship added duplicate of 0000228
2009-11-10 10:11 virgile Duplicate ID 0 => 228
2009-11-10 10:11 virgile Status assigned => resolved
2009-11-10 10:11 virgile Resolution open => duplicate
2009-11-10 10:53 signoles Status resolved => closed
2009-11-10 17:26 signoles Status closed => resolved
2009-11-10 17:26 signoles Resolution duplicate => fixed
2009-11-10 17:26 signoles Duplicate ID 228 => 0
2010-02-05 09:46 signoles Category Kernel => Kernel > ACSL implementation
2010-02-05 09:46 signoles Additional Information Updated
2010-04-13 15:30 signoles Status resolved => new
2010-04-13 15:31 signoles Status new => closed
2010-04-13 15:33 signoles Fixed in Version => Frama-C Boron


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker