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

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000073

Frama-C

Plug-in > jessie

public

2009-04-30 14:46

2009-06-23 18:03

Reporter

bobot

Assigned To

cmarche

Priority

normal

Severity

crash

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C GIT, precise the release id

Target Version

Fixed in Version

Frama-C Beryllium-20090601-beta1

Summary

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

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

Tags

No 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