GitLab

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.