WP: Assertion not proved -> conversion from float to int issue?
ID0001655: This issue was created automatically from Mantis Issue 1655. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001655 | Frama-C | Plug-in > wp | public | 2014-02-27 | 2014-06-02 |
| Reporter | dharma | Assigned To | correnson | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | Ubuntu | OS | Linux | OS Version | - |
| Product Version | Frama-C Fluorine-20130601 | Target Version | - | Fixed in Version | - |
Description :
I'm using Frama-C for my course at UMD. Found it pretty helpful.
I tried this puzzle, but cannot get WP to prove the assertion, which is true.
I ran through the GDB and found that the value of i is INT_MIN, satisfying the assert.
#include <limits.h>
/*@ requires x != 0; assigns \nothing; */ void assert(int x);
int main() { float f = INT_MAX; int i = f; assert(i == INT_MIN); return 0; }
Steps To Reproduce :
[formal_verification]$ frama-c -wp -wp-rte float_to_int_assert.c [kernel] preprocessing with "gcc -C -E -I. float_to_int_assert.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 (8ms) [wp] [Alt-Ergo] Goal typed_main_assert_rte_float_to_int : Valid (12ms) [wp] [Alt-Ergo] Goal typed_main_call_assert_pre : Unknown