summaryrefslogtreecommitdiff
path: root/src/lem_interp/interp_utilities.lem
AgeCommit message (Collapse)Author
2015-10-08augment annot of interpreterKathy Gray
2015-08-06Update analysis to merge states and values after branches taken due to ↵Kathy Gray
unknown conditions. Does not merge if one path has resulted in an exit
2015-07-24Begin doing better analysis on case splits over unknownsKathy Gray
2015-06-24Support new write memory eventsKathy Gray
2015-06-03make string functions used to UI and debugging output empty strings for ↵cp526
theorem provers, use structural (in)equality for Isabelle and HOL for literals and values
2015-06-02Fix 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-15actually match depend effect in has_effect functionKathy Gray
2015-05-13Add dynamic footprint dependency check event/outcomeKathy Gray
Also fix type checker bug in not reporting modifications to parameter values
2015-05-01Change 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-15Many changes:Kathy Gray
Split out specification specific memory and external functions Reduce the presence of big_int Reduce the use of inc direction, instead using a default from the spec. Still a few places need to be parameterised over direction Also some bug fixes exposed by above and running ARM second instruction
2014-11-23make interpreter now buildsKathy Gray
and I *think* that I'm making vectors of unknowns in all the necessary places now.
2014-11-20set more vector starts before sending them off to register writesKathy Gray
2014-10-07Actually add the new fileKathy Gray