Commit 11235736 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remove obsolete test targets.

parent 15c3c97f
......@@ -1407,41 +1407,6 @@ bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS) \
# test targets
###############
test2: bin/why3.byte $(TOOLS)
bin/why3.byte tests/test-jcf.why
test: bin/why3.byte plugins.byte $(TOOLS)
mkdir -p output_why3
bin/why3.byte -D drivers/why3.drv -o output_why3 tests/test-jcf.why
# bin/why3.byte -D drivers/alt_ergo.drv tests/test-jcf.why -T Test -G G
# bin/why3.byte -P alt-ergo --timelimit 3 tests/test-jcf.why -T Test -G G
# bin/why3.byte -D drivers/coq.drv tests/test-jcf.why -T Test -G G
echo bin/why3.byte -P alt-ergo --timelimit 1 --prove theories/real.why
@printf "*** Checking Coq file generation ***\\n"
@mkdir -p output_coq
@for i in int.Abs int.EuclideanDivision int.ComputerDivision \
real.Abs real.FromIntTest real.SquareTest \
real.ExpLogTest real.PowerTest real.TrigonometryTest \
floating_point.Test map.TestBv32 \
; do \
printf "Generating Coq file for $$i\\n" && \
bin/why3.byte -P coq -o output_coq -T $$i ; done
@printf "*** Checking Coq compilation ***\\n"
@for i in output_coq/*.v; do printf "coq $$i\\n" && coqc $$i ; done
testl: bin/why3.byte
ocamlrun -bt bin/why3.byte tests/test-pgm-jcf.mlw
ocamlrun -bt bin/why3.byte -P alt-ergo tests/test-pgm-jcf.mlw
testl-debug: bin/why3.opt
bin/why3.opt --debug program_typing tests/test-pgm-jcf.mlw
testl-ide: bin/why3ide.opt
bin/why3ide.opt tests/test-pgm-jcf.mlw
testl-type: bin/why3.byte
ocamlrun -bt bin/why3.byte --type-only tests/test-pgm-jcf.mlw
test-api-logic.byte: examples/use_api/logic.ml lib/why3/why3.cma
$(if $(QUIET),@echo 'Ocaml $<' &&) \
ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< > /dev/null \
......
theory T
use import int.Int
goal G: exists x: int. 1+3 > 2
end
(*
Local Variables:
compile-command: "make -C .. tests/test-jcf.gui"
End:
*)
module TestAbstr
use import int.Int
use import ref.Ref
exception E1 int
exception E2 int
let test (r : ref int) (z : int)
ensures { !r = 3 /\ result > 0 }
raises { E1 x -> !r = 1 /\ x < 0 }
raises { E2 x -> !r = 3 /\ x = 0 }
=
r := 1;
abstract begin
if z < 0 then raise (E1 z);
r := !r + 2;
if z = 0 then raise (E2 z)
end
ensures { !r = 3 }
raises { E1 x -> x = 5 };
if z = 42 then 41 else z
end
module M1
predicate eq (x y : 'a)
end
module M2
predicate my_eq (x : 'a) (y : 'a) = my_eq1 x y
with my_eq1 (x : 'a) (y : 'a) = my_eq2 x y
with my_eq2 (x : 'a) (y : 'a) = my_eq3 x y
with my_eq3 (x : 'a) (y : 'a) = my_eq4 x y
with my_eq4 (x : 'a) (y : 'a) = my_eq5 x y
with my_eq5 (x : 'a) (y : 'a) = my_eq6 x y
with my_eq6 (x : 'a) (y : 'a) = my_eq7 x y
with my_eq7 (x : 'a) (y : 'a) = my_eq8 x y
with my_eq8 (x : 'a) (y : 'a) = my_eq9 x y
with my_eq9 (x : 'a) (y : 'a) = x = y
clone M1 with predicate eq = my_eq
end
module TestGhost
use import int.Int
use import ref.Ref
use import M2
let peq x y = let _ = my_eq x (y : ~'c) in y
let test1 (x: int) =
assert { x > 0 };
let r1 = ref x in
peq r1 r1
end
(*
Local Variables:
compile-command: "unset LANG; make -C .. testl-ide"
End:
*)
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