summaryrefslogtreecommitdiff
path: root/src/lem_interp/run_interp_model.ml
AgeCommit message (Expand)Author
2017-12-05Update license headers for Sail sourceAlasdair Armstrong
2017-11-29Better lem_ast tagging and interpreter tweaksAlasdair Armstrong
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-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-03-24Christopher, Peter: make "run_interp_model.ml" build again (endianness)Peter Sewell
2017-02-03fix headersPeter Sewell
2016-10-17updates for ppcmem printingKathy Gray
2016-10-06move type definitions that both interpreter and shallow embedding use to sail...Christopher Pulte
2016-09-14Add memory kind for concurrent tag reads and writesKathy Gray
2016-09-14Change reading and writing of tag memory to report the tag/look for the tag a...Kathy Gray
2016-09-13Support memea and memv in sequential interpreterKathy Gray
2016-07-28Banish exit from the mips/cheri sail except at end of SignalException functio...Robert Norton
2016-06-07Fix issue in accessing fields and slices of registers during translate addressKathy Gray
2016-06-03Fix bug exposed/introduced by properly handling vector starts in the type che...Kathy Gray
2016-04-25Make interpreter able to read registers during translate address and decode.Kathy Gray
2016-03-08missing file from last commitKathy Gray
2016-03-08Start task of setting up tagged memory in sequential interpreterKathy Gray
2016-01-28Support exit and assert better in sequential interpreter and general interpre...Kathy Gray
2016-01-27Make mips build againKathy Gray
2016-01-26Fix some bugs in writing registers with slices in the sequential interpreterKathy Gray
2016-01-26Fix problem in run_with_model where we forgot that ppcmem2 treats everything ...Kathy Gray
2016-01-20see writes to registers in the register file for sequential interpreterKathy Gray
2016-01-20Assorted bug fixes that gets one mips instruction running (then fails for exp...Kathy Gray
2015-11-17Very nearly there sequential interpreter, just need to hook in the spec files...Kathy Gray
2015-11-12Incorporating elf into sequential interpreterKathy Gray
2015-11-10Make first half of sequential interpreter driver compile againKathy Gray
2015-04-22Fix some interpreter bugs preventing ARM instructions from making progressKathy Gray
2014-11-17Use red printing for the value in the hole from Printing_functions instead of...Kathy Gray
2014-11-06Refactor printing to display the contents the [_] and to better format bit ve...Kathy Gray
2014-11-04Fix setting of initial position in a vector after a sliceKathy Gray
2014-10-30Add parameter to interp_exhaust with type maybe (list (reg_name,value)) for r...Kathy Gray
2014-10-27Correct externally visible endianness bugsKathy Gray
2014-10-20Separate out printing facility from model driver into printing_functions int...Kathy Gray
2014-10-14Iron out bugs in running new executable with branching; add new executable as...Kathy Gray
2014-10-07kathy,peter: making decode integration with ppcmem2 typecheckPeter Sewell
2014-10-07Put in type for instruction form for models; remove extra information from By...Kathy Gray
2014-09-30Corrected writing to register bug. Now interpreter produces same result as gd...Kathy Gray
2014-08-27Changes to get another (slightly larger) executable running;Kathy Gray
2014-08-21Improve printing of function calls in stepper modeKathy Gray
2014-08-21Allow command line interface to exhaustively evaluate the next step, printing...Kathy Gray
2014-08-20Add ability to track register dependencies in interactive stepper; thus testi...Kathy Gray
2014-08-19make test_power_interactive working again; now using interp_interface instead...Kathy Gray
2014-08-19Add file that actually drives command line interpreterKathy Gray