View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0000794 | Frama-C | Plug-in > wp | public | 2011-04-14 16:11 | 2013-04-19 11:05 | ||||
Reporter | patrick | ||||||||
Assigned To | correnson | ||||||||
Priority | normal | Severity | feature | Reproducibility | have not tried | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C GIT, precise the release id | ||||||||
Target Version | Fixed in Version | Frama-C Fluorine-20130401 | |||||||
Summary | 0000794: initial value of strings | ||||||||
Description | WP 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 | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
dargaye (developer) 2011-05-27 14:17 |
The constant of type string are not yet implemented for the moment in the Wp plugin's. |
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. |
correnson (manager) 2013-03-12 13:11 |
SVN 21663 |
![]() |
|||
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 |