AstraVer Toolset » Deductive Verification Tools for Linux Kernel

Frama-C (CIL) fails to process valid GNU C source code. I attached the input files. Here is the command:

toplevel.opt "-no-autoload-plugins" "-no-findlib" "-machdep" "x86_64" "-c11" "-kernel-warn-key" "CERT:MSC:38=active" "-keep-logical-operators" "-remove-unused-inline-functions" "-remove-unused-static-functions" "-print" "-print-lines" "-no-print-annot" "-ocode" "cil.i" ".tmp_addr.abs-paths.trimmed.i" ".tmp_sysctl.abs-paths.trimmed.i" ".tmp_auth_generic.abs-paths.trimmed.i" ".tmp_backchannel_rqst.abs-paths.trimmed.i" ".tmp_sunrpc_syms.abs-paths.trimmed.i" ".tmp_rpc_pipe.abs-paths.trimmed.i" ".tmp_xprt.abs-paths.trimmed.i" ".tmp_svc.abs-paths.trimmed.i" ".tmp_timer.abs-paths.trimmed.i" ".tmp_xdr.abs-paths.trimmed.i" ".tmp_svcauth_unix.abs-paths.trimmed.i" ".tmp_cache.abs-paths.trimmed.i" ".tmp_xprtsock.abs-paths.trimmed.i" ".tmp_stats.abs-paths.trimmed.i" ".tmp_auth.abs-paths.trimmed.i" ".tmp_svcauth.abs-paths.trimmed.i" ".tmp_svc_xprt.abs-paths.trimmed.i" ".tmp_sched.abs-paths.trimmed.i" ".tmp_auth_null.abs-paths.trimmed.i" ".tmp_rpcb_clnt.abs-paths.trimmed.i" ".tmp_clnt.abs-paths.trimmed.i" ".tmp_bc_svc.abs-paths.trimmed.i" ".tmp_socklib.abs-paths.trimmed.i" ".tmp_auth_unix.abs-paths.trimmed.i" ".tmp_svcsock.abs-paths.trimmed.i" "atomic.abs-paths.trimmed.i" "dd.abs-paths.trimmed.i" "spi.abs-paths.trimmed.i" "err.abs-paths.trimmed.i" "module.bk.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" 

...
[kernel] .../linux-stable/include/linux/crypto.h:433:0: User Error: 
field `base' declared with a type containing a flexible array member.
...
[kernel] User Error: skipping file .tmp_xprtsock.abs-paths.trimmed.i that has errors.
[kernel] Frama-C aborted: invalid user input.