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
Assigned Tocmarche 
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 - 2020 MantisBT Team
Powered by Mantis Bugtracker