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

View Issue Details [ Jump to Notes ]

[ 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

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

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).

Notes

Date Modified	Username	Field	Change
Issue History
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
2013-12-19 01:14		Source_changeset_attached	=> framac master 76639685
2014-02-12 16:56		Source_changeset_attached	=> framac stable/neon 76639685

Issue History