summaryrefslogtreecommitdiff
path: root/src/lem_interp/interp_inter_imp.lem
AgeCommit message (Expand)Author
2015-10-08augment annot of interpreterKathy Gray
2015-08-06Update analysis to merge states and values after branches taken due to unknow...Kathy Gray
2015-07-24Begin doing better analysis on case splits over unknownsKathy Gray
2015-07-01fix equality comparisonKathy Gray
2015-07-01Use set instead of list for tainted valuesKathy Gray
2015-07-01Go on despite the presence of an exit in exhaustive modeKathy Gray
2015-06-28Tag enumeration variables properly when introducing themKathy Gray
2015-06-26Better handling of literal true and false (turn them into the expected bit0 a...Kathy Gray
2015-06-24Support new write memory eventsKathy Gray
2015-06-24Add new outcomes/events separating effective address and value for memory writesKathy Gray
2015-06-22Fixes issue #12Kathy Gray
2015-06-18Consistent handling of constructors with no parametersKathy Gray
2015-06-17Extend mode and external memory functions with endian flagKathy Gray
2015-06-09Too hasty removal; still used by trans_sail.genKathy Gray
2015-06-09remove superfluous num_to_bits; replaced by bit_list_of_integerKathy Gray
2015-06-09support exit/escape out of the interfaceKathy Gray
2015-06-07Fix instruction extractorKathy Gray
2015-06-02Fix errors around ARM not being able to decode due to instruction_extractor b...Kathy 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-04-22Fix some interpreter bugs preventing ARM instructions from making progressKathy Gray
2015-03-18Use boolean on write where applicableKathy Gray
2015-03-17Correct directionality in interpreter. Now the interpreter shouldn't use inc ...Kathy Gray
2015-03-15Many changes:Kathy Gray
2015-02-27Fix a series of errors leading to the first ARM instruction not running.Kathy Gray
2014-12-11Many fixes, primarily dealing with undefinedKathy Gray
2014-12-10Fix mismatch errors in interpreter, mostly relating to taint/detaint behaviourKathy Gray
2014-11-23make interpreter work better with unknowns, make interp_inter_imp do better o...Kathy Gray
2014-11-23Merge branch 'master' of bitbucket.org:Peter_Sewell/l2Peter Sewell
2014-11-23the properly named "git"Peter Sewell
2014-11-23extern single bit and single bool to instruction_fieldsKathy Gray
2014-11-23Fill in some of the basic coercionsKathy Gray
2014-11-23clean up interp interKathy Gray
2014-11-23more coercionsPeter Sewell
2014-11-23OCaml stubs for coercions and _to_istate OCamlPeter Sewell
2014-11-23wib (comment out to typecheck the rest...)Peter Sewell
2014-11-23fight with interface/impl mismatch. lose.Peter Sewell
2014-11-23update instruction/istate decoding.Kathy Gray
2014-11-22interp_interface happy again. printing functions now doesn't compileKathy Gray
2014-11-22Add size of register to register for making appropriate unknown register_valuesKathy Gray
2014-11-22Changing interface in step with Peter and ppcmem changesKathy Gray
2014-11-21Support signed and unsigned arithmeticKathy Gray
2014-11-21Fix bugs now documented in ppcmem notesKathy Gray
2014-11-20look for sub matches of registers on exhaustive modeKathy Gray
2014-11-19add byte_list_of_integerKathy Gray
2014-11-19Correct off-by-one bug in type checking vector slicesKathy Gray
2014-11-18Actually expect barriers to happenKathy Gray
2014-11-18Fix countLeadingZeroes typo (diff in number of es present)Kathy Gray
2014-11-16Add some missing functionsKathy Gray
2014-11-16Add overflow checking arithmetic operations. Fix various bugs that this exposedKathy Gray
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 11:27:36 +0000