--- layout: fc_discuss_archives title: Message 46 from Frama-C-discuss on February 2014 ---
Hi, In my understanding conversion from int to double and then back to int should be the same. I was expecting this assert to be true. Did I model it wrong? #include <stdio.h> #include <limits.h> /*@ requires x != 0; assigns \nothing; */ void assert(int x); int x = 0; int main() { assert(x == (int)(double)x); return 0; } [formal_verification]$ frama-c -wp -wp-rte -lib-entry -pp-annot -wp-proof=alt-ergo double_casting_puzzle.c [kernel] preprocessing with "gcc -C -E -I. -dD double_casting_puzzle.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 : Unknown (1s) [wp] [Alt-Ergo] Goal typed_main_assert_rte_float_to_int : Unknown (1s) [wp] [Alt-Ergo] Goal typed_main_call_assert_pre : Unknown (1s)