summaryrefslogtreecommitdiff
path: root/src/lem_interp/interp_inter_imp.lem
AgeCommit message (Expand)Author
2019-07-31Revert "Need to separate out the 0.10 lem library from upcoming 0.11"Alasdair Armstrong
2019-07-18Need to separate out the 0.10 lem library from upcoming 0.11Alasdair Armstrong
2019-07-18Support DMB/DSB domainsShaked Flur
2018-02-17Merge master branch into sail2 for OCaml 4.06 compatibilityThomas Bauereiss
2018-02-08replaced NIA_LR/CTR/register with NIA_indirect;Shaked Flur
2017-12-05Update header files on masterAlasdair Armstrong
2017-12-05Update license headers for Sail sourceAlasdair Armstrong
2017-11-30Merge branch 'master' into experimentsAlasdair Armstrong
2017-11-29Better lem_ast tagging and interpreter tweaksAlasdair Armstrong
2017-11-17Fix interpreter to work with new typecheckerAlasdair Armstrong
2017-10-09add translations for missing read/write kinds.Robert Norton
2017-10-09add translation of IK_mem_rmw interp_inter_imp. TODO: could we get rid of thi...Robert Norton
2017-10-06move nias_of_instruction into RMEM so that it can use shallow embedding ast a...Robert Norton
2017-09-29fix deep_shallow_convert, stop using interp_interface.instruction for most th...Christopher Pulte
2017-09-15x86: implement regfp analysis function (no control flow yet)Robert Norton
2017-08-31added RISC-V AMOsShaked Flur
2017-08-22added RISC-V "fence w,w" and "fence.i";Shaked Flur
2017-07-24interpreter: optionally print debugging tracesJon French
2017-07-24move value type definitions to ott, and introduce new E_internal_value ast no...Jon French
2017-05-28fixed exmemShaked Flur
2017-05-24Merge branch 'master' of bitbucket.org:Peter_Sewell/sailShaked Flur
2017-05-24added the exmem effect for AArch64 store-exclusiveShaked Flur
2017-05-24Change types of MEMr_tag, MEMval_tag and co. so that tag is separate from dat...Robert Norton
2017-04-18added transactional memory supportShaked Flur
2017-04-03Rename TranslateAddress to TranslatePC and remove the accessType argument -- ...Robert Norton
2017-03-24Print tracking information for V_track, hopefully fix extern_vector_value, fi...Christopher Pulte
2017-03-23the interpreter/shallow expects little-endian memory-valuesShaked Flur
2017-02-03fix headersPeter Sewell
2017-01-26christopher, kathy, peter: hacky experiment on nias_of_instructionPeter Sewell
2017-01-24functionality for comparing handwritten analysis function with exhaustive int...Christopher Pulte
2017-01-14changes to enable interpreter exhaustive analysis in ppcmem againChristopher Pulte
2016-12-09sail changes for making lem embedding Isabelle-friendlierChristopher Pulte
2016-12-01move interpreter-specific types from Sail_impl_base to Interp_interfaceChristopher Pulte
2016-11-30add new barrier kind for MIPS (only one for now).Robert Norton
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-07factor out regfp analysis types into etc/regfp.sailChristopher Pulte
2016-10-25fix my decode_to_istate bugChristopher Pulte
2016-10-21shallow embedding progressChristopher Pulte
2016-10-20factor out instr_external_to_interp_valueChristopher Pulte
2016-10-20fix previous FromToInterpValue typeclass issue, factor out intpreter's interp...Christopher Pulte
2016-10-19fixChristopher Pulte
2016-10-19remove effect list from instruction typeChristopher Pulte
2016-10-06move type definitions that both interpreter and shallow embedding use to sail...Christopher Pulte
2016-09-30fixes, update isntruction_analysis for NIAs and DIAChristopher Pulte
2016-09-21fixesChristopher Pulte
2016-09-13Add optional address to memv eventsKathy Gray
2016-09-13add show functions, fixChristopher Pulte
2016-09-13extern slice for instruction analysisKathy Gray
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:39:12 +0000