check_nocontinue

[andrew-appel]

There is a bug in Ltac check_nocontinue in floyd/forward.v. When doing forward_loop in a context of an Sfor with a defined postcondition, we get the error message "Tactic failure: applied forward_loop to something that is not a loop (level 99)." However, this should work.

To replicate this bug, use progs/Verif_sumarray2.v, replacing body_sumarray with the following.

Lemma body_sumarray: semax_body Vprog Gprog f_sumarray sumarray_spec.
Proof.
start_function. 
forward.  (* s = 0; *)

apply semax_seq with   (PROP ( )
   LOCAL (temp _a a;
   temp _n (Vint (Int.repr size));
   temp _s (Vint (Int.repr (sum_Z contents))))
   SEP (data_at sh (tarray tuint size)
          (map Vint (map Int.repr contents)) a)).

forward_loop (EX i: Z,
   PROP  (0 <= i <= size)
   LOCAL (temp _a a;
          temp _i (Vint (Int.repr i));
          temp _n (Vint (Int.repr size));
          temp _s (Vint (Int.repr (sum_Z (sublist 0 i contents)))))
   SEP   (data_at sh (tarray tuint size) (map Vint (map Int.repr contents)) a))%assert.

[andrew-appel]

P.R. #554 fixes this, not by changing check_nocontinue, but by adding a case to Tactic Notation forward_loop.