summaryrefslogtreecommitdiff
path: root/src/rewriter.ml
AgeCommit message (Expand)Author
2016-01-21Start splitting values/etc into int/big_int for ocaml generationKathy Gray
2016-01-14small edit to previous commitKathy Gray
2016-01-14Fix cumulative effects for circumstance when lifting variable introductions o...Kathy Gray
2016-01-12Fix undefined nvar occurrences that were impacting ARMKathy Gray
2016-01-07Add E_assert to basic rewritersKathy Gray
2015-12-21fixes, pp progressChristopher
2015-12-16rewriter and pp changes for generating ARM outputChristopher
2015-12-15better location informationChristopher
2015-12-10fixChristopher
2015-12-09adapted for Kathy's lexp effect typing changes: register writes should be cor...Christopher
2015-11-25fixes, ppChristopher Pulte
2015-11-22do effect annotation updates more systematically, fix dedupChristopher Pulte
2015-11-20no more unecessary variables from removing vector-concatenation pattern match...Christopher Pulte
2015-11-19fixes for cumulative effect anotationsChristopher Pulte
2015-11-13fixes, more ppChristopher Pulte
2015-11-10fix case-expressions' newreturnChristopher Pulte
2015-11-10rewriting fixes, syntactically correct lem syntax, number type errors remainingChristopher Pulte
2015-11-07fixes, no more uncessary variables, pp progressChristopher Pulte
2015-11-06fixesChristopher Pulte
2015-11-06fixesChristopher Pulte
2015-11-05some progress on lem backend: rewrite away mutable variable assignments, rewr...Christopher Pulte
2015-11-04Add a new module for writing queries/analyses that aren't type checking but c...Kathy Gray
2015-10-29Ocaml generation now just needing big int/little int issues resolved (probabl...Kathy Gray
2015-10-28progress on lem backend: auto-generate read_register and write_register funct...Christopher Pulte
2015-10-26Switch name set to name map to include type and expression dataKathy Gray
2015-10-26Add variable set to rewritersKathy Gray
2015-10-26Begin if variable introduction rewritingKathy Gray
2015-10-20fix a-normalisation bugChristopher Pulte
2015-10-19progress on lem backendChristopher Pulte
2015-10-17clean up, more readabilityChristopher Pulte
2015-10-17a-normalisation for lem backendChristopher Pulte
2015-10-13some progress on sequentialise_effectsChristopher Pulte
2015-10-12fixesChristopher Pulte
2015-10-12apply rewriter changes to master as wellChristopher Pulte
2015-10-07adapted pretty_print and rewriter to new tannot typeChristopher Pulte
2015-10-06added the preliminary lem output option that for now uses ocaml ppChristopher 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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 11:23:19 +0000