From 3abd997c58b7abb8a69da136e7833d9ab6820bb2 Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Wed, 31 May 2023 17:17:12 +0200
Subject: [PATCH] [tests] Added test oracles to verify-json unit test.
---
src/verification.ml | 1 -
tests/verify_json.t | 75 ++++++++++++++++++++++++++++++++++++++++++++-
2 files changed, 74 insertions(+), 2 deletions(-)
diff --git a/src/verification.ml b/src/verification.ml
index 08552fb..776b1ca 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -180,7 +180,6 @@ let combine_prover_answers answers =
| Call_provers.Valid, r | r, Call_provers.Valid -> r
| _ -> acc)
-(* TODO: does printing the task means printing the csv here?*)
let answer_dataset limit config env prover config_prover driver dataset task =
let dataset_predicate =
let on_model ls =
diff --git a/tests/verify_json.t b/tests/verify_json.t
index b625f98..b4493fe 100644
--- a/tests/verify_json.t
+++ b/tests/verify_json.t
@@ -14,5 +14,78 @@ Test verify-json
$ PATH=$(pwd)/bin:$PATH
- $ caisar verify-json config.json 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify-json config.json --verbosity=info 2>&1 <<EOF | ./filter_tmpdir.sh
+ [caisar][INFO] Specification to verify:
+ ;;; produced by PyRAT/VNN-LIB driver
+ ;;; produced by VNN-LIB driver
+ ;; X_0
+ (declare-const X_0 Real)
+
+ ;; X_1
+ (declare-const X_1 Real)
+
+ ;; X_2
+ (declare-const X_2 Real)
+
+ ;; X_3
+ (declare-const X_3 Real)
+
+ ;; X_4
+ (declare-const X_4 Real)
+
+ ;; Y_0
+ (declare-const Y_0 Real)
+
+ ;; Y_1
+ (declare-const Y_1 Real)
+
+ ;; Y_2
+ (declare-const Y_2 Real)
+
+ ;; Y_3
+ (declare-const Y_3 Real)
+
+ ;; Y_4
+ (declare-const Y_4 Real)
+
+ ;; axiom_ge_x0
+ (assert (>= X_0 0.0))
+
+ ;; axiom_le_x0
+ (assert (<= X_0 0.299999999999999988897769753748434595763683319091796875))
+
+ ;; axiom_ge_x1
+ (assert (>= X_1 0.6999999999999999555910790149937383830547332763671875))
+
+ ;; axiom_le_x1
+ (assert (<= X_1 1.0))
+
+ ;; axiom_ge_x2
+ (assert (>= X_2 0.484313724999999972720132745962473563849925994873046875))
+
+ ;; axiom_le_x2
+ (assert (<= X_2 1.0))
+
+ ;; axiom_ge_x3
+ (assert (>= X_3 0.0))
+
+ ;; axiom_le_x3
+ (assert (<= X_3 0.319607843000000002575688995420932769775390625))
+
+ ;; axiom_ge_x4
+ (assert (>= X_4 0.476470588000000028205960234117810614407062530517578125))
+
+ ;; axiom_le_x4
+ (assert (<= X_4 1.0))
+
+ ;; Goal robust_record0_y1
+ (assert
+ (or
+ (and (>= Y_0 Y_1))
+ (and (>= Y_2 Y_1))
+ (and (>= Y_3 Y_1))
+ (and (>= Y_4 Y_1))
+ ))
+
+ [caisar][INFO] Verification results for theory 'JSON'
[caisar] Goal property: Unknown ()
--
GitLab