Commit 8980fa19 authored by Benedikt Becker's avatar Benedikt Becker

Fix examples/use_api_mlw_tree.ml and bench

parent 67a84b35
......@@ -310,7 +310,7 @@ let mods = Typing.type_mlw_file env [] "myfile.mlw" mlw_file
(* END{typemodules} *)
(* BEGIN{typemoduleserror} *)
let mods =
let _mods =
try
Typing.type_mlw_file env [] "myfile.mlw" mlw_file
with Loc.Located (loc, e) -> (* A located exception [e] *)
......
module M1
use int.Int
use int.Int
goal g: Int.(=) 4 (Int.(+) 2 2)
end
module M2
use int.Int
use int.Int
let f (x: int) requires { x = 6 } ensures { result = 42 } = Int.(*) x 7
let f (x : int)
requires {(x = 6)}
ensures { (result = 42) } =
(Int.(*) x 7)
end
module M3
use int.Int
use ref.Ref
use int.Int
use ref.Ref
let f (_: ())
ensures { Int.(>=) result 0 } =
let x = Ref.ref 42 in (Ref.(!) x)
let f (_ : ())
ensures { (Int.(>=) result 0) } =
(let x = (Ref.ref 42) in Ref.(!) x)
end
module M4
use int.Int
use array.Array
use int.Int
use array.Array
let f (a: Array.array int)
requires { Int.(>=) (Array.length a) 1 }
returns { _ -> ((Array.([]) a 0) = 42) } =
Array.([]<-) a 0 42
let f (a : Array.array int)
requires {(Int.(>=) (Array.length a) 1)}
returns { _ -> (Array.([]) a 0) = 42 } =
(Array.([]<-) a 0 42)
end
Tasks are:
Task 1: theory Task
......
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