is_finite predicate: type double expected instead of real in .jc file
ID0000260:
**This issue was created automatically from Mantis Issue 260. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000260 | Frama-C | Plug-in > jessie | public | 2009-09-30 | 2009-10-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | ayad | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090902 |
### 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
issue