Crash when size of field is zero with Unexpected error (Invalid_argument("Z.shift_left: count argument must be positive")).
Steps to reproduce the issue
frama-c -eva 5523daed847ab69918007c2c696bec546984c2d8.c
will get the crash:
Unexpected error (Invalid_argument("Z.shift_left: count argument must be positive")).
Expected behaviour
Return a user error for line 3.
Actual behaviour
With this code and eva:
struct __attribute__((packed)) S
{
int s : (0);
};
void main () {
struct S e[] = {0};
}
we get this crash:
[kernel] Parsing 5523daed847ab69918007c2c696bec546984c2d8.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: 5523daed847ab69918007c2c696bec546984c2d8.c:6
The full backtrace is:
Raised by primitive operation at file "z.ml", line 180, characters 4-20
Called from file "src/libraries/stdlib/integer.ml" (inlined), line 30, characters 2-22
Called from file "src/kernel_services/abstract_interp/int_val.ml", line 549, characters 14-45
Called from file "src/kernel_services/abstract_interp/int_val.ml", line 566, characters 10-63
Called from file "src/kernel_services/abstract_interp/ival.ml", line 525, characters 24-65
Called from file "src/plugins/value_types/cvalue.ml", line 427, characters 23-57
Called from file "src/plugins/value/engine/evaluation.ml", line 700, characters 18-50
Called from file "src/plugins/value/engine/evaluation.ml", line 747, characters 10-57
Called from file "src/plugins/value/engine/evaluation.ml", line 917, characters 14-39
Called from file "src/plugins/value/eval.ml", line 48, characters 29-32
Called from file "src/plugins/value/engine/evaluation.ml", line 845, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 810, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 1118, characters 6-36
Called from file "src/plugins/value/engine/evaluation.ml" (inlined), line 1166, characters 4-67
Called from file "src/plugins/value/engine/evaluation.ml", line 1527, characters 23-77
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 164, characters 14-59
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 184, characters 4-54
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 258, characters 10-55
Called from file "src/plugins/value/engine/initialization.ml", line 131, characters 10-48
Called from file "list.ml", line 121, characters 24-34
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/initialization.ml", line 304, characters 8-95
Called from file "src/plugins/value/engine/iterator.ml", line 234, characters 33-36
Called from file "src/plugins/value/partitioning/partition.ml", line 649, characters 29-42
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/iterator.ml", line 436, characters 15-74
Called from file "src/plugins/value/engine/iterator.ml", line 501, characters 18-35
Called from file "list.ml", line 92, characters 20-23
Called from file "src/plugins/value/engine/iterator.ml", line 503, characters 18-60
Called from file "src/plugins/value/engine/iterator.ml", line 550, characters 13-31
Called from file "list.ml", line 110, characters 12-15
Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 547, characters 4-31
Called from file "src/plugins/value/engine/iterator.ml", line 609, characters 6-22
Called from file "src/plugins/value/engine/iterator.ml", line 776, characters 20-39
Called from file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from file "src/plugins/value/engine/compute_functions.ml", line 206, characters 8-45
Called from file "src/plugins/value/engine/compute_functions.ml", line 344, characters 8-63
Called from file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from file "src/plugins/value/engine/analysis.ml", line 181, characters 2-49
Called from file "src/libraries/project/state_builder.ml", line 998, characters 9-13
Re-raised at file "src/libraries/project/state_builder.ml", line 1006, 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 846, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 876, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 235, characters 4-8
Unexpected error (Invalid_argument("Z.shift_left: count argument must be positive")).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 24.0 (Chromium).
Without Eva, we don't get the crash, but we also got no warning, which we should get for line 3.
Contextual information
- Frama-C installation mode: Opam
- Frama-C version: Frama-C version 24.0 (Chromium)
- Plug-in used: Eva
- OS name: Ubuntu
- OS version: 18
Additional information (optional)
Might be related to bug #2556 (closed)