--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on May 2010 ---
Hi, Awesome tool suite! I just discovered Frama-C this morning. I especially like how the GUI compares results in rows from the various solvers. A couple questions. First, why does 'why-config' require exact solver versions? Even though we had Yices 1.0.26 installed, we had to go back to Yices 1.0.17 to get Why to use it. And second, why would inserting a volatile qualifier cause a type error? Here's my example (test.c): #include <stdint.h> // This works... //uint32_t * a; // But this throws a type error... volatile uint32_t * a; void f(double b) { *a = (uint32_t) b; } If the first declaration of 'a' is used, everything works fine. However, if 'a' is volatile this happens... e0082888 at e0082888-laptop:~/frama$ frama-c -jessie test.c [kernel] preprocessing with "gcc -C -E -I. -dD test.c" [jessie] Starting Jessie translation [jessie] Producing Jessie files in subdir test.jessie [jessie] File test.jessie/test.jc written. [jessie] File test.jessie/test.cloc written. [jessie] Calling Jessie tool in subdir test.jessie File "test.jc", line 40, characters 64-78: typing error: bad cast to integer [jessie] user error: Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs test.cloc test.jc And test.jc reveals this: unit f(double b) behavior default: ensures (C_6 : true); { { (C_5 : ((C_4 : a.unsigned_int_M) = (C_3 : ((C_2 : ((C_1 : (b :> integer)) :> uint32)) :> uint32)))); (return ()) } } What does the ':>' operator mean in this *.jc language? Thanks for any help. -Tom