Skip to content

[kernel] Crash when parsing compound literal in `sizeof`

I often use sizeof in macros with compound literals as arguments, to use a list of values to initialize both an array value and the value of its size. But this is not supported by the Frama-C kernel. It seems to crash after the parsing step is completed.

Here is a minimal practical example:

#include <stddef.h>

long index_in_str_array(char const * str, char const * const array[], size_t nb_elems);
#define index_of_str(str, ...) \
  index_in_str_array(str, ((char const *[])__VA_ARGS__), sizeof((char const *[])__VA_ARGS__) / sizeof(char const *))

void Help(void);

int main(int argc, char const * argv[])
{
  if (index_of_str(argv[1], { "-help", "?" }) >= 0) {
    Help();
  }
}

Steps to reproduce the issue

A simple code like this:

int main()
{
   sizeof((int[]){ 1, 2, 3 });
}

makes Frama-C:

frama-c compound_in_sizeof.c

crash.

Expected behaviour

Nothing special. Just, this shouldn’t crash.

Actual behaviour

I’m getting the following output:

[kernel] Parsing compound_in_sizeof.c (with preprocessing)
[kernel] compound_in_sizeof.c:3: Dropping side-effect in sizeof.
[kernel] Current source was: <unknown>
  The full backtrace is:
  Raised at Frama_c_kernel__Kernel_function.local_definition_opt in file "src/kernel_services/ast_data/kernel_function.ml", line 534, characters 22-34
  Called from Frama_c_kernel__Kernel_function.var_is_in_scope in file "src/kernel_services/ast_data/kernel_function.ml", line 545, characters 13-61
  Called from Stdlib__List.find_all in file "list.ml", line 265, characters 17-20
  Called from Stdlib__List.find_all in file "list.ml", line 265, characters 31-43
  Called from Frama_c_kernel__Destructors.vis#vstmt_aux.vars_from_blocks.(fun) in file "src/kernel_services/analysis/destructors.ml", line 190, characters 11-70
  Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
  Called from Frama_c_kernel__Destructors.vis#vstmt_aux in file "src/kernel_services/analysis/destructors.ml", line 281, characters 8-74
  Called from Frama_c_kernel__Visitor.internal_generic_frama_c_visitor#vstmt in file "src/kernel_services/visitors/visitor.ml", line 73, characters 16-35
  Called from Frama_c_kernel__Cil.doVisit in file "src/kernel_services/ast_queries/cil.ml", line 779, characters 15-31
  Called from Frama_c_kernel__Cil.visitCilStmt in file "src/kernel_services/ast_queries/cil.ml", lines 1806-1807, characters 4-84
  Called from Stdlib__Fun.protect in file "fun.ml", line 34, characters 8-15
  Re-raised at Stdlib__Fun.protect in file "fun.ml", line 39, characters 6-52
  Called from Frama_c_kernel__Extlib.map_no_copy.aux in file "src/libraries/stdlib/extlib.ml", line 191, characters 15-18
  Called from Frama_c_kernel__Cil.childrenBlock in file "src/kernel_services/ast_queries/cil.ml", line 1989, characters 15-48
  Called from Frama_c_kernel__Cil.doVisit in file "src/kernel_services/ast_queries/cil.ml", line 794, characters 19-39
  Called from Frama_c_kernel__Cil.childrenFunction in file "src/kernel_services/ast_queries/cil.ml", line 2215, characters 13-38
  Called from Frama_c_kernel__Cil.doVisit in file "src/kernel_services/ast_queries/cil.ml", line 794, characters 19-39
  Called from Frama_c_kernel__Cil.visitCilFunction in file "src/kernel_services/ast_queries/cil.ml", lines 2176-2177, characters 4-34
  Called from Frama_c_kernel__Visitor.visitFramacFunction in file "src/kernel_services/visitors/visitor.ml", line 866, characters 11-47
  Called from Frama_c_kernel__Destructors.add_destructor.process_one_global in file "src/kernel_services/analysis/destructors.ml", line 293, characters 13-57
  Called from Stdlib__Fun.protect in file "fun.ml", line 34, characters 8-15
  Re-raised at Stdlib__Fun.protect in file "fun.ml", line 39, characters 6-52
  Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
  Called from Frama_c_kernel__Cil.foldGlobals in file "src/kernel_services/ast_queries/cil.ml", line 4090, characters 13-49
  Called from Frama_c_kernel__Destructors.add_destructor in file "src/kernel_services/analysis/destructors.ml", line 298, characters 18-63
  Called from Frama_c_kernel__File.transform_and_check in file "src/kernel_services/ast_queries/file.ml", line 1134, characters 2-7
  Called from Stdlib__Queue.iter.iter in file "queue.ml", line 130, characters 6-15
  Called from Graph__Topological.Make_stable.fold.walk in file "src/topological.ml", line 137, characters 18-25
  Called from Frama_c_kernel__File.prepare_cil_file in file "src/kernel_services/ast_queries/file.ml", line 1240, characters 2-35
  Called from Frama_c_kernel__File.prepare_from_c_files in file "src/kernel_services/ast_queries/file.ml", line 1839, characters 2-22
  Called from Frama_c_kernel__File.init_from_cmdline in file "src/kernel_services/ast_queries/file.ml", line 1915, characters 4-27
  Called from Frama_c_kernel__Ast.force_compute in file "src/kernel_services/ast_data/ast.ml", line 112, characters 2-28
  Called from Frama_c_kernel__Ast.compute in file "src/kernel_services/ast_data/ast.ml", line 120, characters 53-71
  Called from Frama_c_kernel__Boot.play_analysis in file "src/kernel_internals/runtime/boot.ml", line 31, characters 6-20
  Called from Frama_c_kernel__Cmdline.play_in_toplevel_one_shot in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 866, characters 2-9
  Called from Frama_c_kernel__Cmdline.play_in_toplevel in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 896, characters 18-64
  Called from Frama_c_kernel__Cmdline.catch_toplevel_run in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 237, characters 4-8
  
  Unexpected error (File "src/kernel_services/ast_data/kernel_function.ml", line 534, characters 22-28: Assertion failed).

Contextual information

  • Frama-C installation mode: from source
  • Frama-C version: 30.0+dev (Zinc)
  • Plug-in used: none
  • OS name: Manjaro Linux
  • OS version: 6.6.80-1-MANJARO
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information