Frama-C Bug Tracking System - Frama-C
View Issue Details
0000794Frama-CPlug-in > wppublic2011-04-14 16:112013-04-19 11:05
Reporterpatrick 
Assigned Tocorrenson 
PrioritynormalSeverityfeatureReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0000794: initial value of strings
DescriptionWP is unable to proof properties on initial value of a string.
That comes from the uncompleteness of the generated PO; there is nothing about the initial value of the string.
Additional Information> frama-c -wp -wp-prop p0 valinit.c -wp-proof alt-ergo
...
[wp] [Alt-Ergo] Goal store_main_post_9_p0 : Timeout


TagsNo tags attached.
Attached Filesc valinit.c (4,137) 2011-04-14 16:11
https://bts.frama-c.com/file_download.php?file_id=200&type=bug

Notes
(0001929)
dargaye   
2011-05-27 14:17   
The constant of type string are not yet implemented for the moment in the Wp plugin's.
(0003751)
correnson   
2013-03-12 13:08   
This bug is now corrected.
You must set the option -wp-literals to get the value of string literals axiomatized.
(0003752)
correnson   
2013-03-12 13:11   
SVN 21663

Issue History
2011-04-14 16:11patrickNew Issue
2011-04-14 16:11patrickStatusnew => assigned
2011-04-14 16:11patrickAssigned To => dargaye
2011-04-14 16:11patrickFile Added: valinit.c
2011-05-27 14:17dargayeNote Added: 0001929
2011-05-27 14:31dargayeSeverityminor => feature
2011-07-04 14:37dargayeAssigned Todargaye => correnson
2013-03-12 13:08corrensonNote Added: 0003751
2013-03-12 13:11corrensonNote Added: 0003752
2013-03-12 13:11corrensonStatusassigned => resolved
2013-03-12 13:11corrensonResolutionopen => fixed
2013-04-19 11:05signolesFixed in Version => Frama-C Fluorine
2013-04-19 11:05signolesStatusresolved => closed