Unexpected error when using/typecasting _Bool types
The following code crashed with an unexpected error.
Steps to reproduce the issue
_Bool get_bool(void);
_Bool pass_bool(_Bool b);
_Bool b_flag1, b_flag2;
void main(){
b_flag1 = pass_bool( !(_Bool)get_bool() );
b_flag2 = pass_bool( (_Bool)get_bool() );
}
> frama-c -deps bool_fails.i
Expected behaviour
.
.
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function get_bool:
\result FROM \nothing
[from] Function pass_bool:
\result FROM b
[from] Function main:
b_flag1 FROM \nothing
b_flag2 FROM \nothing
[from] ====== END OF DEPENDENCIES ======
Actual behaviour
[from] Computing for function main
[from] Computing for function get_bool <-main
[from] Done for function get_bool
[from] Computing for function pass_bool <-main
[kernel] Current source was: bool_fails.i:10
The full backtrace is:
Raised at Offsetmap.Make.merge in file "src/kernel_services/abstract_interp/offsetmap.ml", line 945, characters 23-35
Called from Binary_cache.Symmetric_Binary.merge in file "src/libraries/utils/binary_cache.ml", line 275, characters 19-26
Called from Offsetmap.Make.merge in file "src/kernel_services/abstract_interp/offsetmap.ml", line 999, characters 10-57
Called from Binary_cache.Symmetric_Binary.merge in file "src/libraries/utils/binary_cache.ml", line 275, characters 19-26
Called from Offsetmap.Make.join in file "src/kernel_services/abstract_interp/offsetmap.ml", line 1222, characters 15-62
Called from Hptmap.Make.join.decide_both in file "src/libraries/utils/hptmap.ml", line 1195, characters 14-37
Called from Binary_cache.Symmetric_Binary.merge in file "src/libraries/utils/binary_cache.ml", line 275, characters 19-26
Called from Hptmap.Make.generic_merge.merge_branches in file "src/libraries/utils/hptmap.ml", line 1131, characters 17-28
Called from Binary_cache.Symmetric_Binary.merge in file "src/libraries/utils/binary_cache.ml", line 275, characters 19-26
Called from Hptmap.Make.generic_merge.merge_branches in file "src/libraries/utils/hptmap.ml", line 1131, characters 17-28
Called from Binary_cache.Symmetric_Binary.merge in file "src/libraries/utils/binary_cache.ml", line 275, characters 19-26
Called from Lmap.Make_LOffset.join in file "src/kernel_services/abstract_interp/lmap.ml", line 688, characters 41-55
Called from Stdlib__Hashtbl.fold.do_bucket in file "hashtbl.ml", line 211, characters 23-40
Called from Stdlib__Hashtbl.fold in file "hashtbl.ml", line 218, characters 14-35
Re-raised at Stdlib__Hashtbl.fold in file "hashtbl.ml", line 224, characters 4-13
Called from Db.Value.get_initial_state in file "src/kernel_services/plugin_entry_points/db.ml", line 503, characters 10-140
Called from From_compute.Make.compute_using_prototype in file "src/plugins/from/from_compute.ml", line 674, characters 16-45
Called from From_compute.Make.compute_and_return in file "src/plugins/from/from_compute.ml", line 693, characters 11-37
Called from From_compute.Make.compute in file "src/plugins/from/from_compute.ml", line 705, characters 11-34
Called from Functionwise.To_Use.memo.(fun) in file "src/plugins/from/functionwise.ml", line 45, characters 9-26
Called from State_builder.Hashtbl.memo in file "src/libraries/project/state_builder.ml", line 565, characters 17-22
Called from From_compute.Make.Computer.transfer_call.do_on in file "src/plugins/from/from_compute.ml", line 383, characters 27-55
Called from From_compute.Make.Computer.transfer_call in file "src/plugins/from/from_compute.ml", line 444, characters 17-65
Called from From_compute.Make.Computer.transfer_stmt in file "src/plugins/from/from_compute.ml", line 535, characters 36-61
Called from Dataflows.Forward_monotone_generic_storage.do_stmt in file "src/kernel_services/analysis/dataflows.ml", line 515, characters 12-42
Called from Dataflows.Forward_monotone_generic_storage.compute in file "src/kernel_services/analysis/dataflows.ml", line 523, characters 19-30
Called from Dataflows.Forward_monotone_generic_storage in file "src/kernel_services/analysis/dataflows.ml", line 524, characters 5-14
Called from Dataflows.Simple_forward in file "src/kernel_services/analysis/dataflows.ml" (inlined), line 583, characters 10-48
Called from Dataflows.Simple_forward in file "src/kernel_services/analysis/dataflows.ml" (inlined), line 583, characters 10-57
Called from Dataflows.Simple_forward in file "src/kernel_services/analysis/dataflows.ml", line 583, characters 10-60
Called from From_compute.Make.compute_using_cfg.Compute in file "src/plugins/from/from_compute.ml" (inlined), line 634, characters 31-61
Called from From_compute.Make.compute_using_cfg.Compute in file "src/plugins/from/from_compute.ml", line 634, characters 31-75
Called from From_compute.Make.compute_and_return in file "src/plugins/from/from_compute.ml", line 694, characters 11-31
Called from From_compute.Make.compute in file "src/plugins/from/from_compute.ml", line 705, characters 11-34
Called from Functionwise.To_Use.memo.(fun) in file "src/plugins/from/functionwise.ml", line 45, characters 9-26
Called from State_builder.Hashtbl.memo in file "src/libraries/project/state_builder.ml", line 565, characters 17-22
Called from Functionwise.(fun) in file "src/plugins/from/functionwise.ml", line 106, characters 22-38
Called from Stdlib__Queue.iter.iter in file "queue.ml", line 121, characters 6-15
Called from State_builder.apply_once.(fun) in file "src/libraries/project/state_builder.ml", line 998, characters 9-13
Re-raised at State_builder.apply_once.(fun) in file "src/libraries/project/state_builder.ml", line 1006, characters 9-18
Called from From_register.main.(fun) in file "src/plugins/from/from_register.ml", line 151, characters 9-32
Called from From_register.main in file "src/plugins/from/from_register.ml", line 149, characters 4-119
Called from Stdlib__Queue.iter.iter in file "queue.ml", line 121, characters 6-15
Called from Boot.play_analysis in file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from Cmdline.play_in_toplevel_one_shot in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 846, characters 2-9
Called from Cmdline.play_in_toplevel in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 876, characters 18-64
Called from Cmdline.catch_toplevel_run in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 235, characters 4-8
Unexpected error (File "src/kernel_services/abstract_interp/offsetmap.ml", line 945, characters 23-29: Assertion failed).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 25.0-beta (Manganese).
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 installation
- Frama-C version: 25.0-beta (Manganese)
- OS name: Ubuntu (WSL)
Additional information (optional)
There are some modifications that prevent the program from a crash. Some examples are:
- remove the negation in the first call of pass_bool
- remove one of the calls to pass_bool, does not matter which one
- remove the typecast (_Bool) inside the call to pass_bool
- use temporary variables for the return value from get_bool and pass that variables to pass_bool