summaryrefslogtreecommitdiff
path: root/src/process_file.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-21Add reformat option to SailAlasdair
2020-08-13Preserve file structure through initial checkAlasdair
2020-06-10Prepare Coq library for packagingBrian Campbell
2020-04-14Add add_symbol to the API of Process_fileAlasdair
2019-11-11Update libsail slightly with recent changesAlasdair Armstrong
2019-11-11Make sure we include LEXP_cast register refs when slicing the specificationAlasdair Armstrong
2019-08-22additional option to tweak Coq output to support user-defined monad:pes20
2019-08-20add -coq_alt_modules option to override the default imported modulespes20
2019-08-01Merge branch 'sail2' into separate_bvAlasdair Armstrong
2019-07-18Add a option to check for a feature symbolAlasdair Armstrong
2019-07-18Add a feature flag for barrier type changeAlasdair Armstrong
2019-07-16Merge remote-tracking branch 'origin/sail2' into separate_bvAlasdair Armstrong
2019-06-19Rewriting improvements for monomorphic aarch64_smallBrian Campbell
2019-06-04Merge branch 'sail2' into separate_bvAlasdair Armstrong
2019-05-22Move Util.warn to Reporting, and make it take the location as a parameterAlasdair Armstrong
2019-05-17Experiment with making vector and bitvector distinct typesAlasdair Armstrong
2019-05-16Fix: Add a feature symbol for new constant type variable syntaxAlasdair Armstrong
2019-05-14Fix: Issue a warning for any unrecognised directiveAlasdair Armstrong
2019-04-06Various bugfixes and improvementsAlasdair
2019-03-27Interactive: Refactor sail.mlAlasdair Armstrong
2019-02-18Add option to linearize constraints containing exponentialsAlasdair Armstrong
2019-02-08Rewrite type definitions in rewrite_nexp_idsThomas Bauereiss
2019-02-07Add a symbol for new implicit arguments for backwards compatabilityAlasdair Armstrong
2019-02-06Emacs mode understands relationships between Sail filesAlasdair
2019-02-06Improve emacs modeAlasdair Armstrong
2019-01-29Merge branch 'sail2' into asl_flow2Thomas Bauereiss
2019-01-21Add output directory option for generated Isabelle auxiliary theoriesThomas Bauereiss
2019-01-17Work around an issue with type abbreviations in HOLThomas Bauereiss
2019-01-14Add options for output directories for the lem and coq backends.Prashanth Mundkur
2019-01-11Updates for sail-arm releaseAlasdair Armstrong
2018-12-26More cleanupAlasdair Armstrong
2018-12-22Improve error messages and debuggingAlasdair Armstrong
2018-12-20Make sure sail -v prints useful version infoAlasdair Armstrong
2018-12-06Re-factor initial checkAlasdair Armstrong
2018-11-19Merge branch 'latex' into sail2Robert Norton
2018-11-16Various bugfixes and a simple profiling feature for rewritesAlasdair Armstrong
2018-11-09Improvements to latex generationAlasdair Armstrong
2018-10-31Rename Reporting_basic to ReportingAlasdair Armstrong
2018-09-13Coq: real built-ins for AArch64Brian Campbell
2018-09-12Jenkins: Fix deprecation warningsAlasdair Armstrong
2018-09-06Allow options to be set in the interactive modeAlasdair Armstrong
2018-09-04Improve error messages for include and ifdef statementsAlasdair Armstrong
2018-08-10Coq: add some of string libraryBrian Campbell
2018-08-07Revert "Warnings: deal with all the deprecation warnings"Alasdair Armstrong
2018-07-26Warnings: deal with all the deprecation warningsAlastair Reid
2018-07-25Remove unused internal AST nodesAlasdair Armstrong