From 29d19a81efa8f164856a10a7734e9ee260d74729 Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Tue, 5 Apr 2022 10:36:34 +0200
Subject: [PATCH] [SAVer] Modified comment.
---
src/language.ml | 7 ++++---
src/verification.ml | 7 +++----
2 files changed, 7 insertions(+), 7 deletions(-)
diff --git a/src/language.ml b/src/language.ml
index ba7fb6e3..425458d6 100644
--- a/src/language.ml
+++ b/src/language.ml
@@ -7,8 +7,8 @@
open Why3
open Base
-(* -- Support for the NNet and ONNX neural network formats, as well as SVM under
- the .ovo format *)
+(* Support for several model formats: - NNet and ONNX for neural networks, - OVO
+ for for SVM *)
type nnshape = {
nb_inputs : int;
@@ -57,7 +57,8 @@ let register_svm nb_inputs nb_outputs filename env =
let ls_svm_apply =
Term.create_fsymbol
(Ident.id_fresh "svm_apply")
- [] (Ty.ty_func asarray_input_type asarray_input_type)
+ []
+ (Ty.ty_func asarray_input_type asarray_input_type)
in
Why3.Term.Hls.add loaded_svms ls_svm_apply
{ filename; nb_inputs; nb_outputs; ty_data = asarray_input_type };
diff --git a/src/verification.ml b/src/verification.ml
index ee54efab..0aec2d25 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -87,7 +87,7 @@ let answer_saver limit config task env prover dataset_csv =
let svm_filename =
match Language.lookup_loaded_svms svm_app_sym with
| Some t -> t.filename
- | None -> failwith "Svm file not found in environment."
+ | None -> failwith "SVM file not found in environment."
in
(eps, svm_filename)
else failwith "Wrong predicate found."
@@ -136,9 +136,8 @@ let answer_saver limit config task env prover dataset_csv =
then Call_provers.Valid
else Call_provers.Invalid
| None -> Call_provers.HighFailure
- (* Any other answer than HighFailure should
- * never happen as we do not define
- * anything in SAVer's driver *))
+ (* Any other answer than HighFailure should never happen as we do not
+ define anything in SAVer's driver *))
| _ -> assert false
in
answer
--
GitLab