Problems proving trivial things involving shift operators using Frama-C WP

I have this very simple example.

/*@
  requires a >= 0 && a <= 2;
  assigns \nothing;
  ensures \result < 10;
*/
int bob(int a) {
  return 1 << a;
}

When I try to prove this with both Alt-Ergo and z3 it times out

$ frama-c test.c -wp -wp-prover="Alt-Ergo,z3" -wp-status
[kernel] Parsing test.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Timeout] typed_bob_ensures (Qed 1ms) (Alt-Ergo) (Cached)
[wp] [Cache] found:2
[wp] Proved goals:    3 / 4
  Terminating:     1
  Unreachable:     1
  Qed:             1 (0.72ms)
  Timeout:         1
------------------------------------------------------------
  Function bob
------------------------------------------------------------

Goal Post-condition (file test.c, line 110) in 'bob':
Let x = lsl(1, a).
Assume {
  Type: is_sint32(a) /\ is_sint32(x).
  (* Pre-condition *)
  Have: (0 <= a) /\ (a <= 2).
}
Prove: x <= 9.
Prover Alt-Ergo 2.6.2 returns Timeout (Qed:1ms) (2s) (cached)
Prover Z3 4.8.12 returns Timeout (Qed:1ms) (2s) (cached)

------------------------------------------------------------

According to the WP manual there is a shift strategy that should be able to transform lsl(a,k) to a*2^k and with that transformation it feels like this should be automatically provable (Right??)

I have tried defining a strategy with:

/*@
@strategy shift:
  \tactic("Wp.shift");
*/

/*@
  requires a >= 0 && a <= 2;
  assigns \nothing;
  ensures \result < 10;
*/
int bob(int a) {
  return 1 << a;
}


//@proof shift : bob;

And I have tried applying the strategy with the -wp-strategy="shift" flag as well but i has had no effect.

Is there any other explicit thing that I have to do in order to get any of the provers to handle the << operator?

Solution

According to the Wp manual, the shift tactic only applies when its second argument is a constant:

For positive integers, logical shifts such as a << k and a >> k where k is a constant can be interpreted into a multiplication or a division by 2k.

Hence, it won't help you directly. On the other hand, it is possible to interactively apply the range tactic to a (with parameters inf set to 0 and sup to 2 obviously). Then, Wp can complete the proof all by itself.