--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on May 2010 ---
Please fill in a bug report, Anyway, I think the answer should have been "volatile are not supported by Jessie" - Claude Tom Hawkins wrote: > 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 > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |