Frama-C Bug Tracking System - Frama-C
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0000260Frama-CPlug-in > jessiepublic2009-09-30 16:122009-10-15 12:26
Reporterdpariente 
Assigned Toayad 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090902 
Target VersionFixed in VersionFrama-C Beryllium-20090902 
Summary0000260: is_finite predicate: type double expected instead of real in .jc file
DescriptionLaunching: frama-c -jessie foo.c with foo.c containing: double f(double a , double b ) { double t ; t = 0.0; //@ assert \is_finite((double)(a-b)); t = a - b; return (t); } yields: File "foo.jc", line 36, characters 56-71: typing error: type double expected instead of real [jessie] user error: Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs foo.cloc foo.jc ":> real" in foo.jc should be removed when used within "is_finite_double" predicate, not? Regards, Dillon
Steps To Reproduce
Additional Information
TagsNo tags attached.
Relationships
Attached Files
Issue History
Date ModifiedUsernameFieldChange
2009-09-30 16:12dparienteNew Issue
2009-09-30 19:42signolesStatusnew => assigned
2009-09-30 19:42signolesAssigned To => signoles
2009-09-30 19:42signolesAssigned Tosignoles => cmarche
2009-10-01 10:01signolesAssigned Tocmarche => ayad
2009-10-14 09:36ayadNote Added: 0000451
2009-10-14 10:04signolesStatusassigned => resolved
2009-10-14 10:04signolesResolutionopen => fixed
2009-10-15 12:25signolesStatusresolved => closed
2009-10-15 12:25signolesFixed in Version => Frama-C Beryllium 2
2009-10-15 12:26signolesNote Added: 0000463

Notes
(0000451)
ayad   
2009-10-14 09:36   
it is solved now by adding the following warning when the used mode is "real": "\is_finite always true in mode JessieFloatModel(real)" We have an analogue warning for the "strict" mode and for "\is_infinite,\is_NaN,\is_plus_infinity,\is_minus_infinity". Best regards. Ali Ayad
(0000463)
signoles   
2009-10-15 12:26   
Fixed in why 2.21