Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002126Frama-CPlug-in > wppublic2015-06-02 08:522016-01-26 08:43
Reportervirgile 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Magnesium 
Summary0002126: WP crashes on generation of PO for assigns clause (assertion failure in MemVar.ml)
DescriptionOn the example source below, frama-c -wp reduced.i crashes with the following error:
File "src/wp/MemVar.ml", line 491, characters 54-60: Assertion failed

Apparently (by inferring why the offending function in MemVar got called), the p1+0 in the assigns for fn1 leads WP to think that p1 should be instantiated with an array (in particular, if you remove the +0, everything is fine).

-- reduced.i
/*@ assigns *(p1); */
int fn1(char *p1);

/*@
  assigns \nothing;
*/
void fn2(void) {
  char pcr_index;
  fn1(&pcr_index);
}
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0005951)
correnson (manager)
2015-06-29 16:42

Proved by Qed.

- Issue History
Date Modified Username Field Change
2015-06-02 08:52 virgile New Issue
2015-06-02 08:52 virgile Status new => assigned
2015-06-02 08:52 virgile Assigned To => correnson
2015-06-02 08:53 virgile Relationship added has duplicate 0002124
2015-06-29 16:42 correnson Note Added: 0005951
2015-06-29 16:42 correnson Status assigned => resolved
2015-06-29 16:42 correnson Fixed in Version => Frama-C Magnesium
2015-06-29 16:42 correnson Resolution open => fixed
2016-01-26 08:43 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker