0000406: assert false (* TODO *) - Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000406

Frama-C

Plug-in > jessie

public

2010-02-16 10:16

2014-02-12 16:56

Reporter

sboldo

Assigned To

cmarche

Priority

normal

Severity

minor

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 Boron-20100401

Summary

0000406: assert false (* TODO *)

Description

Hello, I have run into an "assert false" in the code of jessie. It prevents me from describing an axiomatic. The assert false is here: File "jc/jc_typing.ml", line 2820, characters 29-29: that is to say: | JCTreal_cast (_, _) -> assert false (* TODO *) And I was unable to understand what this function is about in order to correct it. :-/ Here is a simplified axiomatization example that fails: # pragma JessieFloatModel(strict) /*@ axiomatic FP { @ @ axiom toto : @ \forall double f; 0x1p-1022 <= \abs(f) || \abs(f) < 0x1p-1022; @ } */ Reagrds, Sylvie Boldo

Tags

No tags attached.

Attached Files

Relationships

Notes
(0000681) cmarche (developer) 2010-02-16 10:19	Ouaip, c'est bien sur un bug. Neanmoins, meme si ce bug est corrigé, ce sera rejeté plus loin. Seul un lemma sera accepté.

(0000682) cmarche (developer) 2010-02-16 10:39	Fixed in why CVS

(0000776) signoles (manager) 2010-04-19 16:14	Fix in Why 2.24 (require Frama-C Boron-20100401).

Issue History
Date Modified	Username	Field	Change
2010-02-16 10:16	sboldo	New Issue
2010-02-16 10:16	sboldo	Status	new => assigned
2010-02-16 10:16	sboldo	Assigned To	=> cmarche
2010-02-16 10:19	cmarche	Note Added: 0000681
2010-02-16 10:39	cmarche	Note Added: 0000682
2010-02-16 10:39	cmarche	Status	assigned => resolved
2010-02-16 10:39	cmarche	Resolution	open => fixed
2010-04-19 16:13	signoles	Status	resolved => closed
2010-04-19 16:13	signoles	Fixed in Version	=> Frama-C Boron
2010-04-19 16:14	signoles	Note Added: 0000776