summaryrefslogtreecommitdiff
path: root/src/ast_util.ml
AgeCommit message (Expand)Author
2019-08-05Print effect sets in alphabetical orderAlasdair Armstrong
2019-08-02Fix all warnings (except for two lem warnings)Alasdair Armstrong
2019-07-16Merge remote-tracking branch 'origin/sail2' into separate_bvAlasdair Armstrong
2019-06-13Add AST for greater-than and less-than constraintsBrian Campbell
2019-06-10Add well-formedness check for type schemes in valspecs.Brian Campbell
2019-06-04Merge branch 'sail2' into separate_bvAlasdair Armstrong
2019-06-04Remove unused AST constructorAlasdair Armstrong
2019-05-21Lem: Fix bug in generation of val-specsThomas Bauereiss
2019-05-17Experiment with making vector and bitvector distinct typesAlasdair Armstrong
2019-05-14Add feature that allows functions to require type variables are constantAlasdair Armstrong
2019-05-13move simple_string_of_loc to Ast_utilJon French
2019-04-25Fill in missing map_..._annot caseBrian Campbell
2019-04-15Merge branch 'sail2' of github.com:rems-project/sail into sail2Jon French
2019-04-15Merge branch 'sail2' into rmem_interpreterJon French
2019-04-15Basic loop termination measures for CoqBrian Campbell
2019-04-06Various bugfixes and improvementsAlasdair
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-19Don't expand set constraints when substituting vars for varsBrian Campbell
2019-03-14Merge branch 'sail2' into rmem_interpreterJon French
2019-03-13Debugging: string_of_value internal values in string_of_expJon 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-02-25Merge branch 'sail2' into rmem_interpreterJon French
2019-02-21Fix specialization bug involving function annotations not matching valspecsAlasdair
2019-02-19Refactor specializationAlasdair Armstrong
2019-02-18Add option to linearize constraints containing exponentialsAlasdair Armstrong
2019-02-14Fix a bug that caused constant propagation option to fail for v8.5Alasdair Armstrong
2019-02-14Don't do any rewrites when checking files for EmacsAlasdair 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-04Fix some warningsAlasdair Armstrong
2019-02-03Merge branch 'sail2' into rmem_interpreterJon French
2019-02-02Merge remote-tracking branch 'origin/sail2' into asl_flow2Alasdair
2019-01-31Add missing cases to constraint comparisonBrian Campbell
2019-01-29Merge branch 'sail2' into asl_flow2Thomas Bauereiss
2019-01-22Add a pragma for unrolling recursive functionsAlasdair Armstrong
2019-01-11Updates for sail-arm releaseAlasdair Armstrong
2019-01-08Improvements for v85Alasdair Armstrong
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-26More cleanupAlasdair Armstrong
2018-12-19Improve sizeof rewriting performanceAlasdair Armstrong
2018-12-18Fix rewriter issuesAlasdair Armstrong
2018-12-17Changes for ASL parserAlasdair Armstrong
2018-12-12Add a test case for various simple boolean propertiesAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 07:19:48 +0000