summaryrefslogtreecommitdiff
path: root/src/lem_interp/interp_interface.lem
AgeCommit message (Expand)Author
2017-01-14changes to enable interpreter exhaustive analysis in ppcmem againChristopher Pulte
2016-12-01move interpreter-specific types from Sail_impl_base to Interp_interfaceChristopher Pulte
2016-11-27make outcome_s contain the instruction state pretty print rather than the ins...Christopher Pulte
2016-11-09move decode_error type back to Sail_impl_base for nowChristopher Pulte
2016-11-08fixesChristopher Pulte
2016-11-05fixesChristopher Pulte
2016-10-21shallow embedding progressChristopher Pulte
2016-10-06move type definitions that both interpreter and shallow embedding use to sail...Christopher Pulte
2016-09-30add Robert's DIA typeclass instancesChristopher Pulte
2016-09-30fixes, update isntruction_analysis for NIAs and DIAChristopher Pulte
2016-09-19remove conflict messageChristopher Pulte
2016-09-16make vector concatenation pattern removal deal with vector patterns of unknow...Christopher Pulte
2016-09-14Add memory kind for concurrent tag reads and writesKathy Gray
2016-09-13Add optional address to memv eventsKathy Gray
2016-09-13add show functions, fixChristopher Pulte
2016-09-09minor fixesKathy Gray
2016-09-09update instruction_analysis to support nias and instruction kindChristopher Pulte
2016-09-02Extend type checking so that patterns with vector concatenation don't permit ...Kathy Gray
2016-08-18move register_base_name and slice_of_reg_name from ppcmem thread semantics to...Christopher
2016-08-06Add duplicate_bits to libKathy Gray
2016-05-03Change decode and translate_address to support writing register events (altho...Kathy Gray
2016-04-25Make interpreter able to read registers during translate address and decode.Kathy Gray
2016-04-18More fixes to interp with regards to warnings and debugging infoKathy Gray
2016-03-08Return undefined value on reads of uninitialised memoryKathy Gray
2016-03-08Start task of setting up tagged memory in sequential interpreterKathy Gray
2016-02-02add translate_address functionalityKathy Gray
2016-01-29fix typo in kathy's last commit.Robert Norton
2016-01-29Put correct tags on to_vec callsKathy Gray
2016-01-28Support exit and assert better in sequential interpreter and general interpre...Kathy Gray
2016-01-26Fix some bugs in writing registers with slices in the sequential interpreterKathy Gray
2015-11-10Make first half of sequential interpreter driver compile againKathy Gray
2015-07-24Merge branch 'master' of bitbucket.org:Peter_Sewell/l2Shaked Flur
2015-07-24added signed_integerShaked Flur
2015-07-24Begin doing better analysis on case splits over unknownsKathy Gray
2015-07-19abbreviate printing of memory values <=9Peter Sewell
2015-07-01Go on despite the presence of an exit in exhaustive modeKathy Gray
2015-06-24Add new outcomes/events separating effective address and value for memory writesKathy Gray
2015-06-19one more end flag for memory_value functionsKathy Gray
2015-06-18Add more end_flag parametersKathy Gray
2015-06-17Extend mode and external memory functions with endian flagKathy Gray
2015-06-16Incorporate comments from Peter.Kathy Gray
2015-06-09Fix error in building register valuesKathy Gray
2015-06-02changes to compare and equality instances to make lem generate isabelle outputcp526
2015-06-02Fix errors around ARM not being able to decode due to instruction_extractor b...Kathy Gray
2015-05-18Add equality check for addressesKathy Gray
2015-05-18Add comparison for addressKathy Gray
2015-05-16Fix bug where undef was blown up to fill the full register on a field assignmentKathy Gray
2015-05-13Add dynamic footprint dependency check event/outcomeKathy Gray
2015-05-01Change interpreter interface to support ppcmem2's view of vectors as always i...Kathy Gray
2015-03-19added constructors for aarch64 read_kind and write_kindShaked Flur