summaryrefslogtreecommitdiff
path: root/src/lem_interp
AgeCommit message (Collapse)Author
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-24Turn back off new analysis style until it worksKathy 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-20minor fixesKathy Gray
2015-07-19abbreviate printing of memory values <=9Peter Sewell
2015-07-02fix match_pattern reverse bugKathy 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-30Fix updating dec vector start bugsKathy Gray
2015-06-29Fix pattern match errorKathy Gray
2015-06-29Return unknown for a == unknown or unknown == a. Fixes issue #15Kathy 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 ↵Kathy Gray
and bit1); also fix some handling of wmv and eamem.
2015-06-24Support new write memory eventsKathy Gray
2015-06-24Support new memory write events in the sail front end and pretty printerKathy Gray
Events are eamem to signal the memory address to write to and wmv to pass the value to write
2015-06-24Add new outcomes/events separating effective address and value for memory writesKathy Gray
2015-06-22Fixes issue #12Kathy Gray
2015-06-21Taint printing changes: make it for debugging only, except when showing all ↵Kathy Gray
events in exhaustive mode
2015-06-19one more end flag for memory_value functionsKathy Gray
2015-06-18Add more end_flag parametersKathy Gray
2015-06-18Put reverse in the correct placeKathy Gray
2015-06-18add endian flag to memory printingKathy Gray
2015-06-18Consistent handling of constructors with no parametersKathy Gray
2015-06-17fix missed pattern caseKathy Gray
2015-06-17Extend mode and external memory functions with endian flagKathy Gray
2015-06-16Incorporate comments from Peter.Kathy Gray
Add a flag type for endian, not used yet
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-09Fix error in building register valuesKathy Gray
(make one function to do it instead of almost the same function multiple times) Fix lost nexp variable in constraints, removing another undefined
2015-06-08keeping tainted values in functionally updating recordsKathy Gray
2015-06-07Fix instruction extractorKathy Gray
2015-06-06append vectors with proper length for dec caseKathy Gray
2015-06-05Manually turn negative nat values to 0 instead of letting Lem use an abs ↵Kathy Gray
call to turn them positive, in to_vec*
2015-06-05Fix issue #5Kathy Gray
2015-06-05small variable renaming for Isabellecp526
2015-06-05slight change of binary_taint for Isabellecp526
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-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 ↵Kathy Gray
being very power-specific. Note: slight interface change to instruction_extractor
2015-05-28fix pattern matching bug on concatenated vectorsKathy Gray
2015-05-26small bug fixesKathy Gray
2015-05-19Merge branch 'master' of bitbucket.org:Peter_Sewell/l2Shaked Flur
2015-05-19avoid the use of Str.regexp as it breaks js_of_ocamlShaked Flur
2015-05-19Add signed and unsigned functions, converting bit vectors to appropriate ↵Kathy Gray
numbers (explicit instead of implicit in operations)
2015-05-18Match cases better in bit vector printing (i.e. allow undef, and taint)Kathy Gray
2015-05-18expand unsigned comparisonsKathy Gray