Project

General

Profile

Actions
Copy link

Feature #10361

open

Static initialization of flexible array members is an unsupported GNU extension

Added by Evgeny Novikov almost 4 years ago. Updated about 2 years ago.

Status:
New
Priority:
High
Assignee:
Mikhail Mandrykin
Start date:
05/29/2020
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

There are quite many failures related with this unsupported feature during verification of Linux loadable kernel modules. If this is not hard to implement this feature, it would be great.

A attached an example of the C source file for which there are following errors:

[kernel] /home/debian/klever-inst/klever/build bases/linux-5.5/Storage/home/zakharov/src/linux-stable/drivers/media/i2c/et8ek8/et8ek8_mode.c:18:0: User Error:
  static initialization of flexible array members is an unsupported GNU extension
[kernel] /home/debian/klever-inst/klever/build bases/linux-5.5/Storage/home/zakharov/src/linux-stable/drivers/media/i2c/et8ek8/et8ek8_mode.c:119:0: User Error:
  static initialization of flexible array members is an unsupported GNU extension
[kernel] /home/debian/klever-inst/klever/build bases/linux-5.5/Storage/home/zakharov/src/linux-stable/drivers/media/i2c/et8ek8/et8ek8_mode.c:175:0: User Error:
  static initialization of flexible array members is an unsupported GNU extension
[kernel] /home/debian/klever-inst/klever/build bases/linux-5.5/Storage/home/zakharov/src/linux-stable/drivers/media/i2c/et8ek8/et8ek8_mode.c:231:0: User Error:
  static initialization of flexible array members is an unsupported GNU extension
[kernel] /home/debian/klever-inst/klever/build bases/linux-5.5/Storage/home/zakharov/src/linux-stable/drivers/media/i2c/et8ek8/et8ek8_mode.c:287:0: User Error:
  static initialization of flexible array members is an unsupported GNU extension
[kernel] /home/debian/klever-inst/klever/build bases/linux-5.5/Storage/home/zakharov/src/linux-stable/drivers/media/i2c/et8ek8/et8ek8_mode.c:343:0: User Error:
  static initialization of flexible array members is an unsupported GNU extension
[kernel] /home/debian/klever-inst/klever/build bases/linux-5.5/Storage/home/zakharov/src/linux-stable/drivers/media/i2c/et8ek8/et8ek8_mode.c:398:0: User Error:
  static initialization of flexible array members is an unsupported GNU extension
[kernel] /home/debian/klever-inst/klever/build bases/linux-5.5/Storage/home/zakharov/src/linux-stable/drivers/media/i2c/et8ek8/et8ek8_mode.c:454:0: User Error:
  static initialization of flexible array members is an unsupported GNU extension
[kernel] /home/debian/klever-inst/klever/build bases/linux-5.5/Storage/home/zakharov/src/linux-stable/drivers/media/i2c/et8ek8/et8ek8_mode.c:510:0: User Error:
  static initialization of flexible array members is an unsupported GNU extension
[kernel] /home/debian/klever-inst/klever/build bases/linux-5.5/Storage/home/zakharov/src/linux-stable/drivers/media/i2c/et8ek8/et8ek8_mode.c:565:0: User Error:
  static initialization of flexible array members is an unsupported GNU extension
[kernel] User Error: skipping file /home/debian/klever-inst/klever-work/native-scheduler/scheduler/jobs/9e762226-2206-4f95-9b31-3095b99785e8/klever-core-work-dir/job/vtg/drivers/media/i2c/et8ek8/et8ek8.ko/memory safety/weaver/et8ek8_mode.c that has errors.
[kernel] Frama-C aborted: invalid user input.

Files

Download all files
et8ek8_mode.c (3.19 MB) et8ek8_mode.c Evgeny Novikov, 05/29/2020 05:09 PM
input.tar.gz (333 KB) input.tar.gz Evgeny Novikov, 03/09/2022 11:01 AM
Actions
Copy link
 #1

Updated by Evgeny Novikov about 2 years ago

It seems that there is another, also quite widespread sequence of this unsupported GNU extension. When I ran the following command for the attached source file:

toplevel.opt "-no-autoload-plugins" "-no-findlib" "-kernel-log" "e:problem desc.txt" "-machdep" "gcc_x86_64" "-c11" "-kernel-warn-key" "CERT:MSC:38=active" "-remove-unused-inline-functions" "-remove-unused-static-functions" "-no-annot" "-no-single-return" "-fold-temp-vars" "-shrink-initializers" "-keep-logical-operators" "-aggressive-merging" "-print" "-print-lines" "-no-print-annot" "-ocode" "cil.i" "-more-files" "input files"

I got the following error within "problem desc.txt":

.../linux-5.10.27/drivers/md/bcache/bset.h:217:[kernel] user error: declaration of array of incomplete type 'struct bset_tree`
.../linux-5.10.27/drivers/md/bcache/bcache.h:231:[kernel] user error: declaration of array of incomplete type 'struct keybuf_key`
[kernel] user error: skipping file .../stats.i that has errors.

while GCC can handle the corresponding source file without errors. You can note that both these structures refer this one:

struct bkey {
 __u64 high;
 __u64 low;
 __u64 ptr[];
};

This issue is responsible for failures for ~1.4% of all drivers of Linux 5.10. Both these issues break verification of ~2.8% of these drivers.

Actions
Copy link

Also available in: Atom PDF