summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2015-10-06fix generated message to have correct file extensionChristopher Pulte
2015-10-06Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2Christopher Pulte
2015-10-06fixesChristopher Pulte
2015-10-06make let and case actually call pattern rewriterKathy Gray
2015-10-05made vector_concat pass remove typ annotation expression inside vector_concat...Christopher Pulte
2015-10-05some fixesChristopher Pulte
2015-10-05Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2Christopher Pulte
2015-10-05added pattern rewriting for DEF_val expressionsChristopher Pulte
2015-10-05More library functionsKathy Gray
2015-10-05added funcl pattern rewriting to remove vector concat patternsChristopher Pulte
2015-10-04add find_updated_vars to support for-loops for lem or prover backend, add nor...Christopher Pulte
2015-09-30Alias support for ocaml modeKathy Gray
2015-09-29capitalise and uncapitalise according to ocaml requirementsKathy Gray
2015-09-29ml output passing simple test suite, except for register aliasesKathy Gray
2015-09-29Boiler plate to generate an ml file from a sail spec. Now debugging the outpu...Kathy Gray
2015-09-28for loop variant without closure requiredKathy Gray
2015-09-28basic untested ocaml boiler plateKathy Gray
2015-09-28Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2Christopher Pulte
2015-09-28completed pp for E_for expressions, necessary OCaml foreach_inc and foreach_d...Christopher Pulte
2015-09-28Add initial support for register fieldsKathy Gray
2015-09-28tweak what the output expectsKathy Gray
2015-09-28added rewriter rewrite_defs_remove_vector_concat that should get rid of vecto...Christopher Pulte
2015-09-25added something for remove_vector_string_patterns that for a give pattern-mat...Christopher Pulte
2015-09-25added something for remove_vector_string_patterns that for a give pattern-mat...Christopher Pulte
2015-09-25Potentially working ocaml mode, minus registers with fields, awaiting pattern...Kathy Gray
2015-09-25building version of last change, removing stray )Kathy Gray
2015-09-25Rewrite expressions for ocaml, lifting assignment introductions into a specia...Kathy Gray
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
2015-09-24added 'remove_vector_string_patterns and .._expressions functionsChristopher Pulte
2015-09-23More pretty printingKathy Gray
2015-09-22Start pretty printing ocaml for sequentialKathy Gray
2015-09-17Type checker checking on case splits properly, and dependency transformations...Kathy Gray
2015-09-06Turn off debug print outsKathy Gray
2015-09-06Improved type system, so that it catches int where there should be natKathy Gray
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 unknow...Kathy Gray
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) instea...Kathy Gray
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 03:14:50 +0000