ID0000794: **This issue was created automatically from Mantis Issue 794. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0000794 | Frama-C | Plug-in > wp | public | 2011-04-14 | 2013-04-19 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | patrick | **Assigned To** | correnson | **Resolution** | fixed | | **Priority** | normal | **Severity** | feature | **Reproducibility** | have not tried | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Fluorine-20130401 | ### 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 ## Attachments - [valinit.c](/uploads/eae1e5e251e971c442edd54f99d0c958/valinit.c)