summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
2020-05-21Merge branch 'mono-tweaks' of github.com:rems-project/sail into mono-tweaksAlasdair
2020-05-21Merge branch 'sail2' into mono-tweaksAlasdair
2020-05-15Update type error messages for jenkinsAlasdair
2020-05-14Merge remote-tracking branch 'origin' into codegenAlasdair
2020-05-14Re-activate some testsAlasdair
2020-05-11Functorise and refactor C code generatorAlasdair
2020-05-04Mono: Try to fix bug in inter-procedural analysisThomas Bauereiss
2020-05-04Try to fix bug in size parameter rewritingThomas Bauereiss
2020-04-28Update test error messages, hopefully will make Jenkins happy againAlasdair
2020-04-28Add flooring division in preludeAlasdair
2020-04-27Fix try in exception handler jib bugBrian Campbell
2020-04-21Take kid synonyms into account when propagating constantsThomas Bauereiss
2020-04-21Mono: Check for non-constant calls to make_the_valueThomas Bauereiss
2020-04-21Tweak types of loop combinators for prover combinatorsThomas Bauereiss
2020-04-15Add more intuitive defaults to interactive toplevelAlasdair
2020-04-10Add test output to gitignoreThomas Bauereiss
2020-04-10Make bounds check for vector subrange assignments stricterThomas Bauereiss
2020-04-10Update path for newer versions of BBV Coq libraryThomas Bauereiss
2020-04-10Be more careful when flow-typing loopsThomas Bauereiss
2020-03-19Improve a particularly unhelpful type errorAlasdair
2020-03-18Expose details of failed lexp bounds checksThomas Bauereiss
2020-02-24Allow overloading of subrange builtins for non-bitvectorsThomas Bauereiss
2020-02-21Make sure we test that struct literals have a complete set of fields. Fixes #60Alasdair Armstrong
2020-02-20More list C codegen fixes for issue #59Alasdair Armstrong
2020-02-20Fix missing code generation builtins for lists. Fixes #59Alasdair Armstrong
2020-01-31Fix soundness bug found by MarkAlasdair
2020-01-17Merge scattered mapping fixesJames Clarke
2020-01-17Merge branch 'coq-bool-props' into sail2Brian Campbell
2020-01-16Allow effects on mappingsAlasdair Armstrong
2020-01-16Cleanup type-checking rule for LEXP_fieldAlasdair Armstrong
2019-12-10Introduce new bitfield syntax for ASL translationAlasdair Armstrong
2019-12-06Don't introduce uneccesary control flow when compilingAlasdair Armstrong
2019-12-01Coq: remove last use and definition of doc_nc_propBrian Campbell
2019-11-22Add tests for monomorphisation improvement in eb0e17f2Brian Campbell
2019-11-11Make sure undefined_gen inserts enough type annotations for union constructorsAlasdair Armstrong
2019-11-07Make the world a slightly more sane and consistent placeAlasdair Armstrong
2019-11-07Backport fixes to SMT generation from poly_mapping branchAlasdair Armstrong
2019-11-05Forbid types declared after a scattered union being used in clausesAlasdair
2019-11-05Improve type error for recursive types slightlyAlasdair Armstrong
2019-11-05Make sure we correctly forbid recursive datatypes that we don't want to supportAlasdair Armstrong
2019-11-04Some almost-forgotten mono testsBrian Campbell
2019-11-01Add a missing well-formedness checkAlasdair
2019-10-02Coq: limited support for existentially-typed tuplesBrian Campbell
2019-09-02Enable part of a test that's been fixed recently.Brian Campbell
2019-08-30Add a couple of overlooked testsBrian Campbell
2019-08-29Clean up some mono testsBrian Campbell
2019-08-14Update testsThomas Bauereiss
2019-08-02Fix up some edge cases with the bitvector/polyvector splitBrian Campbell
2019-08-01Merge branch 'sail2' into separate_bvAlasdair Armstrong
2019-08-01Merge remote-tracking branch 'origin/rv_duopod_fix' into sail2Alasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 09:39:35 +0000