Commit 97e48ba6 authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Update to new version of Monolith.

parent e4d7f09f
......@@ -123,24 +123,17 @@ let index =
(* -------------------------------------------------------------------------- *)
(* Define [length] as an alias for the concrete type [int]. Equip it with a
generator. This is used by operations such as [make] and [init]. *)
(* A large value of [max_length] leads to slow tests. E.g., changing it from
0x100 to 0x1000 divides by 3 the number of executions per second that the
system is able to perform, from 300/s to 100/s. *)
let max_length =
64
(* Define [length] as a generator that controls the maximum length of the
lists and sequences that we generate. *)
let length =
le max_length
Gen.lt 64
let list spec =
list ~length:max_length spec
list ~length spec
let aseq_element =
declare_affine_seq ~length:max_length element
declare_affine_seq ~length element
(* -------------------------------------------------------------------------- *)
......@@ -179,7 +172,7 @@ let direction =
let element_array =
let next = Gen.sequential() in
let generate = Gen.(array (le max_length) next)
let generate = Gen.(array length next)
and print = Print.(array int) in
ifpol
(constructible_ generate print)
......@@ -335,11 +328,11 @@ let () =
if testing ECreate then
declare "E.create" spec R.E.create C.E.create;
let spec = default ^> length ^> element ^> esek in
let spec = default ^> int_ length ^> element ^> esek in
if testing EMake then
declare "E.make" spec R.E.make C.E.make;
let spec = default ^> length ^> esek in
let spec = default ^> int_ length ^> esek in
if testing EInit then
declare "harness_init E.init" spec
(harness_init R.E.init) (harness_init C.E.init);
......@@ -350,7 +343,7 @@ let () =
if testing EDefault then
declare "E.default" spec (fun _ -> 0) C.E.default;
let spec = esek ^> length in
let spec = esek ^> int in
if testing ELength then
declare "E.length" spec R.E.length C.E.length;
......@@ -672,11 +665,11 @@ let () =
if testing PCreate then
declare "P.create" spec R.P.create C.P.create;
let spec = default ^> length ^> element ^> psek in
let spec = default ^> int_ length ^> element ^> psek in
if testing PMake then
declare "P.make" spec R.P.make C.P.make;
let spec = default ^> length ^> psek in
let spec = default ^> int_ length ^> psek in
if testing PInit then
declare "harness_init P.init" spec
(harness_init R.P.init) (harness_init C.P.init);
......@@ -687,7 +680,7 @@ let () =
if testing PDefault then
declare "P.default" spec (fun _ -> 0) C.P.default;
let spec = psek ^> length in
let spec = psek ^> int in
if testing PLength then
declare "P.length" spec R.P.length C.P.length;
......@@ -1001,7 +994,7 @@ let () =
(* [sequence] can be applied to an invalid iterator. *)
let spec = viter ^> length in
let spec = viter ^> int in
if testing ILength then
declare "E.Iter.length" spec R.E.Iter.length C.E.Iter.length;
......@@ -1134,7 +1127,7 @@ let () =
sequence that is returned by this operation. That said, [sequence]
is so unlikely to be incorrect that it does not seem worth the trouble. *)
let spec = piter ^> length in
let spec = piter ^> int in
if testing ILength then
declare "P.Iter.length" spec R.P.Iter.length C.P.Iter.length;
......
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