Skip to content
Snippets Groups Projects
Commit 963a7b13 authored by Michele Alberti's avatar Michele Alberti
Browse files

Merge branch 'bump_to_why3_1.5' into 'master' 

Bump Why3 to version 1.5.0

See merge request laiser/caisar!31
parents a9c34568 4835bd80
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
caisar.opam
+ 1
− 4
View file @ 963a7b13
......@@ -29,7 +29,7 @@ depends: [
"menhirLib" {>= "20210310"}
"ppx_deriving_yojson" {>= "3.6.1"}
"csv" {>= "2.4"}
"why3" {= "1.4.0"}
"why3" {>= "1.5.0"}
"re"
"caisar-nnet" {= version}
"caisar-ovo" {= version}
......@@ -53,6 +53,3 @@ build: [
["dune" "install" "-p" name "--create-install-files" name]
]
dev-repo: "git+https://git.frama-c.com/pub/caisar.git"
pin-depends: [
[ "why3.1.4.0" "git+https://gitlab.inria.fr/why3/why3.git#047c34a8" ]
]
caisar.opam.template
+ 0
− 3
View file @ 963a7b13
pin-depends: [
[ "why3.1.4.0" "git+https://gitlab.inria.fr/why3/why3.git#047c34a8" ]
]
dune-project
+ 1
− 1
View file @ 963a7b13
......@@ -72,7 +72,7 @@
(menhirLib (>= 20210310))
(ppx_deriving_yojson (>= 3.6.1))
(csv (>= 2.4))
(why3 (= 1.4.0))
(why3 (>= 1.5.0))
re
(caisar-nnet (= :version))
(caisar-ovo (= :version))
......
src/autodetect.ml
+ 13
− 2
View file @ 963a7b13
......@@ -38,7 +38,18 @@ let autodetection ?(debug = false) () =
lookup_file Dirs.Sites.config "caisar-detection-data.conf"
in
let data = Autodetection.Prover_autodetection_data.from_file caisar_conf in
let provers = Autodetection.find_provers data in
let provers =
List.fold_left ~init:[] provers ~f:(fun acc (path, name, version) ->
{
Autodetection.Partial.name;
path;
version;
shortcut = None;
manual = false;
}
:: acc)
in
let config = Whyconf.init_config (Some null) in
let binaries = Autodetection.request_binaries_version config data in
let provers = Autodetection.compute_builtin_prover binaries config data in
let provers = Autodetection.compute_builtin_prover provers config data in
Whyconf.set_provers config provers
tests/marabou.t
+ 4
− 4
View file @ 963a7b13
......@@ -34,12 +34,12 @@ Test verify
> ((0.0:t) .< y1 \/ (0.5:t) .< y1) /\ (0.0:t) .< y2 .< (0.5:t)
> end
> EOF
<autodetect>Run: ($TESTCASE_ROOT/bin/pyrat.py --version) > $TMPFILE 2>&1
<autodetect>Run: ($TESTCASE_ROOT/bin/saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
<autodetect>Run: ($TESTCASE_ROOT/bin/alt-ergo --version) > $TMPFILE 2>&1
<autodetect>Run: ($TESTCASE_ROOT/bin/Marabou --version) > $TMPFILE 2>&1
<autodetect>0 prover(s) added
<autodetect>Generating strategies:
<autodetect>Run: (Marabou --version) > $TMPFILE 2>&1
<autodetect>Run: (alt-ergo --version) > $TMPFILE 2>&1
<autodetect>Run: (saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
<autodetect>Run: (pyrat.py --version) > $TMPFILE 2>&1
<autodetect>Found prover Alt-Ergo version 2.4.0, OK.
<autodetect>Found prover Marabou version 1.0.+, OK.
<autodetect>Found prover PyRAT version 1.1, OK.
......
tests/simple.t
+ 4
− 4
View file @ 963a7b13
......@@ -37,12 +37,12 @@ Test verify
> ((0.0:t) .< y1 \/ (0.5:t) .< y1) /\ (0.0:t) .< y2 .< (0.5:t)
> end
> EOF
<autodetect>Run: ($TESTCASE_ROOT/bin/pyrat.py --version) > $TMPFILE 2>&1
<autodetect>Run: ($TESTCASE_ROOT/bin/saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
<autodetect>Run: ($TESTCASE_ROOT/bin/alt-ergo --version) > $TMPFILE 2>&1
<autodetect>Run: ($TESTCASE_ROOT/bin/Marabou --version) > $TMPFILE 2>&1
<autodetect>0 prover(s) added
<autodetect>Generating strategies:
<autodetect>Run: (Marabou --version) > $TMPFILE 2>&1
<autodetect>Run: (alt-ergo --version) > $TMPFILE 2>&1
<autodetect>Run: (saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
<autodetect>Run: (pyrat.py --version) > $TMPFILE 2>&1
<autodetect>Found prover Alt-Ergo version 2.4.0, OK.
<autodetect>Found prover Marabou version 1.0.+, OK.
<autodetect>Found prover PyRAT version 1.1, OK.
......
tests/simple_onnx.t
+ 4
− 4
View file @ 963a7b13
......@@ -29,12 +29,12 @@ Test verify
> (0.0:t) .< y1 .< (0.5:t)
> end
> EOF
<autodetect>Run: ($TESTCASE_ROOT/bin/pyrat.py --version) > $TMPFILE 2>&1
<autodetect>Run: ($TESTCASE_ROOT/bin/saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
<autodetect>Run: ($TESTCASE_ROOT/bin/alt-ergo --version) > $TMPFILE 2>&1
<autodetect>Run: ($TESTCASE_ROOT/bin/Marabou --version) > $TMPFILE 2>&1
<autodetect>0 prover(s) added
<autodetect>Generating strategies:
<autodetect>Run: (Marabou --version) > $TMPFILE 2>&1
<autodetect>Run: (alt-ergo --version) > $TMPFILE 2>&1
<autodetect>Run: (saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
<autodetect>Run: (pyrat.py --version) > $TMPFILE 2>&1
<autodetect>Found prover Alt-Ergo version 2.4.0, OK.
<autodetect>Found prover Marabou version 1.0.+, OK.
<autodetect>Found prover PyRAT version 1.1, OK.
......
tests/simple_ovo.t
+ 4
− 4
View file @ 963a7b13
......@@ -35,12 +35,12 @@ Test verify
> robust_to svm_apply a (8.0:t)
> end
> EOF
<autodetect>Run: ($TESTCASE_ROOT/bin/pyrat.py --version) > $TMPFILE 2>&1
<autodetect>Run: ($TESTCASE_ROOT/bin/saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
<autodetect>Run: ($TESTCASE_ROOT/bin/alt-ergo --version) > $TMPFILE 2>&1
<autodetect>Run: ($TESTCASE_ROOT/bin/Marabou --version) > $TMPFILE 2>&1
<autodetect>0 prover(s) added
<autodetect>Generating strategies:
<autodetect>Run: (Marabou --version) > $TMPFILE 2>&1
<autodetect>Run: (alt-ergo --version) > $TMPFILE 2>&1
<autodetect>Run: (saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
<autodetect>Run: (pyrat.py --version) > $TMPFILE 2>&1
<autodetect>Found prover Alt-Ergo version 2.4.0, OK.
<autodetect>Found prover Marabou version 1.0.+, OK.
<autodetect>Found prover PyRAT version 1.1, OK.
......
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