syntax error for alt-ergo with memset spec
ID0001587: This issue was created automatically from Mantis Issue 1587. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001587 | Frama-C | Plug-in > wp | public | 2013-12-16 | 2014-06-12 |
| Reporter | Anne | Assigned To | correnson | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Fluorine-20130601 | Target Version | - | Fixed in Version | Frama-C Neon-20140301 |
Description :
When trying to prove the first loop invariant of this example, there is a message:
/tmp/wpd57f12.dir/typed/A_MemSet.ergo:10:[wp] user error: Prover Alt-Ergo returns Failed characters 6-106:typing error: syntax error
and neither the establishment nor the preservation can be proved.
Additional Information :
Command line is :
frama-c -cpp-extra-args=-Iframa-c -print-share-path/libc pb_wp.c -wp