| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-05-27 | Add sizeof to sail. Documentation to follow | 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-01-26 | move closer to power.sail -> power.ml output | Kathy Gray | |
| 2016-01-21 | Start splitting values/etc into int/big_int for ocaml generation | Kathy Gray | |
| 2016-01-14 | small edit to previous commit | Kathy Gray | |
| 2016-01-14 | Fix cumulative effects for circumstance when lifting variable introductions ↵ | Kathy Gray | |
| out of an if Note: this fixes the local cumulative effects for the e_assign and e_if, it may not properly propagate them to the context of the surrounding block | |||
| 2016-01-12 | Fix undefined nvar occurrences that were impacting ARM | Kathy Gray | |
| 2016-01-07 | Add E_assert to basic rewriters | Kathy Gray | |
| 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-10 | fix | Christopher | |
| 2015-12-09 | adapted for Kathy's lexp effect typing changes: register writes should be ↵ | Christopher | |
| correct now, fixes, pp | |||
| 2015-11-25 | fixes, pp | Christopher Pulte | |
| 2015-11-22 | do effect annotation updates more systematically, fix dedup | Christopher Pulte | |
| 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 | fix case-expressions' newreturn | 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 | fixes | 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-11-04 | Add a new module for writing queries/analyses that aren't type checking but ↵ | Kathy Gray | |
| could be useful Define in that a function for determining a default direction for vectors | |||
| 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 | Switch name set to name map to include type and expression data | Kathy Gray | |
| 2015-10-26 | Add variable set to rewriters | Kathy Gray | |
| 2015-10-26 | Begin if variable introduction rewriting | Kathy Gray | |
| 2015-10-20 | fix a-normalisation bug | Christopher Pulte | |
| 2015-10-19 | progress on lem backend | Christopher Pulte | |
| 2015-10-17 | clean up, more readability | Christopher Pulte | |
| 2015-10-17 | a-normalisation for lem backend | Christopher Pulte | |
| 2015-10-13 | some progress on sequentialise_effects | Christopher Pulte | |
| 2015-10-12 | fixes | Christopher Pulte | |
| 2015-10-12 | apply rewriter changes to master as well | Christopher Pulte | |
| 2015-10-07 | adapted pretty_print and rewriter to new tannot type | Christopher Pulte | |
| 2015-10-06 | added the preliminary lem output option that for now uses ocaml pp | Christopher Pulte | |
| 2015-10-06 | Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2 | Christopher Pulte | |
| 2015-10-06 | fixes | Christopher Pulte | |
| 2015-10-06 | make let and case actually call pattern rewriter | Kathy Gray | |
| 2015-10-05 | made vector_concat pass remove typ annotation expression inside ↵ | Christopher Pulte | |
| vector_concat patterns, fixed a pp missing newline | |||
| 2015-10-05 | some fixes | Christopher Pulte | |
| 2015-10-05 | Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2 | Christopher Pulte | |
| 2015-10-05 | added pattern rewriting for DEF_val expressions | Christopher Pulte | |
| 2015-10-05 | More library functions | Kathy Gray | |
| Tweak to rewriter to actually rewrite function patterns | |||
| 2015-10-05 | added funcl pattern rewriting to remove vector concat patterns | Christopher Pulte | |
| 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 | |||
| 2015-09-29 | ml output passing simple test suite, except for register aliases | Kathy Gray | |
| Known todo: Write library functions in ocaml Properly upper-case/lower-case the first letter of names to conform to ocaml requirements Handle register aliases Turn id reads to dereferences for local ref variables | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |