| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-01-14 | changes to enable interpreter exhaustive analysis in ppcmem again | Christopher Pulte | |
| 2016-12-01 | move interpreter-specific types from Sail_impl_base to Interp_interface | Christopher Pulte | |
| 2016-11-27 | make outcome_s contain the instruction state pretty print rather than the ↵ | Christopher Pulte | |
| instruction state, factor out interpreter/shallow embedding value conversion | |||
| 2016-11-09 | move decode_error type back to Sail_impl_base for now | Christopher Pulte | |
| 2016-11-08 | fixes | Christopher Pulte | |
| 2016-11-05 | fixes | Christopher Pulte | |
| 2016-10-21 | shallow embedding progress | Christopher Pulte | |
| 2016-10-06 | move type definitions that both interpreter and shallow embedding use to ↵ | Christopher Pulte | |
| sail_impl_base, add sail_impl_base.outcome, add interp_inter_imp auxiliary functions, make prompt use sail_impl_base.outcome | |||
| 2016-09-30 | add Robert's DIA typeclass instances | Christopher Pulte | |
| 2016-09-30 | fixes, update isntruction_analysis for NIAs and DIA | Christopher Pulte | |
| 2016-09-19 | remove conflict message | Christopher Pulte | |
| 2016-09-16 | make vector concatenation pattern removal deal with vector patterns of ↵ | Christopher Pulte | |
| unknown length (in the last item) | |||
| 2016-09-14 | Add memory kind for concurrent tag reads and writes | Kathy Gray | |
| 2016-09-13 | Add optional address to memv events | Kathy Gray | |
| 2016-09-13 | add show functions, fix | Christopher Pulte | |
| 2016-09-09 | minor fixes | Kathy Gray | |
| 2016-09-09 | update instruction_analysis to support nias and instruction kind | Christopher Pulte | |
| 2016-09-02 | Extend type checking so that patterns with vector concatenation don't permit ↵ | Kathy Gray | |
| under specified vector lengths (at least for function patterns) Extend interpreter interface to have a function for Christopher's instruction analysis | |||
| 2016-08-18 | move register_base_name and slice_of_reg_name from ppcmem thread semantics ↵ | Christopher | |
| to interp_interface, fix reg_name comparison and equality | |||
| 2016-08-06 | Add duplicate_bits to lib | Kathy Gray | |
| Pull Peter's changes to interp_interface back into the primary repo | |||
| 2016-05-03 | Change decode and translate_address to support writing register events ↵ | Kathy Gray | |
| (although decode isn't pushed through yet). Note: this will break all builds | |||
| 2016-04-25 | Make interpreter able to read registers during translate address and decode. | Kathy Gray | |
| This is not yet connected to any model and not yet tested. Also, reduce the number of parentheses needed by the parser. Namely, register declarations should no longer need parens around the types and let expressions should need fewer instances of parens around the expression (i.e. let a = exp ). | |||
| 2016-04-18 | More fixes to interp with regards to warnings and debugging info | Kathy Gray | |
| 2016-03-08 | Return undefined value on reads of uninitialised memory | Kathy Gray | |
| 2016-03-08 | Start task of setting up tagged memory in sequential interpreter | Kathy Gray | |
| 2016-02-02 | add translate_address functionality | Kathy Gray | |
| 2016-01-29 | fix typo in kathy's last commit. | Robert Norton | |
| 2016-01-29 | Put correct tags on to_vec calls | Kathy Gray | |
| 2016-01-28 | Support exit and assert better in sequential interpreter and general ↵ | Kathy Gray | |
| interpreter interface | |||
| 2016-01-26 | Fix some bugs in writing registers with slices in the sequential interpreter | Kathy Gray | |
| 2015-11-10 | Make first half of sequential interpreter driver compile again | Kathy Gray | |
| 2015-07-24 | Merge branch 'master' of bitbucket.org:Peter_Sewell/l2 | Shaked Flur | |
| 2015-07-24 | added signed_integer | Shaked Flur | |
| 2015-07-24 | Begin doing better analysis on case splits over unknowns | Kathy Gray | |
| 2015-07-19 | abbreviate printing of memory values <=9 | Peter Sewell | |
| 2015-07-01 | Go on despite the presence of an exit in exhaustive mode | Kathy Gray | |
| 2015-06-24 | Add new outcomes/events separating effective address and value for memory writes | Kathy Gray | |
| 2015-06-19 | one more end flag for memory_value functions | Kathy Gray | |
| 2015-06-18 | Add more end_flag parameters | Kathy Gray | |
| 2015-06-17 | Extend mode and external memory functions with endian flag | Kathy Gray | |
| 2015-06-16 | Incorporate comments from Peter. | Kathy Gray | |
| Add a flag type for endian, not used yet | |||
| 2015-06-09 | Fix error in building register values | Kathy Gray | |
| (make one function to do it instead of almost the same function multiple times) Fix lost nexp variable in constraints, removing another undefined | |||
| 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-18 | Add equality check for addresses | Kathy Gray | |
| And fix match failure problem (hopefully) | |||
| 2015-05-18 | Add comparison for address | Kathy Gray | |
| 2015-05-16 | Fix bug where undef was blown up to fill the full register on a field assignment | Kathy Gray | |
| 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-01 | Change interpreter interface to support ppcmem2's view of vectors as always ↵ | Kathy Gray | |
| increasing while supporting inc and dec views to the interpreter and in printing Fix bugs exposed by running idlarm several instructions (after fixing above) | |||
| 2015-03-19 | added constructors for aarch64 read_kind and write_kind | Shaked Flur | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |