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