[WP] Fails to verify left shift by 2 on range
Steps to reproduce the issue
/*@
requires a == 1;
assigns \nothing;
ensures \result == (a << 2);
*/
unsigned int do_one(const unsigned int a) {
return (a << 2);
}
/*@
requires a == 2;
assigns \nothing;
ensures \result == (a << 2);
*/
unsigned int do_two(const unsigned int a) {
return (a << 2);
}
/*@
requires 1 <= a <= 2;
assigns \nothing;
ensures \result == (a << 2);
*/
unsigned int do_some_shift2(const unsigned int a) {
return (a << 2);
}
/*@
requires 1 <= a <= 2;
assigns \nothing;
ensures \result == (a << 1);
*/
unsigned int do_some_shift1(const unsigned int a) {
return (a << 1);
}
$ frama-c -wp -wp-rte fcshift.c
Expected behaviour
All goals verified successfully.
Actual behaviour
$ frama-c -wp -wp-rte fcshift.c
[kernel] Parsing fcshift.c (with preprocessing)
[rte:annot] annotating function do_one
[rte:annot] annotating function do_some_shift1
[rte:annot] annotating function do_some_shift2
[rte:annot] annotating function do_two
[wp] 8 goals scheduled
[wp] [Alt-Ergo 2.4.1] Goal typed_do_some_shift2_ensures : Timeout (Qed:2ms) (10s)
[wp] Proved goals: 7 / 8
Qed: 6 (0.33ms-0.64ms-2ms)
Alt-Ergo 2.4.1: 1 (10ms) (92) (interrupted: 1)
The ensures goal can be verified when a
has a single value of either 1
or 2
respectively for the do_one
and do_two
functions.
But if a
is 1
or 2
(for function do_some_shift2
), then the ensures goal fails to verify.
Oddly, the goal succeeds if the left shift is by 1
instead of 2
(function do_some_shift1
).
cppreference.com is stating that unsigned int
should always have at least 16 bits, so it is weird to me that changing the amount of the shift is making a difference.
Doubling the timeout to 20 does not make the goal succeed automatically.
Using frama-c-gui
, I know that I can apply tactic Logical Shift
on lsl(a, 2)
in order to make the goal succeed, but a goal that is this specific and simple failing to verify seems like a bug.
Contextual information
- Frama-C installation mode: opam
- Frama-C version: 25.0 (Manganese)
- Plug-in used: WP, RTE, Alt-Ergo 2.4.1
- OS name: Manjaro Linux
- OS version: Sikaris 22.0.0
Additional information (optional)
N/A