Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002128Frama-CPlug-in > wppublic2015-06-04 11:542015-06-08 23:34
Reporterloic 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionunable to reproduce 
PlatformLinuxOSUbuntuOS Version12.04.5 LTS
Product Version 
Target VersionFixed in VersionFrama-C Sodium 
Summary0002128: *i == *j cannot be proven from i == j
DescriptionNitrogen-20111001 alt-ergo 0.94 The following assertion cannot be proven. void pointer_testcase(int *i, int *j) { /*@ assert i == j ==> *i == *j; */ }
Steps To Reproduceframa-c -wp -wp-rte on the code above (also as attachment).
TagsNo tags attached.
Attached Filesc file icon pointer_testcase.c [^] (138 bytes) 2015-06-04 11:54 [Show Content]

- Relationships

-  Notes
(0005929)
virgile (developer)
2015-06-04 14:36

Nitrogen is an old version which is not supported anymore. The example works fine in Frama-C Sodium.

- Issue History
Date Modified Username Field Change
2015-06-04 11:54 loic New Issue
2015-06-04 11:54 loic Status new => assigned
2015-06-04 11:54 loic Assigned To => virgile
2015-06-04 11:54 loic File Added: pointer_testcase.c
2015-06-04 14:36 virgile Note Added: 0005929
2015-06-04 14:36 virgile Status assigned => resolved
2015-06-04 14:36 virgile Fixed in Version => Frama-C Sodium
2015-06-04 14:36 virgile Resolution open => unable to reproduce
2015-06-04 15:13 signoles Status resolved => closed
2015-06-08 23:34 yakobowski Category ptests => Plug-in > wp


Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker