2021-01-22 20:49 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000260Frama-CPlug-in > jessiepublic2009-10-15 12:26
Reporterdpariente 
Assigned Toayad 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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

TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0000451

ayad (reporter)

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 (manager)

Fixed in why 2.21
+Notes

-Issue History
Date Modified Username Field Change
2009-09-30 16:12 dpariente New Issue
2009-09-30 19:42 signoles Status new => assigned
2009-09-30 19:42 signoles Assigned To => signoles
2009-09-30 19:42 signoles Assigned To signoles => cmarche
2009-10-01 10:01 signoles Assigned To cmarche => ayad
2009-10-14 09:36 ayad Note Added: 0000451
2009-10-14 10:04 signoles Status assigned => resolved
2009-10-14 10:04 signoles Resolution open => fixed
2009-10-15 12:25 signoles Status resolved => closed
2009-10-15 12:25 signoles Fixed in Version => Frama-C Beryllium 2
2009-10-15 12:26 signoles Note Added: 0000463
+Issue History