From cedb1b63e3dbc64de9384579544a55f0a0a605b1 Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Thu, 31 Mar 2022 15:14:01 +0200
Subject: [PATCH] [SAVer] Reworked tests.
---
ovo.opam | 5 +++--
src/verification.ml | 2 +-
tests/dune | 1 +
tests/simple_ovo.t | 14 ++++++--------
tests/test_data.csv | 2 ++
5 files changed, 13 insertions(+), 11 deletions(-)
create mode 100644 tests/test_data.csv
diff --git a/ovo.opam b/ovo.opam
index 6adaf24e..443011ba 100644
--- a/ovo.opam
+++ b/ovo.opam
@@ -9,7 +9,7 @@ depends: [
"odoc" {with-doc}
]
build: [
- ["dune" "subst"] {dev}
+ ["dune" "subst" "--root" "."] {dev}
[
"dune"
"build"
@@ -17,7 +17,8 @@ build: [
name
"-j"
jobs
- "--promote-install-files=false"
+ "--promote-install-files"
+ "false"
"@install"
"@runtest" {with-test}
"@doc" {with-doc}
diff --git a/src/verification.ml b/src/verification.ml
index 2c5f03ec..c16475ab 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -138,7 +138,7 @@ let call_prover ~limit config (prover : Why3.Whyconf.config_prover) driver env
= Int.of_string (Re__Core.Group.get g 2)
then Call_provers.Valid
else Call_provers.Invalid
- | None -> assert false
+ | None -> Call_provers.HighFailure
(* Any other answer than HighFailure should
* never happen as we do not define
* anything in SAVer's driver *))
diff --git a/tests/dune b/tests/dune
index f4fdcc24..663a7daf 100644
--- a/tests/dune
+++ b/tests/dune
@@ -4,6 +4,7 @@
TestNetwork.nnet
TestNetworkONNX.onnx
TestSVM.ovo
+ test_data.csv
bin/pyrat.py
bin/Marabou
bin/saver
diff --git a/tests/simple_ovo.t b/tests/simple_ovo.t
index 97fc618d..ad3aaafb 100644
--- a/tests/simple_ovo.t
+++ b/tests/simple_ovo.t
@@ -20,16 +20,15 @@ Test verify
$ PATH=$(pwd)/bin:$PATH
- $ caisar verify -L . --format whyml --prover=PyRAT - 2>&1 <<EOF | sed 's/\/tmp\/[a-z0-9./]*/$TMPFILE/'
+ $ caisar verify -L . --format whyml --prover=SAVer --dataset-csv=test_data.csv - 2>&1 <<EOF | sed 's/\/tmp\/[a-z0-9./]*/$TMPFILE/'
> theory T
- > use TestSVM.AsArray
+ > use TestSVM.SVM
> use ieee_float.Float64
> use caisar.IOShape
+ > use caisar.SVM
>
- > goal G: forall x1 x2 x3.
- > (0.0:t) .< x1 .< (0.5:t) ->
- > let (y1,_) = svm_apply x1 x2 x3 in
- > (0.0:t) .< y1 .< (0.5:t)
+ > goal G: forall a : input_type.
+ > robust_to SVM.svm_apply a (8.0:t)
> end
> EOF
<autodetect>0 prover(s) added
@@ -43,5 +42,4 @@ Test verify
<autodetect>Found prover PyRAT version 1.1, OK.
<autodetect>Found prover SAVer version v1.0, OK.
<autodetect>4 prover(s) added
- Goal G: Unknown
- ()
+ Goal G: High failure
diff --git a/tests/test_data.csv b/tests/test_data.csv
new file mode 100644
index 00000000..a48580a3
--- /dev/null
+++ b/tests/test_data.csv
@@ -0,0 +1,2 @@
+# 1 3
+1,0.5,0.5,0.0,
--
GitLab