Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
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

TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000451)
ayad (reporter)
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 (manager)
2009-10-15 12:26

Fixed in why 2.21

- 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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker