diff options
| -rw-r--r-- | .gitignore | 26 | ||||
| -rwxr-xr-x | test/c/run_tests.py | 10 |
2 files changed, 31 insertions, 5 deletions
@@ -28,8 +28,15 @@ lib/hol/sail-heap # Coq *.vo +*.vok +*.vos *.glob .*.aux +/lib/coq/.nia.cache + +# Isabelle + +/lib/isabelle/output # location specific things @@ -42,6 +49,7 @@ lib/hol/sail-heap /src/jib.ml /src/manifest.ml +/test/sailtest.pyc /test/typecheck/rtpass*/ /test/typecheck/tests.xml /test/lem/Out_lemmas.thy @@ -49,6 +57,19 @@ lib/hol/sail-heap /test/lem/out_types.lem /test/*/tests.xml /test/riscv/tests/*.iout +/test/smt/*.out +/test/smt/*.smt2 +/test/c/*.c +/test/c/*.result +/test/c/*.iresult +/test/c/*.oresult +/test/c/*.bin +/test/c/*_ocaml +/test/c/_sbuild* +/test/mono/Out_lemmas.thy +/test/mono/log +/test/mono/test.cmi +/test/mono/test.cmo /language/*.pdf /language/*.uo @@ -62,6 +83,11 @@ lib/hol/sail-heap /language/*.dvi /language/*.ps +/aarch64_small/ArmV8_lemmas.thy +/aarch64_small/armV8.lem +/aarch64_small/armV8.smt_model +/aarch64_small/armV8_types.lem + /aarch64/Aarch64.thy /aarch64/Aarch64Auxiliary.thy /aarch64/Aarch64_extras.thy diff --git a/test/c/run_tests.py b/test/c/run_tests.py index 64c3ae42..c9474614 100755 --- a/test/c/run_tests.py +++ b/test/c/run_tests.py @@ -21,11 +21,11 @@ def test_c(name, c_opts, sail_opts, valgrind): tests[filename] = os.fork() if tests[filename] == 0: step('sail -no_warn -c {} {} 1> {}.c'.format(sail_opts, filename, basename)) - step('gcc {} {}.c {}/lib/*.c -lgmp -lz -I {}/lib -o {}'.format(c_opts, basename, sail_dir, sail_dir, basename)) - step('./{} 1> {}.result'.format(basename, basename), expected_status = 1 if basename == "exception" else 0) + step('gcc {} {}.c {}/lib/*.c -lgmp -lz -I {}/lib -o {}.bin'.format(c_opts, basename, sail_dir, sail_dir, basename)) + step('./{}.bin 1> {}.result'.format(basename, basename), expected_status = 1 if basename == "exception" else 0) step('diff {}.result {}.expect'.format(basename, basename)) if valgrind: - step("valgrind --leak-check=full --track-origins=yes --errors-for-leak-kinds=all --error-exitcode=2 ./{}".format(basename), expected_status = 1 if basename == "exception" else 0) + step("valgrind --leak-check=full --track-origins=yes --errors-for-leak-kinds=all --error-exitcode=2 ./{}.bin".format(basename), expected_status = 1 if basename == "exception" else 0) print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END) sys.exit() results.collect(tests) @@ -56,8 +56,8 @@ def test_ocaml(name): basename = os.path.splitext(os.path.basename(filename))[0] tests[filename] = os.fork() if tests[filename] == 0: - step('sail -ocaml -ocaml_build_dir _sbuild_{} -o {} {}'.format(basename, basename, filename)) - step('./{} 1> {}.oresult'.format(basename, basename), expected_status = 1 if basename == "exception" else 0) + step('sail -ocaml -ocaml_build_dir _sbuild_{} -o {}_ocaml {}'.format(basename, basename, filename)) + step('./{}_ocaml 1> {}.oresult'.format(basename, basename), expected_status = 1 if basename == "exception" else 0) step('diff {}.oresult {}.expect'.format(basename, basename)) print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END) sys.exit() |