| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-05-27 | Fix parsing of sizeof and some printing issues with let | Kathy Gray | |
| 2016-05-27 | small change to comment printing | Kathy Gray | |
| 2016-05-27 | Add sizeof to sail. Documentation to follow | Kathy Gray | |
| 2016-04-25 | make pretty printer keep up with parser changes | Kathy Gray | |
| 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-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-02-09 | fix scattered type union source printing | Kathy Gray | |
| 2016-02-08 | slightly clean up vector type printing and empty effect printing for functions | Kathy Gray | |
| 2016-01-26 | move closer to power.sail -> power.ml output | Kathy Gray | |
| 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-21 | fixes, pp progress | Christopher | |
| 2015-12-16 | rewriter and pp changes for generating ARM output | Christopher | |
| 2015-12-15 | better location information | Christopher | |
| 2015-12-09 | adapted for Kathy's lexp effect typing changes: register writes should be ↵ | Christopher | |
| correct now, fixes, pp | |||
| 2015-12-07 | adapted pp for Kathy's effect type changes | Christopher | |
| 2015-12-03 | added prompt.lem for connecting to concurrency model and ↵ | Christopher Pulte | |
| {power,armv8}_extras.lem; fixes | |||
| 2015-11-25 | fixes, pp | Christopher Pulte | |
| 2015-11-24 | Add BE_escape effect when an E_exit is seen | Kathy Gray | |
| Close #20 | |||
| 2015-11-20 | no more unecessary variables from removing vector-concatenation pattern ↵ | Christopher Pulte | |
| matches, reset variable name counter for each function clause, fixes | |||
| 2015-11-19 | fixes for cumulative effect anotations | Christopher Pulte | |
| 2015-11-13 | fixes, more pp | Christopher Pulte | |
| 2015-11-10 | rewriting fixes, syntactically correct lem syntax, number type errors remaining | Christopher Pulte | |
| 2015-11-07 | fixes, no more uncessary variables, pp progress | Christopher Pulte | |
| 2015-11-06 | progress on generating function for read/writing register fields | Christopher Pulte | |
| 2015-11-06 | fixes | Christopher Pulte | |
| 2015-11-05 | some progress on lem backend: rewrite away mutable variable assignments, ↵ | Christopher Pulte | |
| rewrite for-loops, if/case-expressions to return updated variables | |||
| 2015-10-29 | Ocaml generation now just needing big int/little int issues resolved ↵ | Kathy Gray | |
| (probably) at least for Power. | |||
| 2015-10-28 | progress on lem backend: auto-generate read_register and write_register ↵ | Christopher Pulte | |
| functions, and state definition | |||
| 2015-10-26 | fix | Christopher Pulte | |
| 2015-10-26 | Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2 | Christopher Pulte | |
| 2015-10-26 | add preliminary Sail_values.lem, adapt lem pp to recent Ocaml pp changes | Christopher Pulte | |
| 2015-10-23 | More of sail correctly generating ocaml; including using polymorphic ↵ | Kathy Gray | |
| variants when there are more than 246 constructors | |||
| 2015-10-20 | add copies of ocaml-pp functions for lem-pp | Christopher Pulte | |
| 2015-10-20 | ocaml output now produces parsing power.sail | Kathy Gray | |
| 2015-10-20 | more fixes | Kathy Gray | |
| 2015-10-20 | Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2 | Christopher Pulte | |
| 2015-10-20 | compiling prettyprinter | Kathy Gray | |
| 2015-10-20 | Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2 | Christopher Pulte | |
| 2015-10-20 | fix a-normalisation bug | Christopher Pulte | |
| 2015-10-20 | Fixing bugs in pretty printer to ocaml | Kathy Gray | |
| 2015-10-19 | progress on lem backend | Christopher Pulte | |
| 2015-10-13 | Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2 | Christopher Pulte | |
| 2015-10-13 | some progress on sequentialise_effects | Christopher Pulte | |
| 2015-10-13 | Refine local vs cumulative effects for lexp | Kathy Gray | |
| More ocaml output, better treatment of registers. | |||
| 2015-10-07 | Compiling again after refactoring. Haven't pushed to interpreter and lem yet | Kathy Gray | |
| 2015-10-07 | adapted pretty_print and rewriter to new tannot type | Christopher Pulte | |
| 2015-10-07 | start changing representation of registers for ocaml | Kathy Gray | |
| 2015-10-06 | better printing for register writing, whole register (maybe not "right" yet) | Kathy Gray | |
| more library | |||
| 2015-10-05 | made vector_concat pass remove typ annotation expression inside ↵ | Christopher Pulte | |
| vector_concat patterns, fixed a pp missing newline | |||
| 2015-10-04 | add find_updated_vars to support for-loops for lem or prover backend, add ↵ | Christopher Pulte | |
| normalise_exp exp that should transform expressions into a form where they can be embedded into monadic lem or prover definitions. Both untested | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |