Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000544Frama-CPlug-in > jessiepublic2010-07-17 02:512010-07-17 02:51
Reporterlogan 
Assigned Tocmarche 
PrioritynormalSeverityfeatureReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in Version 
Summary0000544: Enhancement on assigns annotation and the name of proof obligation
DescriptionConsider the following functions. Both function violates
ACSL specification, and all of the theorem prover gives
UNKNOWN as result (which is correct and expected).

However, the name of proof obligation of test2() is
"loop invariants initially holds" which is a little
confusing. Since the problem is actually on the assign
statement instead of the while-loop. I think it will be
better to have an independent check for @assigns annotation
just like the "postcondition" proof obligation of test1().

--------------------------------------------------------
int global;

/*@ assigns \nothing;
 */
int test1() {
  global = 1;
}

/*@ assigns \nothing;
 */
int test2() {
  global = 2;

  /*@ loop variant 0; */
  while (0) {
  }
}
--------------------------------------------------------
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2010-07-17 02:51 logan New Issue
2010-07-17 02:51 logan Status new => assigned
2010-07-17 02:51 logan Assigned To => cmarche


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker