Merge branch 'fix/absolute_lib_path' into 'master'

Fix for making path to network file absolute.

See merge request laiser/caisar!13

.gitlab-ci.yml

@@ -3,13 +3,13 @@ stages:
 
 tests:
   stage: test
-  image: ocaml/opam@sha256:108b775e7bda2c6d3bddae61c9cdb003e40de746baf3a994e8f7b82d8301dd0a
+  image: ocaml/opam@sha256:013a26ccbaa8344b63274e335e2492c432cec1c3526b9ba888ab151abb2b4c25
   cache:
     key: $CI_COMMIT_REF_SLUG
     paths:
       - _opam
   script:
-  - if [ ! -d _opam ]; then echo "no local switch in the CI cache, we setup a new switch"; opam switch create --yes --no-install . ocaml-base-compiler.4.11.1; fi
+  - if [ ! -d _opam ]; then echo "no local switch in the CI cache, we setup a new switch"; opam switch create --yes --no-install . ocaml-base-compiler.4.13.1; fi
   - eval $(opam env)
   - sudo apt-get update
   - sudo apt install -y protobuf-compiler

caisar.opam

@@ -3,7 +3,7 @@ opam-version: "2.0"
 version: "0.1"
 synopsis: "Framework for neural network verification"
 depends: [
-  "ocaml" {>= "4.10"}
+  "ocaml" {>= "4.13.0"}
   "dune-site" {>= "2.9.0"}
   "piqi" {>= "0.7.6"}
   "piqilib" {>= "0.6.14"}

dune-project

@@ -13,7 +13,7 @@
   (name caisar)
   (synopsis "Framework for neural network verification")
   (depends
-   (ocaml (>= 4.10))
+   (ocaml (>= 4.13.0))
    (dune-site (>= 2.9.0))
    (piqi (>= 0.7.6))
    (piqilib (>= 0.6.14))

src/main.ml

@@ -127,7 +127,7 @@ let verify_cmd =
   in
   let loadpath =
     let doc = "Additional loadpath." in
-    Arg.(value & opt_all string [] & info [ "L" ] ~doc)
+    Arg.(value & opt_all string [ "." ] & info [ "L"; "loadpath" ] ~doc)
   in
   let memlimit =
     let doc = "Memory limit (in megabytes)." in

src/verification.ml

@@ -54,8 +54,8 @@ let call_prover ~limit config (prover : Why3.Whyconf.config_prover) driver task
     | Some _ -> assert false (* By construction of the meta. *)
     | None -> invalid_arg (Fmt.str "No neural network model found in task")
   in
-  let nn_file = Filename.concat (Caml.Sys.getcwd ()) nn_file in
-  let command = Re.replace_string nnet_or_onnx ~by:nn_file command in
+  let nn_file = Unix.realpath nn_file in
+  let command = Re__Core.replace_string nnet_or_onnx ~by:nn_file command in
   let call_prover_on_task task_prepared =
     let prover_call =
       Driver.prove_task_prepared ~libdir:(Whyconf.libdir config)