--- layout: fc_discuss_archives title: Message 4 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



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