srev-inplace.v

(Prog [
(Func "swap" ("a" :: "i" :: "j" :: nil)
  (Sseq 
  (Sset "tmp" (Eidx (Evar "a") (Evar "i")))
  (Sseq 
  (Swrite "a" (Evar "i") (Eidx (Evar "a") (Evar "j")))
  (Swrite "a" (Evar "j") (Evar "tmp"))))
  (Evar "a"));
(Func "reverse" ("a" :: nil)
  (Sseq 
  (Sset "i" (Eval (Vint 0)))
  (Swhile (Eop2 Ole (Evar "i") (Eop2 Osub (Eop2 Osub (Elen (Evar "a")) (Eval (Vint 1))) (Evar "i"))) 
    (Sseq 
    (Scall "_" "swap" ((Evar "a") :: (Evar "i") :: (Eop2 Osub (Eop2 Osub (Elen (Evar "a")) (Eval (Vint 1))) (Evar "i")) :: nil))
    (Sset "i" (Eop2 Oadd (Evar "i") (Eval (Vint 1)))))))
  (Evar "a"))]
(Sseq 
(Scall "a" "read_str" (nil))
(Scall "result" "reverse" ((Evar "a") :: nil)))
(Evar "result"))