Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • 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
  • #2555

Closed
Open
Created May 17, 2021 by Karine EM@karineek

Crash in abstract_interp with an unexpected error when the input program has a syntax error.

Steps to reproduce the issue

Expected behaviour

The following program has a syntax error that crashed frama-c instead of returning an alarm. E.g., gcc returns the following compile-time error:

user42@srg08:~/directed-compiler-fuzzing-code/scripts/9-reduce-bugs/Frama-C-zone$ gcc -w 0bd2a2aa5631e87ab09386dc82e092f5aab23f0e.c
0bd2a2aa5631e87ab09386dc82e092f5aab23f0e.c:10:11: error: negative width in bit-field ‘b’
   10 |   int32_t b:(-19);
      |

Actual behaviour

The following code crashed frama-c:

user42@srg08:~/directed-compiler-fuzzing-code/scripts/9-reduce-bugs/Frama-C-zone$ more 0bd2a2aa5631e87ab09386dc82e092f5aab23f0e.c
#if __SIZEOF_INT__ < 4
  __extension__ typedef __INT32_TYPE__ int32_t;
#else
  typedef int int32_t;
#endif
#pragma pack(1)
struct S
{
  int32_t b:(-19);
} i;
int main ()
{
  return (-1);
}

with the following error:

user42@srg08:~/directed-compiler-fuzzing-code/scripts/9-reduce-bugs/Frama-C-zone$ frama-c -eva 0bd2a2aa5631e87ab09386dc82e092f5aab23f0e.c
[kernel] Parsing 0bd2a2aa5631e87ab09386dc82e092f5aab23f0e.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[kernel] Current source was: 0bd2a2aa5631e87ab09386dc82e092f5aab23f0e.c:11
  The full backtrace is:
  Raised at file "src/kernel_services/abstract_interp/base.ml", line 217, characters 2-27
  Called from file "src/kernel_services/abstract_interp/base.ml", line 480, characters 17-43
  Called from file "src/libraries/project/state_builder.ml", line 565, characters 17-22
  Called from file "src/plugins/value/domains/cvalue/cvalue_domain.ml", line 394, characters 15-38
  Called from file "list.ml", line 121, characters 24-34
  Called from file "src/plugins/value/domains/cvalue/cvalue_domain.ml", line 405, characters 4-34
  Called from file "src/plugins/value/engine/initialization.ml", line 309, characters 16-68
  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 (File "src/kernel_services/abstract_interp/base.ml", line 217, characters 2-8: Assertion failed).
  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 reduced the program manually, I can also share the original code or other examples.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking