Frama-C Bug Tracking System - Frama-C
View Issue Details
0000642Frama-CPlug-in > wppublic2010-12-17 17:432011-04-13 15:28
sduprat 
dargaye 
normalminoralways
closedfixed 
Frama-C Carbon-20101201-beta1 
Frama-C Carbon-20110201 
0000642: unprovable po with -split
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
No tags attached.
tar src.tar (20,480) 2010-12-17 17:43
https://bts.frama-c.com/file_download.php?file_id=136&type=bug
Issue History
2010-12-17 17:43sdupratNew Issue
2010-12-17 17:43sdupratStatusnew => assigned
2010-12-17 17:43sdupratAssigned To => dargaye
2010-12-17 17:43sdupratFile Added: src.tar
2010-12-20 15:05dargayeNote Added: 0001334
2010-12-20 15:05dargayeStatusassigned => resolved
2010-12-20 15:05dargayeResolutionopen => fixed
2011-04-13 15:28signolesNote Added: 0001766
2011-04-13 15:28signolesFixed in Version => Frama-C Carbon-20110201
2011-04-13 15:28signolesStatusresolved => closed

Notes
(0001334)
dargaye   
2010-12-20 15:05   
fixed in rev. : 11073
(0001766)
signoles   
2011-04-13 15:28   
Fixed in WP 0.3 compatible with Frama-C Carbon.