[NN_prover] Add $CAISAR_ONNX_OUTPUT_DIR for specifying output directory

  - todo use the onnx-out-dir option

lib/onnx/tests/print.expected

 true
 ok
 ok
-Input name 0
+1 files checked

src/transformations/native_nn_prover.ml

@@ -185,7 +185,8 @@ let create_new_nn env input_vars outputs : string =
   assert (
     IR.Shape.equal output.shape (IR.Shape.of_array [| List.length outputs |]));
   let nn = IR.create output in
-  let filename = Stdlib.Filename.temp_file "caisar" ".onnx" in
+  let temp_dir = Sys.getenv "CAISAR_ONNX_OUTPUT_DIR" in
+  let filename = Stdlib.Filename.temp_file ?temp_dir "caisar" ".onnx" in
   Onnx.Simple.write nn filename;
   filename
 

tests/acasxu.t

@@ -4,6 +4,9 @@ Test verify on acasxu
   $ bin/pyrat.py --version
   PyRAT 1.1
 
+  $ mkdir out
+  $ export CAISAR_ONNX_OUTPUT_DIR=out
+
   $ cat > file.mlw <<EOF
   > theory T
   >   use ieee_float.Float64
@@ -1179,3 +1182,6 @@ Test verify on acasxu
   Goal run3'vc: Unknown ()
   Goal test'vc: Unknown ()
   Goal P3: Unknown ()
+
+  $ python3 bin/inspect_onnx.py
+  12 files checked

tests/bin/inspect_onnx.py

 import onnx
 import os
 
-for file in os.listdir("out"):
+l = os.listdir("out")
+
+for file in l:
     m = onnx.load(os.path.join("out", file))
-    if len(m.graph.initializer) >= 1:
-        initi = m.graph.initializer[0]
-        print(
-            "Initializer name {name} has data {val:3.3f}".format(
-                name=initi.name, val=initi.float_data[2]
-            )
-        )
-    if len(m.graph.input) >= 1:
-        print(
-            f"Input name {m.graph.input[0].name}"
-        )
     onnx.checker.check_model(m)
+    
+print(len(l),"files checked")
\ No newline at end of file

tests/nier_to_onnx.t

@@ -26,4 +26,4 @@ Test verify
 Data should be 0.135
 
   $ python3 bin/inspect_onnx.py
-  Input name 0
+  1 files checked