From 3083de2d112bb0e0e410c90c813855440098abc6 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Thu, 16 Sep 2021 22:27:23 +0200
Subject: [PATCH] Some more rework.
---
src/language.ml | 6 +++---
src/verification.ml | 2 +-
tests/autodetect.t | 24 ++++++++++++++++++++++++
3 files changed, 28 insertions(+), 4 deletions(-)
diff --git a/src/language.ml b/src/language.ml
index 28bf71e8..177c1f74 100644
--- a/src/language.ml
+++ b/src/language.ml
@@ -6,7 +6,7 @@
open Base
-(* -- Register neural network format. *)
+(* -- Support for the NNet neural network format. *)
let nnet_parser env _ filename _ =
let open Why3 in
@@ -32,11 +32,11 @@ let nnet_parser env _ filename _ =
in
let th_uc =
Pmodule.add_pdecl ~vc:false th_uc
- (Pdecl.create_pure_decl @@ Decl.create_param_decl ls_nnet_apply)
+ (Pdecl.create_pure_decl (Decl.create_param_decl ls_nnet_apply))
in
Wstdlib.Mstr.singleton "AsTuple" (Pmodule.close_module th_uc)
-let register () =
+let register_nnet_support () =
Why3.(
Env.register_format ~desc:"NNet format (ReLU only)" Pmodule.mlw_language
"NNet" [ "nnet" ] nnet_parser)
diff --git a/src/verification.ml b/src/verification.ml
index 74d0fd55..624acb45 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -8,7 +8,7 @@ open Base
module Format = Caml.Format
module Filename = Caml.Filename
-let () = Language.register ()
+let () = Language.register_nnet_support ()
let create_env loadpath =
let config = Autodetection.autodetect ~debug:true () in
diff --git a/tests/autodetect.t b/tests/autodetect.t
index 6f08613f..02dd58bd 100644
--- a/tests/autodetect.t
+++ b/tests/autodetect.t
@@ -1,3 +1,27 @@
Test autodetect
+ $ mkdir bin
+
+ $ cat - > bin/pyrat.py << EOF
+ > #!/bin/sh
+ > echo "PyRAT 1.0"
+ > EOF
+
+ $ cat - > bin/Marabou << EOF
+ > #!/bin/sh
+ > echo "1.0.+"
+ > EOF
+
+ $ chmod u+x bin/pyrat.py bin/Marabou
+
+ $ bin/pyrat.py
+ PyRAT 1.0
+
+ $ bin/Marabou
+ 1.0.+
+
+ $ PATH=$(pwd)/bin:$PATH
+
$ caisar config -d
[caisar] Alt-Ergo 2.4.0
+ Marabou 1.0.+
+ PyRAT 1.0
--
GitLab