From 844b201753394a6f8c83d927c12ab5052425bc97 Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Mon, 4 Apr 2022 10:53:37 +0200
Subject: [PATCH] [SAVer] Created a new table for SVM type and logical symbols.
---
src/language.ml | 8 +++++---
src/language.mli | 3 +++
src/verification.ml | 2 +-
3 files changed, 9 insertions(+), 4 deletions(-)
diff --git a/src/language.ml b/src/language.ml
index 20fa0ddc..ba7fb6e3 100644
--- a/src/language.ml
+++ b/src/language.ml
@@ -17,8 +17,10 @@ type nnshape = {
filename : string;
}
-let loaded_nets = Term.Hls.create 10
-let lookup_loaded_nets = Term.Hls.find_opt loaded_nets
+let loaded_nets = Why3.Term.Hls.create 10
+let loaded_svms = Why3.Term.Hls.create 10
+let lookup_loaded_nets = Why3.Term.Hls.find_opt loaded_nets
+let lookup_loaded_svms = Why3.Term.Hls.find_opt loaded_svms
let register_nn_as_tuple nb_inputs nb_outputs filename env =
let net = Pmodule.read_module env [ "caisar" ] "NN" in
@@ -57,7 +59,7 @@ let register_svm nb_inputs nb_outputs filename env =
(Ident.id_fresh "svm_apply")
[] (Ty.ty_func asarray_input_type asarray_input_type)
in
- Why3.Term.Hls.add loaded_nets ls_svm_apply
+ Why3.Term.Hls.add loaded_svms ls_svm_apply
{ filename; nb_inputs; nb_outputs; ty_data = asarray_input_type };
let th_uc =
Pmodule.add_pdecl ~vc:false th_uc
diff --git a/src/language.mli b/src/language.mli
index 2a053a01..55d5051d 100644
--- a/src/language.mli
+++ b/src/language.mli
@@ -16,6 +16,9 @@ type nnshape = {
val lookup_loaded_nets : Term.lsymbol -> nnshape option
(** @return the filename of a nnet Why3 representation. *)
+val lookup_loaded_svms : Why3.Term.lsymbol -> nnshape option
+(** @return the ioshape of a svm Why3 representation. *)
+
val register_nnet_support : unit -> unit
(** Register NNet parser. *)
diff --git a/src/verification.ml b/src/verification.ml
index c16475ab..03a22e2b 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -82,7 +82,7 @@ let handle_task_saver task env dataset_csv command =
then
let eps = Fmt.str "%a" Constant.print_def e in
let svm_filename =
- match Language.lookup_loaded_nets svm_app_sym with
+ match Language.lookup_loaded_svms svm_app_sym with
| Some t -> t.filename
| None -> failwith "Svm file not found in environment."
in
--
GitLab