Frama-C Bug Tracking System - Frama-C | |||||
View Issue Details | |||||
ID | Project | Category | View Status | Date Submitted | Last Update |
0000260 | Frama-C | Plug-in > jessie | public | 2009-09-30 16:12 | 2009-10-15 12:26 |
Reporter | dpariente | ||||
---|---|---|---|---|---|
Assigned To | ayad | ||||
Priority | normal | Severity | minor | Reproducibility | always |
Status | closed | Resolution | fixed | ||
Platform | OS | OS Version | |||
Product Version | Frama-C Beryllium-20090902 | ||||
Target Version | Fixed in Version | Frama-C Beryllium-20090902 | |||
Summary | 0000260: is_finite predicate: type double expected instead of real in .jc file | ||||
Description | Launching: 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 | ||||
Tags | No tags attached. | ||||
Relationships | |||||
Attached Files |
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 |