summaryrefslogtreecommitdiff
path: root/src/ast_util.mli
AgeCommit message (Expand)Author
2020-09-29Refactor: Change AST type from a union to a structAlasdair
2020-09-28Refactor: Rename 'a defs to 'a astAlasdair
2020-09-28Move the ast defs wrapper into it's own fileAlasdair
2020-08-13Preserve file structure through initial checkAlasdair
2020-05-15Add coverage tracking toolAlasdair
2019-11-29Merge branch 'word-numerals' into sail2Thomas Bauereiss
2019-08-02Fix all warnings (except for two lem warnings)Alasdair Armstrong
2019-05-17Experiment with making vector and bitvector distinct typesAlasdair Armstrong
2019-05-13move simple_string_of_loc to Ast_utilJon French
2019-04-15Merge branch 'sail2' into rmem_interpreterJon French
2019-04-05Lem: Make generated assertion messages look nicer in prover outputAlasdair
2019-04-02Coq: replace n_constraints with equivalent bool variablesBrian Campbell
2019-03-26Lem: Output constant bitvectors as hex or bin literalsThomas Bauereiss
2019-03-14Merge branch 'sail2' into rmem_interpreterJon French
2019-03-13Remove prover reference from typecheck env when marshalling out defsJon French
2019-03-11Improve ocamldoc commentsAlasdair Armstrong
2019-03-07Extract constant propagation and related functions from monomorphisation.Brian Campbell
2019-03-04Merge branch 'sail2' into rmem_interpreterJon French
2019-03-01WIP: Start working on being able to slice single instructions out of specsAlasdair Armstrong
2019-02-25Merge branch 'sail2' into rmem_interpreterJon French
2019-02-19Refactor specializationAlasdair Armstrong
2019-02-13Merge branch 'sail2' into rmem_interpreterJon French
2019-02-12Improvements for emacs modeAlasdair Armstrong
2019-02-08Add parameterization support for bitfields.Prashanth Mundkur
2019-02-08Updates for asl_parserAlasdair Armstrong
2019-02-07Replace equality check for declared effects by subset checkThomas Bauereiss
2019-02-03Merge branch 'sail2' into rmem_interpreterJon French
2019-01-29Merge branch 'sail2' into asl_flow2Thomas Bauereiss
2019-01-22Add a pragma for unrolling recursive functionsAlasdair Armstrong
2019-01-14Support some more unification casesThomas Bauereiss
2018-12-28Merge branch 'sail2' into rmem_interpreterJon French
2018-12-27refactor val-spec AST to store externs as an assoc-list rather than a functio...Jon French
2018-12-18Fix rewriter issuesAlasdair Armstrong
2018-12-17Changes for ASL parserAlasdair Armstrong
2018-12-12Generalise existentials for non-integer type variablesAlasdair
2018-12-12Remove KOpt_none constructorAlasdair
2018-12-12Fix various boolean type-variable related issuesAlasdair
2018-12-08Compiling againAlasdair
2018-12-07Working on better flow typing for ASLAlasdair Armstrong
2018-12-06Re-factor initial checkAlasdair Armstrong
2018-12-04Remove FES_Fexps constructorAlasdair Armstrong
2018-12-04Simplify kinds in the ASTAlasdair Armstrong
2018-11-16Canonicalise functions types in val specsAlasdair Armstrong
2018-11-05Ensure type-synonyms are handled correctly in register dependenciesAlasdair Armstrong
2018-11-01Changes to enable analysing type errors in ASL parserAlasdair Armstrong
2018-10-31Remove Parse_ast.Int, add unique locationsAlasdair Armstrong
2018-10-31Improve error messages for unsolved function quantifiersAlasdair Armstrong
2018-10-24Add constraint synonymsAlasdair Armstrong
2018-10-11Change the function type in the ASTAlasdair
2018-09-28Fix optimisation bug for certain if statementsAlasdair Armstrong