| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-08-15 | Removed Typ_arg_effect - nobody used it and it isn't supported by the backends. | Alasdair Armstrong | |
| 2017-08-10 | Merge remote-tracking branch 'origin/sail_new_tc' into experiments | Alasdair Armstrong | |
| Conflicts: src/pretty_print_common.ml | |||
| 2017-08-07 | Improvements to existentials for ASL parser | Alasdair Armstrong | |
| 2017-08-07 | Fixed pretty printing of E_cons | Alasdair Armstrong | |
| 2017-08-02 | Improve pretty-printing of register declaration and assignment | Thomas Bauereiss | |
| 2017-07-27 | Fixed pretty printer for existentials | Alasdair Armstrong | |
| Also fixed substitution functions so as to not substitute captured kind identifiers | |||
| 2017-07-26 | Allow arbitrary identifiers in nexp expressions | Alasdair Armstrong | |
| Fixed some bugs in the initial check that caused valid code to fail to parse Add a nid utility function that creates an id n-expression, similar to nvar, nconstant etc | |||
| 2017-06-29 | Added a large test case to the test-suite | Alasdair Armstrong | |
| Commented out some buggy re-sugaring logic from pretty_print_common where it re-sugared vectors incorrectly Fixed a bug where the type checker forgot to preserve type signatures in top-level letbinds | |||
| 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-03-29 | Factor out pretty printers into separate files. Hopefully this will make ↵ | Robert Norton | |
| searching easier. | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |