summaryrefslogtreecommitdiff
path: root/src/ast_util.ml
AgeCommit message (Expand)Author
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
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-11Fix all tests with type checking changesAlasdair Armstrong
2018-12-10Various changes:Alasdair Armstrong
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-30Remove constraint synonymsAlasdair Armstrong