Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002169Frama-CPlug-in > wppublic2015-09-21 14:202015-09-21 14:20
ReporterJochen 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformSodium-20150201OSOS Versionxubuntu14.04
Product Version 
Target VersionFixed in Version 
Summary0002169: incomplete Alt-Ergo obligation files generated in presence of lemma "forall int x; ..." with "x" not occurring in "..."
DescriptionRunning "frama-c -wp 483.c -wp-out wp-out" on the attached file generates an Alt-Ergo obligation file "foo_assert_Alt-Ergo.mlw" which contains neither the lemma "xxx" nor the proof goal for the assertion in line 5. Apparently, Frama-C/Wp tacitly crashes during translating the lemma. The problem disappears ifin line 2 "int" is changed to "integer", or "\false" is changed to some formula containing "x".
TagsNo tags attached.
Attached Filesc file icon 483.c [^] (80 bytes) 2015-09-21 14:20 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2015-09-21 14:20 Jochen New Issue
2015-09-21 14:20 Jochen Status new => assigned
2015-09-21 14:20 Jochen Assigned To => correnson
2015-09-21 14:20 Jochen File Added: 483.c


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker