Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000485Frama-CPlug-in > jessiepublic2010-05-18 15:452010-05-18 15:45
Reporterboris 
Assigned Tocmarche 
PrioritynormalSeverityfeatureReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090902 
Target VersionFixed in Version 
Summary0000485: Code containing consts should be verifiable
DescriptionJessie should be able to verify code that contains global C-constants as declared with the keyword const.

I consider using consts instead of macros good programming practice.
Additional Information// Doesn't verify:

const int size=4;

/*@ requires \valid(msg+(0..size));
*/
int setFoo(char* msg) {
  msg[size] = '\0';
  return 0;
}
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2010-05-18 15:45 boris New Issue
2010-05-18 15:45 boris Status new => assigned
2010-05-18 15:45 boris Assigned To => cmarche


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker