summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
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-16Fix omissions in nexp normalisation causing constraints not to be checked.Kathy Gray
Refine types of primitive functions to permit more constraints to be properly checked.
2015-06-15Fix strange resulting type for functions with val spec, favouring the ↵Kathy Gray
declared return type when consistent instead of using the derived one.
2015-06-10Make quantified types work in structs, resolving issue #7.Kathy Gray
2015-06-10Put missing cases into nexp_eq_checkKathy 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-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-04reduce number of unknown identifiers and get one step closer to actually ↵Kathy Gray
decoding an ARM instruction. (Note: may fix issue #2, haven't checked yet)
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
2015-05-18Add equality check for addressesKathy Gray
And fix match failure problem (hopefully)
2015-05-18Add comparison for addressKathy Gray
2015-05-17extend a missing caseKathy Gray
2015-05-16extend a missing caseKathy Gray
2015-05-16Fix bug where undef was blown up to fill the full register on a field assignmentKathy Gray
2015-05-16Fix vector field type annotation errorKathy Gray
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-05allow undefined in mask for sizeKathy Gray
2015-05-05continue moving closer to better Gt Lt constraint checksKathy Gray
2015-05-01Fix pattern match bug with enumerated valuesKathy Gray
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-04-22Fix some interpreter bugs preventing ARM instructions from making progressKathy Gray
2015-04-17remove old elf sourcesKathy Gray