summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2015-07-24added signed_integerShaked Flur
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-30Change rewriter to better reset dec vectors to count from (length - 1) instea...Kathy 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 a...Kathy Gray
2015-06-24Support new write memory eventsKathy Gray
2015-06-24Support new memory write events in the sail front end and pretty printerKathy Gray
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 e...Kathy Gray
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
2015-06-16Fix omissions in nexp normalisation causing constraints not to be checked.Kathy Gray
2015-06-15Fix strange resulting type for functions with val spec, favouring the declare...Kathy Gray
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
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 call...Kathy Gray
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 deco...Kathy Gray
2015-06-03make string functions used to UI and debugging output empty strings for theor...cp526
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 b...Kathy Gray
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 numb...Kathy Gray