AstraVer Toolset » Deductive Verification Tools for Linux Kernel

First experiments with Frama-C CIL clearly showed that it is not so efficient as former CIL (1.5.1 with LDV patches).

I launched CIL 1.5.1 with the following command-line options (input and output files are in attached old.tar.gz):

cilly.asm.exe "--printCilAsIs" "--domakeCFG" "--decil" "--noInsertImplicitCasts" "--useLogicalOperators" "--ignore-merge-conflicts" "--no-convert-direct-calls" "--no-convert-field-offsets" "--no-split-structs" "--rmUnusedInlines" "--out" "cil.i" ".tmp_i7300_idle.abs-paths.trimmed.i" "atomic.abs-paths.trimmed.i" "io.bk.abs-paths.trimmed.i" "dd.abs-paths.trimmed.i" "spi.abs-paths.trimmed.i" "err.abs-paths.trimmed.i" "panic.abs-paths.trimmed.i" "common.abs-paths.trimmed.i" "slab.abs-paths.trimmed.i" "memory.abs-paths.trimmed.i" "gcc.abs-paths.trimmed.i" "nondet.abs-paths.trimmed.i" "reference memory.abs-paths.trimmed.i" "environment_model.abs-paths.trimmed.i" "bug kind funcs.trimmed.i" 

After that we have to fix the CIL output a bit. There is file cil.fixed.i in the archive. That file was provided to CPAchecker as input (see CPAchecker files - old CIL.zip).

Old CIL takes about 2 seconds of CPU time and 40 MB of RAM. CPAchecker spent just ~50 seconds of CPU time and ~1 GB of RAM.

New CIL (indeed Frama-C from our branch 18.0) was launched with the following command-line options (input and output files are in attached new.tar.gz):

toplevel.opt "-no-autoload-plugins" "-no-findlib" "-c11" "-kernel-warn-key" "CERT:MSC:38=inactive" "-keep-logical-operators" "-print" "-print-lines" "-no-print-annot" "-ocode" "cil.i" ".tmp_i7300_idle.abs-paths.trimmed.i" "atomic.abs-paths.trimmed.i" "io.bk.abs-paths.trimmed.i" "dd.abs-paths.trimmed.i" "spi.abs-paths.trimmed.i" "err.abs-paths.trimmed.i" "panic.abs-paths.trimmed.i" "common.abs-paths.trimmed.i" "slab.abs-paths.trimmed.i" "memory.abs-paths.trimmed.i" "gcc.abs-paths.trimmed.i" "nondet.abs-paths.trimmed.i" "reference memory.abs-paths.trimmed.i" "environment_model.abs-paths.trimmed.i" "bug kind funcs.trimmed.i" 

Its output file was passed to CPAchecker as is (CPAchecker files - new CIL.zip).

New CIL (Frama-C) consumed ~7 seconds of CPU time and ~220 MB of RAM. Also it outputs a large source file that took very much time from CPAchecker, namely, ~1.5 minutes of CPU time and ~1.5 GB of RAM.

New CIL processes source code better since I did not need any patches before/after it. The only thing I had to do is getting rid of tricky inline Assembler that is not supported by CPAchecker still.

But taking into account a disaster with computational resources consumption, at the moment there are little chances to switch to the new CIL. Can you provide any ideas, how to fix the situation. We do not suffer much from more hungry CIL since it does not influence total computational resources consumption much, but its output should be improved very considerably.
Taking all this into account