AstraVer Toolset » Deductive Verification Tools for Linux Kernel

For instance, for the following program:

void func(int arg)
{
        (long unsigned int)( arg  == 0 ? -1 : 1);
}

Frama-C (CIL) issues the following error:

[kernel] Parsing test.c (with preprocessing)
[kernel] test.c:4:1: User Error: 
  cannot cast from void to unsigned long

  2     void func(int arg)
  3     {
  4             (long unsigned int)( arg  == 0 ? -1 : 1);
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  5     }
[kernel] User Error: skipping file test.c that has errors.
[kernel] Frama-C aborted: invalid user input.

when launched as follows:

toplevel.opt -no-autoload-plugins -no-findlib -machdep gcc_x86_64 test.c -print -print-lines -ocode test.cil.c

GCC can compile this code without any issues. You can read this discussion.