Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
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 file icon valinit.c [^] (4,137 bytes) 2011-04-14 16:11 [Show Content]

- Relationships

-  Notes
(0001929)
dargaye (developer)
2011-05-27 14:17

The constant of type string are not yet implemented for the moment in the Wp plugin's.
(0003751)
correnson (manager)
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 (manager)
2013-03-12 13:11

SVN 21663

- Issue History
Date Modified Username Field Change
2011-04-14 16:11 patrick New Issue
2011-04-14 16:11 patrick Status new => assigned
2011-04-14 16:11 patrick Assigned To => dargaye
2011-04-14 16:11 patrick File Added: valinit.c
2011-05-27 14:17 dargaye Note Added: 0001929
2011-05-27 14:31 dargaye Severity minor => feature
2011-07-04 14:37 dargaye Assigned To dargaye => correnson
2013-03-12 13:08 correnson Note Added: 0003751
2013-03-12 13:11 correnson Note Added: 0003752
2013-03-12 13:11 correnson Status assigned => resolved
2013-03-12 13:11 correnson Resolution open => fixed
2013-04-19 11:05 signoles Fixed in Version => Frama-C Fluorine
2013-04-19 11:05 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker