Unexpected error "Z.shift_left" with invalid_argument with -eva option when the code had syntax errors
Steps to reproduce the issue
frama-c -eva 1cb6e7577d2fe06f3a0e71a0f8bf2af3d964c6f9_copy1.c
Expected behaviour
When an error-containing program is fed into Frama-C, the expected behaviour should be of it giving an appropriate message instead of a crash (an alarm).
Actual behaviour
The following code:
typedef enum bfd_boolean {false, true} boolean;
typedef unsigned long long bfd_size_type;
typedef unsigned int flagword;
typedef unsigned long long CORE_ADDR;
typedef unsigned long long bfd_vma;
struct bfd_struct {
int x;
};
struct asection_struct {
unsigned int user_set_vma : (-2);
bfd_vma vma;
bfd_vma lma;
unsigned int alignment_power;
unsigned int entsize;
};
typedef struct bfd_struct bfd;
typedef struct asection_struct asection;
static bfd *
bfd_openw_with_cleanup (char *filename, const char *target, char *mode)
{
static bfd foo_bfd = { (-1) };
return &foo_bfd;
}
static asection *
bfd_make_section_anyway (bfd *abfd, const char *name)
{
static asection foo_section = { false, (0), (0), (-1) };
return &foo_section;
}
static boolean
bfd_set_section_size (bfd *abfd, asection *sec, bfd_size_type val)
{
return true;
}
static char hello[] = "hello";
int main(void)
{
}
gives the following trace:
The full backtrace is:
Raised by primitive operation at file "src/libraries/stdlib/integer.ml", line 30, characters 2-22
Called from file "src/kernel_services/abstract_interp/int_val.ml", line 552, characters 14-39
Called from file "src/kernel_services/abstract_interp/int_val.ml", line 566, characters 10-59
Called from file "src/kernel_services/abstract_interp/ival.ml", line 521, 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 908, 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 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 251, characters 10-55
Called from file "src/plugins/value/engine/initialization.ml", line 130, 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/kernel_services/ast_data/globals.ml" (inlined), line 128, characters 33-72
Called from file "src/plugins/value/engine/initialization.ml", line 324, characters 15-65
Called from file "src/libraries/project/state_builder.ml", line 403, characters 17-21
Called from file "src/plugins/value/engine/initialization.ml", line 396, characters 20-43
Called from file "src/plugins/value/engine/compute_functions.ml", line 357, characters 10-55
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 (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 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 (as reported by
frama-c -version
) 22.0 (Titanium) - Plug-in used: -eva
- OS name: Ubuntu
- OS version: 18
Additional information (optional)
I see that there is a similar bug reported 5 years ago (#499 (closed)) which has been marked as fixed but with -wp option instead of -eva. But evidently, we still receive this crash with the given message. I reduced this program manually so that the program is small enough for this bug report. I can provide the original code if required.