While working with Frama-C I discovered an issue which leads to an unexpected error. The following code snippet shows a minimal reproducer of the problem (simplified as far as possible).
_Bool get_bool(void){ return (_Bool)1; };
_Bool pass_bool(_Bool b){ return b; };
_Bool b_flag1, b_flag2;
int main(){
b_flag1 = pass_bool( !((_Bool) get_bool()) );
b_flag2 = pass_bool( (_Bool) get_bool() );
}
When running Frama-C with frama-c -deps -eva test.c I get the following error (only an excerpt of the error message):
[kernel] Parsing test.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
b_flag1 ∈ {0}
b_flag2 ∈ {0}
[eva] done for function main
[kernel] Current source was: test.c:7
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 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
There are some changes that allow a correct analysis:
.
.
b_flag1 = pass_bool( !((_Bool) get_bool()) );
//b_flag2 = pass_bool( (_Bool) get_bool() );
}
.
.
b_flag1 = pass_bool( ! get_bool() );
b_flag2 = pass_bool( get_bool() );
}
.
.
_Bool b_tmp1 = !((_Bool) get_bool());
_Bool b_tmp2 = (_Bool) get_bool();
b_flag1 = pass_bool( b_tmp1 );
b_flag2 = pass_bool( b_tmp2 );
}
I can not explain this behavior and would be pleased about solutions or hints.
It was a bug and was reported on: https://git.frama-c.com/pub/frama-c/-/issues/2623. It has been solved and works now.