| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-12-07 | Reading of register slices and bits should now be tagged and effect ↵ | Kathy Gray | |
| annotated properly, as well as field accesses. Writing of register slices and bits still look like writes of full registers from tags and effects (probably, if it works, it's an accident) WARNING: interpreter still not up to date with this change | |||
| 2015-12-04 | First bit of making tags and effects on sub vector accesses work for static ↵ | Kathy Gray | |
| compilation. So, it should be right for E_field, but isn't right for E_vector_access, and hasn't begun for E_vector_subrange Isn't right for any writes **WARNING** lem ast files generated from this may not have the proper behaviour on field accesses. | |||
| 2015-12-03 | added prompt.lem for connecting to concurrency model and ↵ | Christopher Pulte | |
| {power,armv8}_extras.lem; fixes | |||
| 2015-11-25 | non-working sail/mips interpreter integration for kathy to look at and ↵ | Robert Norton | |
| example mips elf file. | |||
| 2015-11-25 | fixes, pp | Christopher Pulte | |
| 2015-11-24 | Fixup effect equality bug introduced by adding e_escape | Kathy Gray | |
| 2015-11-24 | Add BE_escape effect when an E_exit is seen | Kathy Gray | |
| Close #20 | |||
| 2015-11-22 | do effect annotation updates more systematically, fix dedup | Christopher Pulte | |
| 2015-11-20 | Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2 | 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-20 | make the abis directory as well | Kathy Gray | |
| 2015-11-20 | fixes to get-elf to work on linux. Hope it works on Mac too. | Robert Norton | |
| 2015-11-20 | Initial version of mips sail model. | Robert Norton | |
| 2015-11-19 | Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2 | Christopher Pulte | |
| 2015-11-19 | fixes for cumulative effect anotations | Christopher Pulte | |
| 2015-11-19 | Keep up with linksem | Kathy Gray | |
| 2015-11-19 | More makefile type | Kathy Gray | |
| 2015-11-19 | typo in make file | Kathy Gray | |
| 2015-11-18 | Update makefile for elf | Kathy Gray | |
| 2015-11-17 | Very nearly there sequential interpreter, just need to hook in the spec ↵ | Kathy Gray | |
| files for the different isas to support | |||
| 2015-11-13 | fixes, more pp | Christopher Pulte | |
| 2015-11-12 | Incorporating elf into sequential interpreter | Kathy Gray | |
| Fix an effect bug on aliased id | |||
| 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-10 | More tag refinement for lexp | Kathy Gray | |
| 2015-11-10 | Update tag for register write in nested lexp | Kathy Gray | |
| Also starting to try to get elf compiling for sequential interpreter | |||
| 2015-11-10 | Make first half of sequential interpreter driver compile again | Kathy Gray | |
| 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 | Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2 | Christopher Pulte | |
| 2015-11-06 | fixes | Christopher Pulte | |
| 2015-11-06 | fixes | Christopher Pulte | |
| 2015-11-05 | Fix a type internal bug | Kathy Gray | |
| Start checking for numeric ranges for int/big int separation | |||
| 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-11-03 | Support int and bigint library functions | Kathy Gray | |
| 2015-11-02 | Catch missing cumulative effect on setting local var | Kathy Gray | |
| 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-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 | slight change to library | Kathy Gray | |
| 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 | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |