summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
2020-11-01Fix interpreter pattern matching bugAlasdair
2020-09-28LaTeX: Underscore-escape values in the \ifstrequal codeAlex Richardson
2020-09-28LaTeX tests: check that the generated code buildsAlex Richardson
2020-09-28LaTeX: provide default implementations of the other saildoc commandsAlex Richardson
2020-09-28Re-generate latex testsAlex Richardson
2020-09-28LaTeX: Add newline after itemize and enumerate environmentsAlex Richardson
2020-09-28Handle sectioning commands in saildoc LaTeX outputAlex Richardson
2020-09-25Saildoc: do not mangle links targets enclosed in <>Alex Richardson
2020-09-25Add an initial LaTeX testAlex Richardson
2020-09-25tests: Move copy-pasted code into a shared helper .shAlex Richardson
2020-09-12Merge some of the gitignore filesColumbus240
2020-09-07Fix typo a mono_rewrites definitionBrian Campbell
2020-08-10Fix a C backend bug with letbindings in guards shadowing body definitionsAlasdair
2020-08-06Forbid duplicate top-level letbindingsAlasdair
2020-07-15Update duplicate ctor warningAlasdair
2020-07-15Add test files missed from last commitMark Wassell
2020-06-23Fix bug with duplicate enum identifiers in patternsAlasdair
2020-06-17Make `if cond { ... return() };` assert cond in the type environmentBrian Campbell
2020-06-17Add test for if-return patternBrian Campbell
2020-06-14Coq: tidy up scope in libraryBrian Campbell
2020-06-10Prepare Coq library for packagingBrian Campbell
2020-06-05Generate nice error messages for patterns woth duplicate bindingsAlasdair
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