Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000642Frama-CPlug-in > wppublic2010-12-17 17:432011-04-13 15:28
Reportersduprat 
Assigned Todargaye 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20101201-beta1 
Target VersionFixed in VersionFrama-C Carbon-20110201 
Summary0000642: unprovable po with -split
Description
po of VAR2_PANNE seems to unprovable using -wp-split option. No problem without -wp-split for this property.

cmd:
sduprat@vmu3cat03:~/tmp$ frama-c-gui -pp-annot -wp -wp-proof alt-ergo -wp-model Store -wp-par 10 -wp-no-arrays source_combined.c -wp-split

sduprat@vmu3cat03:~/tmp$ frama-c-gui -pp-annot -wp -wp-proof alt-ergo -wp-model Store -wp-par 10 -wp-no-arrays source_combined.c

TagsNo tags attached.
Attached Filestar file icon src.tar [^] (20,480 bytes) 2010-12-17 17:43

- Relationships

-  Notes
(0001334)
dargaye (developer)
2010-12-20 15:05

fixed in rev. : 11073
(0001766)
signoles (manager)
2011-04-13 15:28

Fixed in WP 0.3 compatible with Frama-C Carbon.

- Issue History
Date Modified Username Field Change
2010-12-17 17:43 sduprat New Issue
2010-12-17 17:43 sduprat Status new => assigned
2010-12-17 17:43 sduprat Assigned To => dargaye
2010-12-17 17:43 sduprat File Added: src.tar
2010-12-20 15:05 dargaye Note Added: 0001334
2010-12-20 15:05 dargaye Status assigned => resolved
2010-12-20 15:05 dargaye Resolution open => fixed
2011-04-13 15:28 signoles Note Added: 0001766
2011-04-13 15:28 signoles Fixed in Version => Frama-C Carbon-20110201
2011-04-13 15:28 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker