2020-12-05 01:09 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000642Frama-CPlug-in > wppublic2011-04-13 15:28
Reportersduprat 
Assigned Todargaye 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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 Files
  • tar file icon src.tar (20,480 bytes) 2010-12-17 17:43

-Relationships
+Relationships

-Notes

~0001334

dargaye (developer)

fixed in rev. : 11073

~0001766

signoles (manager)

Fixed in WP 0.3 compatible with Frama-C Carbon.
+Notes

-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
+Issue History