Frama-C Bug Tracking System - Frama-C
View Issue Details
0001587Frama-CPlug-in > wppublic2013-12-16 12:152014-06-12 12:53
Anne 
correnson 
normalminorhave not tried
closedfixed 
Frama-C Fluorine-20130601 
Frama-C Neon-20140301 
0001587: syntax error for alt-ergo with memset spec
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.
Command line is : frama-c -cpp-extra-args=-I`frama-c -print-share-path`/libc pb_wp.c -wp
No tags attached.
c pb_wp.c (609) 2013-12-16 12:15
https://bts.frama-c.com/file_download.php?file_id=623&type=bug
Issue History
2013-12-16 12:15AnneNew Issue
2013-12-16 12:15AnneStatusnew => assigned
2013-12-16 12:15AnneAssigned To => correnson
2013-12-16 12:15AnneFile Added: pb_wp.c
2013-12-17 13:03svnCheckin
2013-12-17 13:03svnStatusassigned => resolved
2013-12-17 13:03svnResolutionopen => fixed
2013-12-17 13:03corrensonNote Added: 0004379
2014-01-06 14:20corrensonNote Added: 0004385
2014-02-12 16:57corrensonNote Added: 0004543
2014-03-13 15:56signolesFixed in Version => Frama-C Neon-20140301
2014-03-13 15:57signolesStatusresolved => closed
2014-06-12 12:53corrensonRelationship addedhas duplicate 0001806
2014-06-12 12:55corrensonRelationship deletedhas duplicate 0001806

Notes
(0004379)
correnson   
2013-12-17 13:03   
@Anne : merci pour le rapport de bug ! L.
(0004385)
correnson   
2014-01-06 14:20   
Fix committed to master branch.
(0004543)
correnson   
2014-02-12 16:57   
Fix committed to stable/neon branch.