Project

General

Profile

Bug #9544

Better support of fields declared using flexible array members

Added by Evgeny Novikov 4 months ago. Updated 4 months ago.

Status:
Closed
Priority:
Urgent
Start date:
03/14/2019
Due date:
% Done:

0%

Estimated time:
Detected in build:
svn
Platform:
Published in build:

Description

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" 

And here is the error:
...
[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.


Files

fvtp.tar.gz (8.25 MB) fvtp.tar.gz Evgeny Novikov, 03/14/2019 10:48 AM

Related issues

Blocks Klever - Bug #6629: Used CIL is outdatedClosed03/13/2019

Actions

History

#1

Updated by Evgeny Novikov 4 months ago

  • Blocks Bug #6629: Used CIL is outdated added
#2

Updated by Mikhail Mandrykin 4 months ago

  • Status changed from New to Feedback

For some reason in latest upstream Frama-C the flexible array members in nested structures were disallowed. However, due to their prevalence in Linux kernel source code we already enabled them back in GCC mode. So Frama-C succeeds on this code with "-machdep" "gcc_x86_64" (with gcc_).

#3

Updated by Evgeny Novikov 4 months ago

Thank you for explaining the issue. With this option everything seems to work nice. You can close the bug!

#4

Updated by Mikhail Mandrykin 4 months ago

  • Status changed from Feedback to Closed

Also available in: Atom PDF