Frama-c crash with Cil.SizeOfError sizeof(void)
This issue looks like a similar one to #263 (closed), which was closed because it is related to jessie plug-in. The example here gives an error message that is almost the same as the one reported in bug 263 but with eva plug-in. Since I am getting this error quite a lot, I was thinking it is important to report.
Steps to reproduce the issue
frama-c -eva test.c
Expected behaviour
Not to crash frama-c.
Actual behaviour
Frama-c crashed with this error trace:
[kernel] Parsing test.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
[kernel] Current source was: test.c:5
The full backtrace is:
Raised at file "src/kernel_services/ast_queries/cil.ml", line 4038, characters 22-72
Called from file "src/kernel_services/ast_queries/cil.ml", line 4533, characters 42-58
Called from file "src/kernel_services/ast_queries/cil.ml", line 4793, characters 8-29
Called from file "src/plugins/value/engine/evaluation.ml", line 917, characters 12-35
Called from file "src/plugins/value/engine/evaluation.ml", line 864, characters 6-40
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 907, characters 6-33
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 1103, characters 6-36
Called from file "src/plugins/value/engine/evaluation.ml" (inlined), line 1148, characters 4-67
Called from file "src/plugins/value/engine/evaluation.ml", line 1509, characters 23-77
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 157, characters 14-59
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 177, characters 4-54
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 526, characters 6-65
Called from file "src/plugins/value/eval.ml", line 48, characters 29-32
Called from file "list.ml", line 126, characters 16-37
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 564, characters 4-68
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 752, characters 29-72
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 769, characters 24-59
Called from file "src/kernel_services/abstract_interp/bottom.ml" (inlined), line 31, characters 18-21
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 742, characters 6-1023
Called from file "src/plugins/value/engine/iterator.ml", line 274, characters 6-47
Called from file "src/plugins/value/partitioning/partition.ml", line 494, characters 29-34
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/iterator.ml", line 430, characters 15-71
Called from file "src/plugins/value/engine/iterator.ml", line 494, characters 18-35
Called from file "list.ml", line 92, characters 20-23
Called from file "src/plugins/value/engine/iterator.ml", line 496, characters 18-60
Called from file "src/plugins/value/engine/iterator.ml", line 543, characters 13-31
Called from file "list.ml", line 110, characters 12-15
Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 540, characters 4-31
Called from file "src/plugins/value/engine/iterator.ml", line 602, characters 6-22
Called from file "src/plugins/value/engine/iterator.ml", line 769, characters 20-39
Called from file "src/plugins/value/engine/compute_functions.ml", line 201, characters 8-45
Called from file "src/plugins/value/engine/compute_functions.ml", line 333, characters 25-75
Called from file "src/libraries/project/state_builder.ml", line 994, characters 9-13
Re-raised at file "src/libraries/project/state_builder.ml", line 1002, characters 9-18
Called from file "src/plugins/value/register.ml", line 39, characters 46-66
Called from file "queue.ml", line 121, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 842, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 872, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 231, characters 4-8
Unexpected error (Cil.SizeOfError("Undefined sizeof(void).", _)).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 22.0 (Titanium).
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
Contextual information
- Frama-C installation mode: Opam
- Frama-C version: Frama-C version is 21.0 (Scandium) and Frama-C version is 22.0 (Titanium)
- Plug-in used: eva
- OS name: Ubuntu
- OS version: 18
Additional information (optional)
I reduced the program that crashed Frama-c into this: (via Creduce)
void a(char *b, int align) {}
#define c(d) #d
#define f() c()
#define a(e) a(f(), __alignof__(e))
int main() { a(void); return 0; }