summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2015-09-25building version of last change, removing stray )Kathy Gray
2015-09-25Rewrite expressions for ocaml, lifting assignment introductions into a ↵Kathy Gray
special let form to set the scope
2015-09-24Beginning of expression rewriter for ocamlKathy Gray
2015-09-24basic pattern rewriterKathy Gray
2015-09-24Parameterise the rewriter's for multiple different rewritingsKathy Gray
Add a new internal node for moving assignments into scope-preserving expressions that more explicitly define the scope
2015-09-24added 'remove_vector_string_patterns and .._expressions functionsChristopher Pulte
2015-09-23More pretty printingKathy Gray
A few more expressive tags for introducing mutable variables and for tracking local mutations A new pred for detecting bit vectors
2015-09-22Start pretty printing ocaml for sequentialKathy Gray
2015-09-17Type checker checking on case splits properly, and dependency ↵Kathy Gray
transformations restored :)
2015-09-06Turn off debug print outsKathy Gray
2015-09-06Improved type system, so that it catches int where there should be natKathy Gray
Note: the resulting Lem file generated may or may not actually work properly with the interpreter (i.e. it might have too many unknowns); still in the process of debugging some changes there.
2015-08-18Make register fields with concatenated ranges compile nowKathy Gray
2015-08-14Steps towards making constraint solver smarterKathy 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-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-30Change rewriter to better reset dec vectors to count from (length - 1) ↵Kathy Gray
instead of whatever random spot they might be in, where functions expect length-n to 0
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-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