Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001587Frama-CPlug-in > wppublic2013-12-16 12:152014-06-12 12:53
ReporterAnne 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001587: syntax error for alt-ergo with memset spec
DescriptionWhen 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 InformationCommand line is :
frama-c -cpp-extra-args=-I`frama-c -print-share-path`/libc pb_wp.c -wp
TagsNo tags attached.
Attached Filesc file icon pb_wp.c [^] (609 bytes) 2013-12-16 12:15 [Show Content]

- Relationships

-  Notes
(0004379)
correnson (manager)
2013-12-17 13:03

@Anne : merci pour le rapport de bug !
L.
(0004385)
correnson (manager)
2014-01-06 14:20

Fix committed to master branch.
(0004543)
correnson (manager)
2014-02-12 16:57

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2013-12-16 12:15 Anne New Issue
2013-12-16 12:15 Anne Status new => assigned
2013-12-16 12:15 Anne Assigned To => correnson
2013-12-16 12:15 Anne File Added: pb_wp.c
2013-12-17 13:03 svn Checkin
2013-12-17 13:03 svn Status assigned => resolved
2013-12-17 13:03 svn Resolution open => fixed
2013-12-17 13:03 correnson Note Added: 0004379
2014-01-06 14:20 correnson Note Added: 0004385
2014-02-12 16:57 correnson Note Added: 0004543
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed
2014-06-12 12:53 correnson Relationship added has duplicate 0001806
2014-06-12 12:55 correnson Relationship deleted has duplicate 0001806


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker