frama-c jessie killed during VC generation

Question

I'm trying to apply frama-c/jessie on a module of a proprietary safety critical system from our customer. The function under analysis is pretty big (image 700 uncommented lines count) with a lot of conditional statements as well as complex (&&, ||, etc).

I got this error message when I ran it on Ubuntu VM 64 bit machine. It appears Error 137 is related to memory size, etc. But I'm not quite sure.

Any suggestion for how to approach this error is greatly appreciated.

[

formal_verification]$ 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 tests.jessie
Generating Why function testFun
[jessie] Calling VCs generator.
gwhy-bin [...] why/test.why
Computation of VCs...
Killed
make: *** [test.stat] Error 137

Answer 1

with a lot of conditional statements as well as complex (&&, ||, etc).

You should use the so-called “fast WP” option when analyzing functions with lots of nested conditionals. Otherwise, the target does not even need to be very large to cause a blowup.

It happens to be the example in Jessie's manual for passing options to Why (it is really a Why option):

-jessie-why-opt=<s>
give an option to Why (e.g., -fast-wp)

You would therefore use -jessie-why-opt=-fast-wp.