summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2015-11-03Support int and bigint library functionsKathy Gray
2015-11-02Catch missing cumulative effect on setting local varKathy Gray
2015-10-29Ocaml generation now just needing big int/little int issues resolved ↵Kathy Gray
(probably) at least for Power.
2015-10-28progress on lem backend: auto-generate read_register and write_register ↵Christopher Pulte
functions, and state definition
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-26fixChristopher Pulte
2015-10-26Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2Christopher Pulte
2015-10-26add preliminary Sail_values.lem, adapt lem pp to recent Ocaml pp changesChristopher Pulte
2015-10-23slight change to libraryKathy Gray
2015-10-23More of sail correctly generating ocaml; including using polymorphic ↵Kathy Gray
variants when there are more than 246 constructors
2015-10-20add copies of ocaml-pp functions for lem-ppChristopher Pulte
2015-10-20ocaml output now produces parsing power.sailKathy Gray
2015-10-20more fixesKathy Gray
2015-10-20Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2Christopher Pulte
2015-10-20compiling prettyprinterKathy Gray
2015-10-20Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2Christopher Pulte
2015-10-20fix a-normalisation bugChristopher Pulte
2015-10-20Fixing bugs in pretty printer to ocamlKathy Gray
2015-10-19progress on lem backendChristopher Pulte
2015-10-17clean up, more readabilityChristopher Pulte
2015-10-17a-normalisation for lem backendChristopher Pulte
2015-10-13Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2Christopher Pulte
2015-10-13some progress on sequentialise_effectsChristopher Pulte
2015-10-13Refine local vs cumulative effects for lexpKathy Gray
More ocaml output, better treatment of registers.
2015-10-12fixesChristopher Pulte
2015-10-12apply rewriter changes to master as wellChristopher Pulte
2015-10-08augment annot of interpreterKathy Gray
2015-10-07Compiling again after refactoring. Haven't pushed to interpreter and lem yetKathy Gray
2015-10-07refactor type_internalKathy Gray
2015-10-07adapted pretty_print and rewriter to new tannot typeChristopher Pulte
2015-10-07Start expanding annot for more refined effect trackingKathy Gray
2015-10-07start changing representation of registers for ocamlKathy Gray
2015-10-06better printing for register writing, whole register (maybe not "right" yet)Kathy Gray
more library
2015-10-06added the preliminary lem output option that for now uses ocaml ppChristopher Pulte
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 ↵Christopher Pulte
vector_concat patterns, fixed a pp missing newline
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
Tweak to rewriter to actually rewrite function patterns
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 ↵Christopher Pulte
normalise_exp exp that should transform expressions into a form where they can be embedded into monadic lem or prover definitions. Both untested
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
Known todo: Write library functions in ocaml Properly upper-case/lower-case the first letter of names to conform to ocaml requirements Handle register aliases Turn id reads to dereferences for local ref variables
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 23:13:46 +0000