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