--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on May 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] volatile type qualifiers



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                    |