Crash on subdivided evaluation by inout for an unsatisfiable guard

Thank you for submitting an issue to the Frama-C team. We propose the following template to ease the process. Please directly edit it inline to provide the required information.

Before submitting the issue, please confirm (by adding a X in the [ ]): opam 2.0.5

• the issue has not yet been reported on Gitlab;
• the issue has not yet been reported on our old BTS (note: the old BTS is deprecated);
• you installed Frama-C as prescribed in the instructions.

Contextual information

• Frama-C installation mode: Opam, Homebrew, package from distribution, from source, ... (for Ubuntu 20+21.1 (Scandium)): Opam 2.0.5, why3 1.3.3
• Frama-C version: Frama-C version (as reported by frama-c -version): I tried two versions 20.0 and 21.1
• Plug-in used: -eva -eva-precision 5
• OS name: Ubuntu (64 bit)
• OS version: tried two versions Ubuntu LTS 18 and 20 (LTS 18 I ran with Frama-c 20.0 and LTS 20 I ran with Frama-c 21.1) in Oracle virtual box

Please add specific information deemed relevant with regard to this issue. I got this error: Unexpected error (File "src/plugins/value/engine/subdivided_evaluation.ml", line 238, characters 39-45: Assertion failed).

I have several programs that produce this crash. One of them is this:

#include <stdint.h>
struct {
  uint32_t a;
} b, c;
int32_t *d[][4][8] = {&b};
uint16_t e() {
  for (;; c.a++) {
    uint8_t f = 6;
    d[0][c.a][c.a] == 0 && f;
  }
}
void main() { e(); }

Steps to reproduce the issue

frama-c -eva -slevel 100 -plevel 255 -eva-precision 5 -val-warn-undefined-pointer-comparison pointer -no-val-alloc-returns-null -warn-signed-overflow -warn-unsigned-overflow -val -no-val-show-progress -machdep x86_64 reduce_5.c

Please indicate here steps to follow to get a minimal, complete, and verifiable example which reproduces the issue. It is enough to run eva only: frama-c -eva -eva-precision 5 reduce_5.c

Expected behaviour

Not to crash

Please explain here what is the expected behaviour.

Actual behaviour

In Frama-c 20.0:

The full backtrace is:

  Raised at file "src/plugins/value/engine/subdivided_evaluation.ml", line 238, characters 39-51
  Called from file "src/plugins/value/engine/subdivided_evaluation.ml", line 461, characters 16-67
  Called from file "src/plugins/value/engine/subdivided_evaluation.ml", line 476, characters 11-22
  Called from file "list.ml", line 121, characters 24-34
  Called from file "src/plugins/value/engine/subdivided_evaluation.ml", line 622, characters 21-74
.
.
.  
  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 792, characters 2-9
  Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 822, characters 18-64
  Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 229, characters 4-8

  Unexpected error (File "src/plugins/value/engine/subdivided_evaluation.ml", line 238, characters 39-45: Assertion failed).
  Please report as 'crash' at http://bts.frama-c.com/.
  Your Frama-C version is 20.0 (Calcium).
  Note that a version and a backtrace alone often do not contain enough
  information to understand the bug. Guidelines for reporting bugs are at:
  http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines

In Frama-c 21.1:

  The full backtrace is:
  Raised at file "src/plugins/value/engine/subdivided_evaluation.ml", line 234, characters 39-51
  Called from file "src/plugins/value/engine/subdivided_evaluation.ml", line 455, characters 16-67
  Called from file "src/plugins/value/engine/subdivided_evaluation.ml", line 470, characters 11-22
  Called from file "list.ml", line 121, characters 24-34
  Called from file "src/plugins/value/engine/subdivided_evaluation.ml", line 618, characters 23-76
.
.
.
  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 803, characters 2-9
  Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 833, characters 18-64
  Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 229, characters 4-8
 
  Unexpected error (File "src/plugins/value/engine/subdivided_evaluation.ml", line 234, characters 39-45: Assertion failed).
  Please report as 'crash' at http://bts.frama-c.com/.
  Your Frama-C version is 21.1 (Scandium).
  Note that a version and a backtrace alone often do not contain enough
  information to understand the bug. Guidelines for reporting bugs are at:
  http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines

Please explain here what is the actual (faulty) behaviour.

Fix ideas

None.

Please tell us if you already tried some work-arounds or have some ideas to solve this issue. I don't have any.

changed the description

changed the description

Thank you for your report.

Here is a minimalized case :

int a;
int *d[4][4] = { &a };

void main(void) {
  int i = 0;
  while (1) {
    if (d[i][i] == 0) {}
    i++;
  }
}

From the backtrace, it seems to come from a subdivided evaluation on a bottom state, requested by the inout plugin during the Eva analysis. We will take a closer look.

changed title from Crash when using for loop (;;) to Crash on subdivided evaluation by inout for an unsatisfiable guard

assigned to @buhler

added eva label

Thanks for the report.

As said by @perrelle, the crash is due to the subdivision of evaluations, which is designed to gain precision on expressions containing several occurrences of the same variable (c.a in your example). Specifically, the crash happens on integer or floating-point expressions (here, d[0][c.a][c.a] == 0 && f) where the subdivision is performed on a pointer expression (here, d[0][c.a][c.a] ).

We will publish a patch fixing this crash soon. In the meantime, you can disable subdivisions with option -eva-subdivide-non-linear 0, to prevent the crash from happening. (Subdivisions are disabled by default, but enabled by the meta option -eva-precision.)