summaryrefslogtreecommitdiff
path: root/src/rewriter.ml
AgeCommit message (Expand)Author
2017-08-24Avoid re-typechecking after rewriting passesThomas Bauereiss
2017-08-24Add some missing type annotationsThomas Bauereiss
2017-08-23Started work on an undefined literal removal pass for the ocamlAlasdair Armstrong
2017-08-22Type quantification elimination working for hexapod specAlasdair Armstrong
2017-08-22More work on quantifier eliminationAlasdair Armstrong
2017-08-21More work on quantifier elimination passAlasdair Armstrong
2017-08-21Modified sizeof rewriting pass so it can correctly deal with existentials.Alasdair Armstrong
2017-08-18Fixed a bug where sizeof re-writing fail for aliased type argumentsAlasdair Armstrong
2017-08-17Work on E_constraint removal pass and diagnosing bugs in E_sizeof removal passAlasdair Armstrong
2017-08-17Add E_constraint support to re-writerAlasdair Armstrong
2017-08-17Various sail fixes for ASL hexapodAlasdair Armstrong
2017-08-15Improve and simplify handling of mutable local variablesThomas Bauereiss
2017-08-10Add support for early return to Lem backendThomas Bauereiss
2017-08-08Various fixes and improvements for the Lem pretty-printingThomas Bauereiss
2017-08-02Improve pretty-printing of register declaration and assignmentThomas Bauereiss
2017-08-02Add debugging option to dump AST after rewriting stepsThomas Bauereiss
2017-08-01Fix some effect propagation bugs in rewriterThomas Bauereiss
2017-07-27Rewrite guarded patterns for Lem backendThomas Bauereiss
2017-07-27Add cons patterns to pretty-printersThomas Bauereiss
2017-07-26Improve rewriting of sizeof expressionsThomas Bauereiss
2017-07-25Add partial support for rewriting of sizeof expressionsThomas Bauereiss
2017-07-24Added cons patterns to sailAlasdair Armstrong
2017-07-21Everything moved to new typecheckerAlasdair Armstrong
2017-07-21Switch to new typechecker (almost)Thomas Bauereiss
2017-07-12Add checks for variable identifiers in pattern subsumptionThomas Bauereiss
2017-07-03Cleanup, and add support for variable bindings in bitvector patternsThomas Bauereiss
2017-06-29Rewrite bitvector patternsThomas Bauereiss
2017-03-24Checkpoint work-in-progress mips sequential interpreter using ocaml shallow e...Robert Norton
2017-03-24changes to ocaml pp to allow mips->ocaml to compileRobert Norton
2017-02-03fix headersPeter Sewell
2016-11-08fixesChristopher Pulte
2016-10-27more shallow embedding fixesChristopher Pulte
2016-10-26shallow embedding fixesChristopher Pulte
2016-10-13make sail-to-lem rewriting passes use dependency analysis, make dependency an...Christopher Pulte
2016-10-10changed the way registers/register fields work, fixes, nicer names for new le...Christopher Pulte
2016-09-26nicer lem output: fewer unnecessary letbinds, monad binds and returnsChristopher Pulte
2016-09-25nicer lem output: no more unecessary 'unit' returns if if-expressions, for-lo...Christopher Pulte
2016-09-24nicer lem output: fewer unecessary 'return'sChristopher Pulte
2016-09-19sail-to-lem progressChristopher Pulte
2016-09-16fixChristopher Pulte
2016-09-16make vector concatenation pattern removal deal with vector patterns of unknow...Christopher Pulte
2016-09-07push some lem pp changesChristopher Pulte
2016-08-14Start adding form for (a,b,c) := foo()Kathy Gray
2016-08-10Fix sizeof code generation to look at parameter boundsKathy Gray
2016-07-23Add a return exp form to Sail, supported in type checker and in interpreter.Kathy Gray
2016-07-20Make rewriter understand type abbreviations for removing internal_exp instancesKathy Gray
2016-05-27Add sizeof to sail. Documentation to followKathy Gray
2016-03-02Add new language feature to permit definitions of items of kind Nat, etc as w...Kathy Gray
2016-01-26move closer to power.sail -> power.ml outputKathy Gray
2016-01-21Start splitting values/etc into int/big_int for ocaml generationKathy Gray
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 12:36:55 +0000