Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #2597

Closed
Open
Created Mar 15, 2022 by Lélio Brun@Lelio-Brun

[WP] Out of memory crash

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

Edited Mar 15, 2022 by Lélio Brun
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking