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 - 2019 MantisBT Team
Powered by Mantis Bugtracker