summaryrefslogtreecommitdiff
path: root/src/pretty_print_lem.ml
AgeCommit message (Expand)Author
2017-10-26Experiment with pretty-printing non-atomic nexps in LemThomas Bauereiss
2017-10-25Allow mutually recursive functionsThomas Bauereiss
2017-10-24Print type annotations in Lem with type variablesBrian Campbell
2017-10-24Limit quantifiers printed in Lem to type variables that actuallyBrian Campbell
2017-10-24Handle existential types in Lem backend by stripping them andBrian Campbell
2017-10-24Remove special case for boolean (as opposed to bool)Brian Campbell
2017-10-23Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-10-19Fix pretty-printing of type abbreviation definitions with argumentsThomas Bauereiss
2017-10-19Mangle names with '#' characters in Lem pretty-printingThomas Bauereiss
2017-10-19Rewrite undefined values, add type annotations to early returnsThomas Bauereiss
2017-10-19Follow AST changes in (Lem) pretty-printersThomas Bauereiss
2017-10-18Merge branch 'experiments' of Peter_Sewell/sail into mono-experimentsBrian Campbell
2017-10-13Fix some bugs that surfaced in the ASL exportThomas Bauereiss
2017-10-13Name (bit)vector operations more explicitlyThomas Bauereiss
2017-10-13Add support for real numbers to Lem backendThomas Bauereiss
2017-10-13Improve debugging outputThomas Bauereiss
2017-10-06Produce type signatures in Lem outputBrian Campbell
2017-10-04Merge branch 'cleanup' into experimentsAlasdair Armstrong
2017-10-03Fixes to new parserAlasdair Armstrong
2017-09-29Support vector registers (other than bitvectors)Thomas Bauereiss
2017-09-29Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into experimentsThomas Bauereiss
2017-09-29Some more refactoring of Sail libraryThomas Bauereiss
2017-09-27Add while-loops to Lem backendThomas Bauereiss
2017-09-21Refactored AST valspecs into single constructorAlasdair Armstrong
2017-09-21Simplify AST by removing LB_val_explicit and replace LB_val_implicit with jus...Alasdair Armstrong
2017-09-21Cleaning up the AST and removing redundant and/or unused nodesAlasdair Armstrong
2017-09-14Fix some more test casesThomas Bauereiss
2017-09-14Fix a regression when writing to a register via a reference in a vector such ...Thomas Bauereiss
2017-09-02Various fixes for HexapodThomas Bauereiss
2017-09-02Remove dependency of state.lem on bitvector operationsThomas Bauereiss
2017-08-29Make Lem export of CHERI(-256) typecheckThomas Bauereiss
2017-08-24Begin refactoring Sail libraryThomas Bauereiss
2017-08-18Fixed a bug where sizeof re-writing fail for aliased type argumentsAlasdair Armstrong
2017-08-17Add support for register types other than bitvector to state monadThomas Bauereiss
2017-08-15Removed Typ_arg_effect - nobody used it and it isn't supported by the backends.Alasdair 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-09Pretty-print some more type annotationsThomas Bauereiss
2017-08-08Fix Lem bindings in test casesThomas 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-01Remove some hardcoded calls to obsolete Lem library functionsThomas 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-21Everything moved to new typecheckerAlasdair Armstrong
2017-07-21Switch to new typechecker (almost)Thomas Bauereiss
2017-07-12Add annotations to raw bitvector slicesThomas Bauereiss
2017-06-21Pretty-print bitvector expressionsThomas Bauereiss