summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2019-01-29Monomorphisation: restrict our attention to Int kidsBrian Campbell
2019-01-25Coq: add enough to generate some output for arm-v8.5-aBrian Campbell
2019-01-24Start supporting informative bool types in Coq backendBrian Campbell
2019-01-24Make recheck_defs_without_effects restore old flag properlyBrian Campbell
2019-01-23Make rewriting of E_assign a bit more robustThomas Bauereiss
2019-01-23Add another flow-typing case for E_internal_pletThomas Bauereiss
2019-01-17Work around an issue with type abbreviations in HOLThomas Bauereiss
2019-01-17Output configuration registers for LemThomas Bauereiss
2019-01-17Fix bug in letbind_effects rewriteThomas Bauereiss
2019-01-14Add a function to perform re-writes in parallelAlasdair
2019-01-14Support some more unification casesThomas Bauereiss
2019-01-14Make rewriting of foreach loops for Lem more robustThomas Bauereiss
2019-01-14Merge remote-tracking branch 'origin/sail2' into asl_flow2Alasdair
2019-01-11Updates for sail-arm releaseAlasdair Armstrong
2019-01-10Fixes so 8.5 with vector instructions compiles to CAlasdair Armstrong
2019-01-09Coq: the division used in smt.sail should be EuclideanBrian Campbell
2019-01-09Coq: add parens around negative integer literalsBrian Campbell
2019-01-08Improvements for v85Alasdair Armstrong
2019-01-03Make sure to close file handles when printing error messagesAlasdair Armstrong
2019-01-03Comment out bisect coverage in ocamlbuild filesAlasdair Armstrong
2019-01-02Coq: tweak recently introduced type check to ignore effectsBrian Campbell
2018-12-31Last rewrite reordering needs more typecheckingBrian Campbell
2018-12-31Coq: move function clause merging to keep measure argument intactBrian Campbell
2018-12-30Sort dependencies of termination measures properlyBrian Campbell
2018-12-29Coq: ensure that recursive functions computeBrian Campbell
2018-12-29Add separate termination_measure declarationsBrian Campbell
2018-12-27Coq: avoid putting ambiguous numeric literals in Coq outputBrian Campbell
2018-12-27Coq: fix name clashes and instantiation calculationBrian Campbell
2018-12-26More cleanupAlasdair Armstrong
2018-12-26Some cleanupAlasdair Armstrong
2018-12-26Add makefile target for building with Bisect coverageAlasdair Armstrong
2018-12-26More error messages improvmentsAlasdair Armstrong
2018-12-23Remove a comment that breaks Isabelle buildThomas Bauereiss
2018-12-22Added RISC-V fence.tsoShaked Flur
2018-12-22Improve error messages and debuggingAlasdair Armstrong
2018-12-21Simplify boolean existentialsAlasdair Armstrong
2018-12-21Expand synonyms in generated mapping val-specsAlasdair Armstrong
2018-12-20Make sure sail -v prints useful version infoAlasdair Armstrong
2018-12-20Fix monomorpisation tests with typechecker changesAlasdair Armstrong
2018-12-19Improve sizeof rewriting performanceAlasdair Armstrong
2018-12-19Coq: handle pairs of ranges (and other existential types) properlyBrian Campbell
2018-12-19Coq: handle existentials in hypotheses during solving, add max_nat, better castsBrian Campbell
2018-12-18Ensure type-variables have consistent namesAlasdair
2018-12-18Revert "Experiment with generating type variable names in a repeatable way"Alasdair
2018-12-18Experiment with generating type variable names in a repeatable wayAlasdair Armstrong
2018-12-18Fix rewriter issuesAlasdair Armstrong
2018-12-18Check more carefully for recursive functions when generating LemThomas Bauereiss
2018-12-18Store function instantiation information within annotations, so we don'tAlasdair
2018-12-17Changes for ASL parserAlasdair Armstrong
2018-12-17Adapt Coq and termination measure support to typechecker changesBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 19:11:21 +0000