Commit 92eb6f5d authored by Martin Clochard's avatar Martin Clochard

(wip) mini-compiler: fix a ghost + new execution example

parent c1abf46d
......@@ -196,6 +196,9 @@ module Compile_com
let code = Cseq (Cassign x (Anum 1)) lp in
compile_program code
let test2 () : code =
compile_program (Cwhile Btrue Cskip)
end
......
......@@ -93,7 +93,7 @@ module Compiler_logic
(* Code combinator for sequence, with wp. *)
let (%) (s:wp 'a) (exn:pre 'a) : wp 'a
let (%) (s:wp 'a) (ghost exn:pre 'a) : wp 'a
requires { wp_correctness s }
ensures { result.wp = fork_wp s.wp exn }
ensures { result.wcode.length = s.wcode.length /\ wp_correctness result }
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment