A pure predicate in an axiomatic with some "unpure" axioms have some strange results

ID0000073: This issue was created automatically from Mantis Issue 73. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0000073	Frama-C	Plug-in > jessie	public	2009-04-30	2009-06-23

Reporter	bobot	Assigned To	cmarche	Resolution	fixed
Priority	normal	Severity	crash	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C GIT, precise the release id	Target Version	-	Fixed in Version	Frama-C Beryllium-20090601-beta1

Description :

A 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 Information :

frama-c : 5186