Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000073Frama-CPlug-in > jessiepublic2009-04-30 14:462009-06-23 18:03
Reporterbobot 
Assigned Tocmarche 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Beryllium-20090601-beta1 
Summary0000073: A pure predicate in an axiomatic with some "unpure" axioms have some strange results
DescriptionA pure predicate in an axiomatic with some "unpure" axioms have some strange results. In this case an assertion failed :

myc.c
============================
/*@
axiomatic myaxioms{

    predicate myrelation(int p,int q);
    logic int mylogic{L}(int * p);

    axiom myaxiom{L} :
    \forall int * p, q; \at(myrelation(mylogic(p),q),L);

}
@*/


frama-c -jessie-analysis unwanted_label.c.assertion_failed.c :
=========================
Calling Jessie tool in subdir unwanted_label.c.assertion_failed.jessie
File "jc/jc_typing.ml", line 2687, characters 20-20:
Uncaught exception: File "jc/jc_typing.ml", line 2687, characters 20-26: Assertion failed
===========================
Additional Informationframa-c : 5186
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2009-04-30 14:46 bobot New Issue
2009-04-30 16:49 monate Status new => assigned
2009-04-30 16:49 monate Assigned To => cmarche
2009-06-18 13:49 cmarche Status assigned => resolved
2009-06-18 13:49 cmarche Resolution open => fixed
2009-06-23 18:02 signoles Status resolved => closed
2009-06-23 18:03 signoles Fixed in Version => Frama-C Beryllium beta-1


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker