GitLab

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.