| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-05-27 | Also add to ott | Kathy Gray | |
| 2016-03-03 | Fix typo in manual which had true instead of false on assert documentation | Kathy Gray | |
| Fix bug in local register access | |||
| 2016-03-02 | Add new language feature to permit definitions of items of kind Nat, etc as ↵ | Kathy Gray | |
| well as items of kind Type. Syntax for the feature is: def Nat id = nexp Note: some useful nexps may not parse properly. All typedef forms can also be used as def Type ... if desired, but this is not required. | |||
| 2016-02-25 | A bit better readme | Kathy Gray | |
| A few more tips Trying to fix up and bring up to date the built-in types and library | |||
| 2016-02-25 | Expand what advice and information is in the manual slightly | Kathy Gray | |
| 2016-02-25 | Add the manual, such as it is, for others to be able to use and have without ↵ | Kathy Gray | |
| needing ott | |||
| 2016-02-25 | Restore manual.tex mysteriously deleted by peter in May 2015. | Robert Norton | |
| 2016-02-23 | Several fixes | Kathy Gray | |
| Improve printing for asl to sail readability; Add -o option for selecting the name of file generation; Add additional initial check module for turning generated ast nodes into ready-to-type-check ast nodes | |||
| 2016-01-06 | Add new assert expression to Sail | Kathy Gray | |
| This splits the former functionality of exit into errors, which should now use assert(bool,option<string>), and a means of signalling actions such as instruction-level exceptions, interrupts, or other features that impact the ISA. The latter will now be tracked with an effect escape, and so any function containing exit and declared pure will generate a type error. WARNING: ARM spec will not build with this commit until I modify it. MIPS spec will not build with this commit until modified. | |||
| 2015-12-17 | First bit of gluing mips onto interpreter and eventually ppcmem infrastructure | Kathy Gray | |
| 2015-12-14 | Adding new location constructor for location of generated terms | Kathy Gray | |
| 2015-11-24 | Add BE_escape effect when an E_exit is seen | Kathy Gray | |
| Close #20 | |||
| 2015-10-19 | progress on lem backend | Christopher Pulte | |
| 2015-10-08 | Add another internal let for Christopher | Kathy Gray | |
| 2015-10-07 | Start expanding annot for more refined effect tracking | Kathy Gray | |
| 2015-09-30 | Alias support for ocaml mode | Kathy Gray | |
| 2015-09-24 | Parameterise the rewriter's for multiple different rewritings | Kathy Gray | |
| Add a new internal node for moving assignments into scope-preserving expressions that more explicitly define the scope | |||
| 2015-08-06 | Update analysis to merge states and values after branches taken due to ↵ | Kathy Gray | |
| unknown conditions. Does not merge if one path has resulted in an exit | |||
| 2015-07-24 | Begin doing better analysis on case splits over unknowns | Kathy Gray | |
| 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-06-02 | changes to compare and equality instances to make lem generate isabelle output | cp526 | |
| 2015-06-02 | Fix errors around ARM not being able to decode due to instruction_extractor ↵ | Kathy Gray | |
| being very power-specific. Note: slight interface change to instruction_extractor | |||
| 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-05-09 | towards buildability - l2.ml and l2_parse.ml as regenerated with current Ott | Peter Sewell | |
| 2015-05-09 | use less confusing Ott binary | Peter Sewell | |
| 2015-03-31 | Fix int -> nat bug. Now something with type int cannot be used as something ↵ | Kathy Gray | |
| of type nat (at least not without a >= 0 check) | |||
| 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 | |||
| 2015-03-15 | Many changes: | Kathy Gray | |
| Split out specification specific memory and external functions Reduce the presence of big_int Reduce the use of inc direction, instead using a default from the spec. Still a few places need to be parameterised over direction Also some bug fixes exposed by above and running ARM second instruction | |||
| 2015-02-24 | Overloading formal relation | Kathy Gray | |
| 2015-02-18 | All existing type rules in line with implementation (and no more red) | Kathy Gray | |
| Still to do: type rules for register aliases and relation for overloading selection | |||
| 2015-02-18 | expression type checking inline with rules, lexp still out of date; ↵ | Kathy Gray | |
| overloading resolution not modelled | |||
| 2015-02-17 | Bring type rules more into modern state of type checker | Kathy Gray | |
| 2015-02-13 | Actually use new dependency information in generation of lem/etc. | Kathy Gray | |
| Also stop rewriting code in the pretty printer, instead move it all into a new general rewriting pass | |||
| 2015-01-26 | update ott path | Kathy Gray | |
| 2015-01-23 | remove dependency on having ott in ones path | Kathy Gray | |
| 2015-01-12 | Add specialised support for numeric singleton types (i.e. what used to be ↵ | Kathy Gray | |
| range<'N,'N>) Non-sugar syntax is -- forall Nat 'N. atom<'N> Sugar syntax is -- [: 'N :] Also begin adding pp support for generating ocaml from ast types. | |||
| 2014-12-18 | More type rules | Kathy Gray | |
| 2014-12-09 | Some of the type rules for expressions | Kathy Gray | |
| 2014-12-04 | ott rules for type checking pattern match | Kathy Gray | |
| 2014-12-03 | Type rules unto coercion now represented in ott | Kathy Gray | |
| 2014-11-28 | full list of built-in functions in rudimentary manual | Kathy Gray | |
| 2014-11-27 | Start having a manual of sorts. At least specify the built in functions | Kathy Gray | |
| (list not complete) | |||
| 2014-09-30 | Add type annotations to funcls to track effects and constraints from one ↵ | Kathy Gray | |
| function-clause | |||
| 2014-08-13 | Kathy, Peter tweak Makefile for interactive demo and src/myocamlbuild.ml to ↵ | Peter Sewell | |
| temporarily use other version of Lem | |||
| 2014-07-29 | A file can now declare that a default order is either inc or dec, and this ↵ | Kathy Gray | |
| will be reflected in short hand type syntax, inc is still the default if undeclared So: default order dec register bit[32] t (* Declares t as a decreasing vector, starting at 31 on the left and decreasing to 0 *) default order inc register bit[32] o (* Declares o as an increasing vector, starting at 0 on the left and increasing to 31 *) It is presently possible to change the default mid-file; this is almost certainly bad and I will turn it into an error soon. | |||
| 2014-07-25 | Start of setting a default order for literal vectors and for vector ↵ | Kathy Gray | |
| shorthand syntax, needed for arm spec | |||
| 2014-07-18 | Writing to concatenated aliases | Kathy Gray | |
| 2014-07-14 | Initial support for aliases and exit through the type system and the ↵ | Kathy Gray | |
| interpreter. An alias can be read within the interpreter, but not written to. Exits aren't yet taken in the interpreter. | |||
| 2014-07-08 | Extend language to support register aliases and to support interrupts, traps ↵ | Kathy Gray | |
| and the like. | |||
| 2014-06-26 | Adding better support for unspecified values in indexed vectors | Kathy Gray | |
| Also begining to add support for nondeterministic blocks and cleaning up some of the Many warnings on pattern matches | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |