--- layout: fc_discuss_archives title: Message 46 from Frama-C-discuss on February 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Casting puzzle - unproved?



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)