sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2019-06-19	Make C emulator exit with failure for uncaught exception. Make special case ↵	Robert Norton
	for 'exception.sail' test that deliberately exits with uncaught exception.
2019-04-09	SMT: Experimental Jib->SMT translation	Alasdair Armstrong
	Currently only works with CVC4, test cases are in test/smt. Can prove that RISC-V add instruction actually adds values in registers and that's about it for now.
2018-12-14	Add a few more tests for Jenkins	Alasdair Armstrong
	Some of the output from the tests scripts is odd on Jenkins, try to fix this by flushing stdout more regularly in the test scripts
2018-12-12	Add parallelism limit to C and builtins test	Alasdair Armstrong
	Spawning a process for every test and running every test in parallel is quite RAM intensive (up to about 8gb) especially when running valgrind on every test in parallel. Now we only run up to TEST_PAR tests in parallel (default 4).
2018-08-17	Improve builtins tests	Alasdair Armstrong
	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.
2018-08-16	Ressurect builtin tests, and add parallel test runner script	Alasdair Armstrong
	Add new python test runner script, which allows tests to be run in parallel before collecting the results. This makes the tests run a lot faster, especially for the builtins and C compilation tests. Also handles reporting errors mushc more nicely than the previous way of doing it in shell script.