[kernel] Ill-typed \valid expression in ACSL annotation causes a crash

The following invalid ACSL annotation produces a crash with Frama-C 31.0:

/*@
  requires \valid(a + (0..0));
*/
void foo(int a);

The command line I used: frama-c ./input.c and the backtrace:

Backtrace

[kernel] Parsing input.c (with preprocessing) [kernel] input.c:1: Failure: arithmetic conversion between non arithmetic types int and set<ℤ> [kernel] Current source was: The full backtrace is: Raised at Frama_c_kernel__Log.finally_raise in file "src/kernel_services/plugin_entry_points/log.ml" (inlined), line 549, characters 24-31 Called from Frama_c_kernel__Log.Register.fatal in file "src/kernel_services/plugin_entry_points/log.ml", line 1115, characters 17-55 Called from Frama_c_kernel__Log.logwithfinal.(fun) in file "src/kernel_services/plugin_entry_points/log.ml", line 542, characters 9-23 Re-raised at Frama_c_kernel__Log.logwithfinal.(fun) in file "src/kernel_services/plugin_entry_points/log.ml", line 545, characters 9-16 Called from Frama_c_kernel__Logic_typing.Make.term_node in file "src/kernel_services/ast_queries/logic_typing.ml", line 2853, characters 32-63 Called from Frama_c_kernel__Logic_typing.Make.term in file "src/kernel_services/ast_queries/logic_typing.ml", line 3439, characters 19-62 Called from Frama_c_kernel__Logic_typing.Make.predicate.term_ptr in file "src/kernel_services/ast_queries/logic_typing.ml", line 3450, characters 14-24 Called from Frama_c_kernel__Logic_typing.Make.predicate.predicate_label_ptr in file "src/kernel_services/ast_queries/logic_typing.ml", line 3455, characters 14-40 Called from Frama_c_kernel__Logic_typing.Make.predicate in file "src/kernel_services/ast_queries/logic_typing.ml" (inlined), line 3686, characters 24-55 Called from Frama_c_kernel__Logic_typing.Make.id_predicate_top in file "src/kernel_services/ast_queries/logic_typing.ml", line 3700, characters 36-56 Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 Called from Frama_c_kernel__Logic_typing.Make.type_spec.(fun) in file "src/kernel_services/ast_queries/logic_typing.ml", line 3830, characters 26-60 Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 Called from Frama_c_kernel__Logic_typing.Make.type_spec in file "src/kernel_services/ast_queries/logic_typing.ml", lines 3818-3851, characters 12-21 Called from Frama_c_kernel__Cabs2cil.createGlobal in file "src/kernel_internals/typing/cabs2cil.ml", line 8565, characters 22-62 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__Cabs2cil.createGlobal in file "src/kernel_internals/typing/cabs2cil.ml", lines 8557-8572, characters 16-19 Called from Frama_c_kernel__Cabs2cil.doDecl.doOneDeclarator in file "src/kernel_internals/typing/cabs2cil.ml", line 9025, characters 18-78 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__Cabs2cil.doDecl in file "src/kernel_internals/typing/cabs2cil.ml", line 9042, characters 14-53 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__Cabs2cil.convFile.doOneGlobal in file "src/kernel_internals/typing/cabs2cil.ml", line 10276, characters 12-35 Called from Stdlib__List.iter in file "list.ml", line 112, characters 12-15 Called from Frama_c_kernel__Cabs2cil.convFile in file "src/kernel_internals/typing/cabs2cil.ml", line 10280, characters 2-25 Called from Frama_c_kernel__Frontc.parse.(fun) in file "src/kernel_internals/typing/frontc.ml", line 88, characters 14-36 Called from Frama_c_kernel__File.parse_cabs in file "src/kernel_services/ast_queries/file.ml", line 642, characters 25-44 Called from Frama_c_kernel__File.to_cil_cabs in file "src/kernel_services/ast_queries/file.ml", line 661, characters 12-36 Called from Frama_c_kernel__File.files_to_cabs_cil.(fun) in file "src/kernel_services/ast_queries/file.ml", line 740, characters 46-72 Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 Called from Frama_c_kernel__File.files_to_cabs_cil in file "src/kernel_services/ast_queries/file.ml", line 740, characters 17-89 Called from Frama_c_kernel__File.prepare_from_c_files in file "src/kernel_services/ast_queries/file.ml", line 1842, characters 24-60 Called from Frama_c_kernel__File.init_from_cmdline in file "src/kernel_services/ast_queries/file.ml", line 1919, 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 957, characters 2-9 Called from Frama_c_kernel__Cmdline.play_in_toplevel in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 987, characters 18-64 Called from Frama_c_kernel__Cmdline.catch_toplevel_run in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 238, characters 4-8

Frama-C aborted: internal error. Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues Your Frama-C version is 31.0 (Gallium). Note that a version and a backtrace alone often do not contain enough information to understand the bug. Guidelines for reporting bugs are at: https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs

Notice that `\valid(a)` is correctly rejected by the frontend.