Commit 55605308 authored by Francois Bobot's avatar Francois Bobot
Browse files

modification de la cible test et ajout de l'option timeout

parent e9285f76
......@@ -148,8 +148,7 @@ test: bin/why.byte
ocamlrun -bt bin/why.byte --debug -I lib/prelude/ --driver lib/drivers/why3.drv \
--output output_why3 src/test.why
bin/why.byte --driver lib/drivers/alt_ergo.drv -I lib/prelude/ \
--output - --goal Test.G src/test.why > ergo.why
timeout 3 alt-ergo ergo.why
--call --goal Test.G src/test.why --timeout 3
testl: bin/whyl.byte
ocamlrun -bt bin/whyl.byte src/programs/test.mlw
......
......@@ -57,6 +57,7 @@ let () =
Can't be used with --output"; (* Why not? *)
"--driver", Arg.String (fun s -> driver := Some s),
"<file> set the driver file";
"--timeout", Arg.Set_int timeout, "set the timeout used when calling provers (0 unlimited, default 10)";
]
(fun f -> Queue.push f files)
"usage: why [options] files..."
......
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