Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Related Changesets ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001116Frama-CKernelpublic2012-03-12 10:262014-02-12 16:59
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeveritytrivialReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001116: axiom outside axiomatic tacitly ignored in presence of struct
DescriptionRunning frama-c -wp on the attached program doesn't produce a syntax error message, although using "axiom" outside "axiomatic" is incorrect.

However, the axiom is not given to the provers: alt-ergo can't verify the program, but it will verify it if "axiom" is changed to "lemma" (in that case, the lemma is given to alt-ergo).

If the struct in line 6-8 is removed, a syntax error is reported as expected (however at EOF position, which seems too late).
TagsNo tags attached.
Attached Filesc file icon ftest.c [^] (135 bytes) 2012-03-12 10:26 [Show Content]

- Relationships

-  Notes
(0002757)
Jochen (reporter)
2012-03-12 10:30

 Concerning the late syntax error position at EOF, there may be a connection to issue 0000840 "syntax error message refers to (true error line + 5 lines)".
(0002758)
signoles (manager)
2012-03-12 10:47

 Agree: an axiom outside an axiomatic should produce an error from the kernel.
(0004705)

2014-02-12 16:59

 Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2012-03-12 10:26 Jochen New Issue
2012-03-12 10:26 Jochen Status new => assigned
2012-03-12 10:26 Jochen Assigned To => correnson
2012-03-12 10:26 Jochen File Added: ftest.c
2012-03-12 10:30 Jochen Note Added: 0002757
2012-03-12 10:46 signoles Assigned To correnson => virgile
2012-03-12 10:47 signoles Note Added: 0002758
2012-03-12 10:47 signoles Category Plug-in > wp => Kernel
2012-04-02 15:51 svn Checkin
2012-04-02 15:51 svn Status assigned => resolved
2012-04-02 15:51 svn Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2014-02-12 16:59 Note Added: 0004705
2014-02-12 16:59 Status closed => resolved

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker