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

Also available in: Atom PDF