sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2017-05-24	Merge branch 'master' of bitbucket.org:Peter_Sewell/sail	Shaked Flur
	# Conflicts: # src/lem_interp/interp.lem # src/lem_interp/interp_inter_imp.lem # src/lem_interp/interp_interface.lem # src/parser.mly # src/pretty_print_lem.ml
2017-05-24	added the exmem effect for AArch64 store-exclusive	Shaked Flur

2017-05-24	Change types of MEMr_tag, MEMval_tag and co. so that tag is separate from ↵	Robert Norton
	data and invent rmemt and wmvt effects for them. Extend the interpreter context to include lists of tagged memory read and write functions. The memory model must round down the address to the nearest capability aligned address when reading/writing tags. Remove TAGw which is no longer needed as a result.
2017-02-03	fix headers	Peter Sewell

2013-10-04	Clean up build system	Gabriel Kerneis

2013-09-26	Adding undefined	Kathy Gray
	Also interpreter now supports reading and writing of basic registers (i.e with no subranges yet)
2013-09-09	Pretty printer to Lem ast added; accessed by -lem_ast on the command line	Kathy Gray

2013-09-05	workaround likely aux rule bug	Peter Sewell

2013-08-30	Small clean up of ott files, start of environments for formal representation ↵	Kathy Gray
	of kind and type system
2013-08-19	Add loops and document optionnal else in conditional	Gabriel Kerneis
	Syntax: foreach id from exp (to\|downto) exp (by exp)? exp foreach and by are keywords; from, to and downto aren't.
2013-08-14	More cases translating from parse_ast to ast. Plus parser changes to syntax ↵	Kathy Gray
	to support type casts; syntax changes not yet reflected in ott file
2013-08-01	Lex and discard comments	Gabriel Kerneis

2013-07-26	A parser without any conflicts.	Kathy Gray
	The ott files have been adjusted to reflect some syntax changes in typquant specifications, and the type annotations are not optional for function definitions; we need additional syntax to help the parser if we want to allow functions without type annotations.
2013-07-26	Remove white space/terminal tracking	Kathy Gray

2013-07-24	Parser compiles and compiles some very small test programs.	Kathy Gray
	Output is only given in the event of a parse or lex failure (with poor reporting for now) There are still 10 shift/reduce conflicts that may need further investigating and a few syntax changes that need discussion.
2013-07-24	Missed files from previous commit	Kathy Gray

2013-07-23	Down to 7 shift/reduce conflicts (with 0 reduce/reduce). Possibly some ↵	Kathy Gray
	syntax needs to change. ott file now builds a pdf again
2013-07-23	wib	Peter Sewell

2013-07-18	More parsing	Kathy Gray

2013-07-17	wib	Peter Sewell

2013-07-17	Separated ott file for parsable AST and parser changes	Kathy Gray