int to double - assert not verified
ID0001651: This issue was created automatically from Mantis Issue 1651. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001651 | Frama-C | Plug-in > wp | public | 2014-02-24 | 2014-06-02 |
| Reporter | dharma | Assigned To | correnson | Resolution | no change required |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | Ubuntu | OS | Linux | OS Version | 64 bit |
| Product Version | Frama-C Fluorine-20130601 | Target Version | - | Fixed in Version | - |
Description :
For this below program, the assert should be valid I think but the WP is not proving it.
#include <limits.h>
/*@ requires x != 0; assigns \nothing; */ void assert(int x);
int main() { double f = INT_MAX; int i = f; assert(i == INT_MAX); return 0; }
Additional Information :
The regular C assert was able to prove when I run the a.out after compiling the wrong (commenting the ACSL's assert).
Steps To Reproduce :
[formal_verification]$ frama-c -wp -wp-rte double_to_int_max_2.c -pp-annot [kernel] preprocessing with "gcc -C -E -I. -dD double_to_int_max_2.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage [rte] annotating function main [wp] 3 goals scheduled [wp] [Alt-Ergo] Goal typed_main_assert_rte_float_to_int_2 : Valid (4ms) [wp] [Alt-Ergo] Goal typed_main_assert_rte_float_to_int : Valid (12ms) [wp] [Alt-Ergo] Goal typed_main_call_assert_pre : Unknown (1s)