[WP] region plugin division by 0 with empty region node
Steps to reproduce the issue
void error_array() {
int a[3];
int *p = &(a[1]);
}
void error_struct() {
struct { int f; char g; } y;
int *p = &y.f;
}
Expected behaviour
No division by 0. Try to fix it using sizeof
region Blob equal to 1.
Actual behaviour
$ frama-c -region file.c
[server] Socket server running.
[server] Server enabled.
[kernel] Parsing file.c (with preprocessing)
[region] Analyzing regions
[kernel] Current source was: :0
The full backtrace is:
Raised at Region__Memory.make_range in file "src/plugins/region/memory.ml", line 260, characters 10-52
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Region__Memory.make_region in file "src/plugins/region/memory.ml", line 274, characters 11-54
Called from Region__Memory.walk in file "src/plugins/region/memory.ml", line 286, characters 6-25
Called from Stdlib__Map.Make.iter in file "map.ml", line 297, characters 20-25
Called from Stdlib__Map.Make.iter in file "map.ml", line 297, characters 10-18
Called from Stdlib__Format.output_acc in file "format.ml", line 1295, characters 4-20
Called from Stdlib__Format.output_acc in file "format.ml", line 1295, characters 4-20
Called from Stdlib__Format.kfprintf.(fun) in file "format.ml", line 1356, characters 16-34
Called from Region__Analysis.get in file "src/plugins/region/analysis.ml", line 59, characters 4-263
Called from Region__Analysis.compute in file "src/plugins/region/analysis.ml", line 70, characters 27-33
Called from Stdlib__Map.Make.iter in file "map.ml", line 297, characters 20-25
Called from Stdlib__Queue.iter.iter in file "queue.ml", line 121, characters 6-15
Called from Frama_c_kernel__Boot.play_analysis in file "src/kernel_internals/runtime/boot.ml", line 38, characters 4-17
Called from Frama_c_kernel__Cmdline.play_in_toplevel_one_shot in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 837, characters 2-9
Called from Frama_c_kernel__Cmdline.play_in_toplevel.aux in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 852, characters 30-76
Called from Frama_c_kernel__Cmdline.catch_toplevel_run in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 231, characters 4-8
Unexpected error (Division_by_zero).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 29.0+dev (Copper).
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
[server] Server disabled.
[frama-c] exit 125
Contextual information
- Frama-C installation mode: from source
- Frama-C version: 29.0+dev (Copper)
- Plug-in used: region
- OS name: Fedora
- OS version: 40
Edited by Jérémy Damour