Commit dcd0fbed authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Update to the latest Monolith.

parent 4bfa1ea3
......@@ -200,7 +200,7 @@ let ordering =
(* [draw length get s] draws an element from the sequence [s]. *)
let draw length get s =
int_ (fun () -> get s (Gen.int (length s) ()))
int_within (fun () -> get s (Gen.int (length s) ()))
let edraw =
draw R.E.length R.E.get
......@@ -224,7 +224,7 @@ let pitindex =
form [jump direction it k]. *)
let itlength length index direction it =
int_ (fun () ->
int_within (fun () ->
let n = length it in
(* Choose the target of the jump. *)
let target = Gen.int (n + 2) () - 1 in
......@@ -328,11 +328,11 @@ let () =
if testing ECreate then
declare "E.create" spec R.E.create C.E.create;
let spec = default ^> int_ length ^> element ^> esek in
let spec = default ^> int_within length ^> element ^> esek in
if testing EMake then
declare "E.make" spec R.E.make C.E.make;
let spec = default ^> int_ length ^> esek in
let spec = default ^> int_within length ^> esek in
if testing EInit then
declare "harness_init E.init" spec
(harness_init R.E.init) (harness_init C.E.init);
......@@ -665,11 +665,11 @@ let () =
if testing PCreate then
declare "P.create" spec R.P.create C.P.create;
let spec = default ^> int_ length ^> element ^> psek in
let spec = default ^> int_within length ^> element ^> psek in
if testing PMake then
declare "P.make" spec R.P.make C.P.make;
let spec = default ^> int_ length ^> psek in
let spec = default ^> int_within length ^> psek in
if testing PInit then
declare "harness_init P.init" spec
(harness_init R.P.init) (harness_init C.P.init);
......
Supports Markdown
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