diff --git a/lib/onnx/tests/print.expected b/lib/onnx/tests/print.expected index e5444a6f08f881a2a427ccc2df25ac60c6d317cc..8088b7083d16a0d4a3c4fde8abf014b524fbd91e 100644 --- a/lib/onnx/tests/print.expected +++ b/lib/onnx/tests/print.expected @@ -1,4 +1,4 @@ true ok ok -Input name 0 +1 files checked diff --git a/src/transformations/native_nn_prover.ml b/src/transformations/native_nn_prover.ml index 7cd8fd9d170146231316c937201b19e139aa1b5f..3bac14153a02920ac73e6459a86f34f3deafc8ae 100644 --- a/src/transformations/native_nn_prover.ml +++ b/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 diff --git a/tests/acasxu.t b/tests/acasxu.t index aaec5a866e4c2dc41b44f76587d8daaebff10957..2612b32215fad627641549147c7d0323b6f2367b 100644 --- a/tests/acasxu.t +++ b/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 diff --git a/tests/bin/inspect_onnx.py b/tests/bin/inspect_onnx.py index a109a495a11f9aef38d80f41c26d4cefb9e5559f..800f144e5a7c67d8cc0caee9f508f0e691ad8b5c 100644 --- a/tests/bin/inspect_onnx.py +++ b/tests/bin/inspect_onnx.py @@ -1,17 +1,10 @@ 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 diff --git a/tests/nier_to_onnx.t b/tests/nier_to_onnx.t index e062cca4fce43f3ba877669b068b67bc7b521a47..d754d03be90f16fbd34cf57f009b89b0f61e49ed 100644 --- a/tests/nier_to_onnx.t +++ b/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