summaryrefslogtreecommitdiff
path: root/src/pretty_print.ml
AgeCommit message (Expand)Author
2015-11-05some progress on lem backend: rewrite away mutable variable assignments, rewr...Christopher Pulte
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-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-23More of sail correctly generating ocaml; including using polymorphic variants...Kathy Gray
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-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
2015-10-07Compiling again after refactoring. Haven't pushed to interpreter and lem yetKathy Gray
2015-10-07adapted pretty_print and rewriter to new tannot typeChristopher Pulte
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
2015-10-05made vector_concat pass remove typ annotation expression inside vector_concat...Christopher 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-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-24Parameterise the rewriter's for multiple different rewritingsKathy Gray
2015-09-23More pretty printingKathy Gray
2015-09-22Start pretty printing ocaml for sequentialKathy 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-06-24Support new memory write events in the sail front end and pretty printerKathy Gray
2015-06-10Put missing cases into nexp_eq_checkKathy Gray
2015-06-02Fix errors around ARM not being able to decode due to instruction_extractor b...Kathy Gray
2015-05-28fix pattern matching bug on concatenated vectorsKathy Gray
2015-05-13Add dynamic footprint dependency check event/outcomeKathy Gray
2015-03-26Add subtraction to nexp grammar (removing the need to do a + (-1 * b))Kathy Gray
2015-02-24Fix lem printingKathy Gray
2015-02-13Actually use new dependency information in generation of lem/etc.Kathy Gray