sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2018-04-18	Fix another reference to BK_nat	Alastair Reid

2017-12-06	Add top-level pattern match guards internally	Brian Campbell
	Also fix bug in mono analysis with generated variables Breaks lots of typechecking tests because it generates unnecessary equality tests on units (and the tests don't have generic equality), which I'll fix next.
2017-12-05	Update license headers for Sail source	Alasdair Armstrong

2017-11-17	Fix interpreter to work with new typechecker	Alasdair Armstrong
	Need to map sail type annotations to interpreter type annotations in lem_ast ouput. This doesn't seem too hard.
2017-08-16	lem_interp: remove broken val_to_string_internal functions, replace with ↵	Jon French
	string_of_value as used everywhere else
2017-07-24	move value type definitions to ott, and introduce new E_internal_value ast ↵	Jon French
	node for passing around encapsulated evaluated values; change Interp.to_exp to now just wrap values in this node
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

2016-10-17	updates for ppcmem printing	Kathy Gray

2016-07-25	Support return in interpreter pretty printer (also fix typo for default case)	Kathy Gray

2016-04-18	More fixes to interp with regards to warnings and debugging info	Kathy Gray

2016-03-30	Small missing cases in patterns	Kathy Gray

2016-02-04	fix pretty printing of new mod_s	Robert Norton

2015-06-24	Support new memory write events in the sail front end and pretty printer	Kathy Gray
	Events are eamem to signal the memory address to write to and wmv to pass the value to write
2015-05-18	Match cases better in bit vector printing (i.e. allow undef, and taint)	Kathy Gray

2015-05-13	Add dynamic footprint dependency check event/outcome	Kathy Gray
	Also fix type checker bug in not reporting modifications to parameter values
2015-04-07	Move interpreter to zarith	Kathy Gray

2015-03-26	Add subtraction to nexp grammar (removing the need to do a + (-1 * b))	Kathy Gray
	Fix up parsing on 2** precedence Fix errors on type variables in function definition
2014-11-23	make pretty_interp be back in sync with pretty_print	Kathy Gray

2014-11-21	Print out default values for underspecified vectors instead of leaving them ↵	Kathy Gray
	and letting them turn into undefineds
2014-11-17	Use red printing for the value in the hole from Printing_functions instead ↵	Kathy Gray
	of mangling the ascii manually
2014-11-11	remove [ and ] from values in the hole	Kathy Gray

2014-11-10	Print contents of the [_] hole when it's available.	Kathy Gray
	Also correct makefile typo
2014-11-07	stop using LEMLIB in makefile, in case that's interfering with lem library ↵	Kathy Gray
	placement, switch to LEMLIBOCAML
2014-11-06	Refactor printing to display the contents the [_] and to better format bit ↵	Kathy Gray
	vectors
2014-10-14	Iron out bugs in running new executable with branching; add new executable ↵	Kathy Gray
	as well.
2014-06-30	Support for nondeterministic blocks	Kathy Gray

2014-06-09	Better, colored hole	Gabriel Kerneis

2014-06-09	Support deinfix pretty-printing	Gabriel Kerneis

2014-06-09	Add switch to show/hide casts in interpreter	Gabriel Kerneis
	Use "show_casts" and "hide_casts" in interactive interpreter to display or show casts in expressions. Hidden by default (makes things much less readable otherwise).
2014-06-07	Print holes as [x]	Gabriel Kerneis

2014-06-07	Fix E_vector_append in interp pretty-printer	Gabriel Kerneis

2014-06-06	Add a pretty-printer for Interp_ast	Gabriel Kerneis
	Copy-pasted with a few tweaks from Pretty_printer. Should really make a functor instead, but not sure how to deal with E_internal_cast yet. Note that Interp_ast and Ast are not generated from the same ott file (resp. l2.ott and l2_type.ott), but they are close enough that the code almost "just works".