GitLab

Steps to reproduce the issue

Here is a (not necessarily) minimal example (see excludes.c):

void excludes8(_Bool x1, _Bool x2, _Bool x3, _Bool x4,
               _Bool x5, _Bool x6, _Bool x7, _Bool x8,
               _Bool *excludes)
{
  *excludes =
    (!x1 && !x2 && !x3 && !x4 && !x5 && !x6 && !x7 && !x8) ||
    ( x1 && !x2 && !x3 && !x4 && !x5 && !x6 && !x7 && !x8) ||
    (!x1 &&  x2 && !x3 && !x4 && !x5 && !x6 && !x7 && !x8) ||
    (!x1 && !x2 &&  x3 && !x4 && !x5 && !x6 && !x7 && !x8) ||
    (!x1 && !x2 && !x3 &&  x4 && !x5 && !x6 && !x7 && !x8) ||
    (!x1 && !x2 && !x3 && !x4 &&  x5 && !x6 && !x7 && !x8) ||
    (!x1 && !x2 && !x3 && !x4 && !x5 &&  x6 && !x7 && !x8) ||
    (!x1 && !x2 && !x3 && !x4 && !x5 && !x6 &&  x7 && !x8) ||
    (!x1 && !x2 && !x3 && !x4 && !x5 && !x6 && !x7 && x8);
  //@ assert *excludes == 1;
  return;
}

Launch Frama-C / WP: frama-c -wp excludes.c

Expected behaviour

The (silly) assertion should be tried by the solvers.

Actual behaviour

Out of memory crash (on a 16G laptop):

[kernel] Parsing FIREFLY_1.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled

'frama-c -wp FIREFLY_1.c' terminated by signal SIGKILL 

Contextual information

• Frama-C installation mode: opam
• Frama-C version: 24.0 (Chromium)
• Plug-in used: WP
• OS name: Ubuntu
• OS version: 20.04.4 LTS
• Memory: 15605 MiB

Additional information (optional)

I tried to profile the execution by using Memtrace on a local installation of Frama-C. It seems that WP is filling huge identifiers tables (Intmap, Idxmap) when executing code from Conditions module. Here is the corresponding trace, that can be viewed using Memtrace_viewer: trace.ctf