summaryrefslogtreecommitdiff
path: root/src/ast_util.ml
AgeCommit message (Expand)Author
2020-09-29Include comments in AST typeAlasdair
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
2020-03-18Expose details of failed lexp bounds checksThomas Bauereiss
2020-01-28Fix a bug with lexp->exp conversion for register referencesAlasdair
2020-01-16Allow effects on mappingsAlasdair Armstrong
2019-11-29Merge branch 'word-numerals' into sail2Thomas Bauereiss
2019-11-11Make sure we include LEXP_cast register refs when slicing the specificationAlasdair Armstrong
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-26Lem: Output constant bitvectors as hex or bin literalsThomas Bauereiss
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:39:12 +0000