summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
2019-03-15Coq: some progress on the test suiteBrian Campbell
2019-03-15Add coq test case for for-loop type variableBrian Campbell
2019-03-14Add various useful methods to interactive modeAlasdair Armstrong
2019-03-13C: Add missing update_lbits builtinAlasdair Armstrong
2019-03-09C: Fix miscompilation of constrained struct field accessAlasdair
2019-03-08Fix: Never consider single variable types to be ambiguousAlasdair
2019-03-06Add option to slice out printing and tracing functions when generating CAlasdair Armstrong
2019-03-05Add forgotten recursive function testBrian Campbell
2019-03-05Additional optimizations for C compilationAlasdair
2019-03-04Fix aarch64_small test XML for jenkinsAlasdair Armstrong
2019-03-04Add test for building handwritten ARM to lem for JenkinsAlasdair Armstrong
2019-03-04Fix execute splitting to work when constructors have constraints.Alasdair Armstrong
2019-03-04Do not store type synonyms as functions in the environmentAlasdair Armstrong
2019-03-01Add some tricky test cases for quantified Sail AST typesAlasdair Armstrong
2019-03-01Add a test case for previous commitAlasdair Armstrong
2019-03-01Make Sail more flexible with existentials in union typesAlasdair Armstrong
2019-02-25Update some test case error messagesAlasdair Armstrong
2019-02-21Allow monomorphisation with C generationAlasdair
2019-02-20Fix bug with missing satisfiablity check in subtypingAlasdair
2019-02-20Remove dead branches when compiling to CAlasdair Armstrong
2019-02-19Add regression test for #34Alasdair Armstrong
2019-02-18Add option to linearize constraints containing exponentialsAlasdair Armstrong
2019-02-15Fix bug in Int-synonym expansionAlasdair Armstrong
2019-02-15Use multiple solversAlasdair
2019-02-11Add an additional test caseAlasdair
2019-02-11Add tests for implicit argumentsAlasdair Armstrong
2019-02-08Add parameterization support for bitfields.Prashanth Mundkur
2019-02-08Updates for asl_parserAlasdair Armstrong
2019-02-07Add a symbol for new implicit arguments for backwards compatabilityAlasdair Armstrong
2019-02-07Fix implicits in v8.2 public ARM specAlasdair Armstrong
2019-02-06Add typechecking test from MarkAlasdair Armstrong
2019-02-06Fix some testsAlasdair Armstrong
2019-02-04Test lem output by running end-to-end tests using ocaml via lemAlasdair Armstrong
2019-02-04Fix behavior for fallthrough cases in catch blocksAlasdair Armstrong
2019-02-02Monomorphisation tests all pass so add them to standard regression testsAlasdair
2019-02-02Merge remote-tracking branch 'origin/sail2' into asl_flow2Alasdair
2019-02-01Add test cases for integer synonymsAlasdair
2019-01-31Monomorphisation: improve cast insertion and nexp rewriting on variantsBrian Campbell
2019-01-31Support case splitting on variables as well as sizeof in cast introductionBrian Campbell
2019-01-29Merge branch 'sail2' into asl_flow2Thomas Bauereiss
2019-01-25Coq: add enough to generate some output for arm-v8.5-aBrian Campbell
2019-01-22Add some more test casesAlasdair Armstrong
2019-01-21Pass Lem library path to IsabelleThomas Bauereiss
2019-01-21Don't require manual set up of Isabelle session directoriesThomas Bauereiss
2019-01-14Merge remote-tracking branch 'origin/sail2' into asl_flow2Alasdair
2019-01-08Improvements for v85Alasdair Armstrong
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 error messages improvmentsAlasdair Armstrong
2018-12-22Improve error messages and debuggingAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 13:35:38 +0000