diff options
| author | Alasdair Armstrong | 2018-08-17 18:49:33 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-08-17 20:42:09 +0100 |
| commit | c0f68b6712c916a3cf16f933840a48ec22330289 (patch) | |
| tree | 549577f558afb31e4171229e37783fce532835bc /test/builtins/test_extras.lem | |
| parent | c3595cbfc8f4f04cb13c693054ba62487bcd0e24 (diff) | |
Improve builtins tests
Test the builtin functions by compiling them to C, OCaml, and OCaml
via Lem. Split up some of the longer builtin test programs to avoid
stack overflows when compiling to OCaml, as 3000+ line long blocks can
cause issues with some re-writing steps.
Also test constant-folding with builtins (this should reduce the
asserts in these files to assert true), and also test constant folding
with the C compilation.
Fix a bug whereby vectors with heap-allocated elements were not
initialized correctly.
Fix a bug caused by compiling and optimising empty vector literals.
Fix an OCaml test case that broke due to the ref type being used. Now
uses references to registers.
Fix a bug where Sail would output big integers that lem can't
parse. Checks if integer is between Int32.min_int and Int32.max_int
and if not, use integerOfString to represent the integer. Really this
should be fixed in Lem.
Make the python test runner script the default for testing builtins
and running the C compilation tests in test/run_tests.sh
Add a ocaml_build_dir option that sets a custom build directory for
OCaml. This is needed for running OCaml tests in parallel so the
builds don't clobber one another.
Diffstat (limited to 'test/builtins/test_extras.lem')
| -rw-r--r-- | test/builtins/test_extras.lem | 19 |
1 files changed, 0 insertions, 19 deletions
diff --git a/test/builtins/test_extras.lem b/test/builtins/test_extras.lem deleted file mode 100644 index ae3ed1ba..00000000 --- a/test/builtins/test_extras.lem +++ /dev/null @@ -1,19 +0,0 @@ -open import Pervasives_extra -open import Sail_instr_kinds -open import Sail_values -open import Sail_operators_mwords -open import Prompt_monad -open import State - -type ty0 -instance (Size ty0) let size = 0 end -declare isabelle target_rep type ty1 = `0` - -val undefined_int : forall 'rv 'e. unit -> monad 'rv integer 'e -let undefined_int () = return 0 - -val undefined_bitvector : forall 'rv 'a 'e. Size 'a => integer -> monad 'rv (mword 'a) 'e -let undefined_bitvector len = return (zeros(len)) - -val undefined_unit : forall 'rv 'e. unit -> monad 'rv unit 'e -let undefined_unit () = return () |