sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2018-01-23	Added additional tests, and fixed ocaml build of ARM tests	Alasdair Armstrong

2018-01-22	Update Lem shallow embedding to Sail2	Thomas Bauereiss
	- Remove vector start indices - Library refactoring: Definitions in sail_operators.lem now use Bitvector type class and work for both bit list and machine word representations - Add Lem bindings to AArch64 and RISC-V preludes TODO: Merge specialised machine word operations from sail_operators_mwords into sail_operators.
2018-01-18	Clean up command line options slightly	Alasdair Armstrong
	Changed -mono-split to -mono_split to be consistent with other options that use underscores, -mono-split still works but gives a warning message, just so nothing breaks immediately because of this. Removed this sil commands since they really don't do anything right now.
2018-01-18	Modified ocaml backend to use ocamlfind for linksem and lem	Alasdair Armstrong
	Fixed test cases for ocaml backend and interpreter
2018-01-18	Modified unification so Type_check.instantiation_of works after sizeof rewriting	Alasdair Armstrong
	This change allows the AST to be type-checked after sizeof re-writing. It modifies the unification algorithm to better support checking multiplication in constraints, by using division and modulus SMT operators if they are defined. Also made sure the typechecker doesn't re-introduce E_constraint nodes, otherwise re-checking after sizeof-rewriting will re-introduce constraint nodes.
2018-01-17	Add generated ARM spec and test cases for it	Alasdair Armstrong
	We add the generated ARM no_vector spec from the public v8.3 XML release, mostly so that we can add end-to-end test cases for sail using it. This kind of large example is very useful for thoroughly testing the sail compiler and interpreter.