summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-01-25Omit redundant let-bindings when rewriting (bit-)vector patternsThomas Bauereiss
2018-01-25Rewrite bitvector patterns for OCaml and C backendsThomas Bauereiss
2018-01-25Merge branch 'sail2' of https://bitbucket.org/Peter_Sewell/sail into sail2Alasdair Armstrong
2018-01-25Fix -ocaml_trace optionAlasdair Armstrong
2018-01-25riscv: remove case for non-existent constructor in match that was being treat...Robert Norton
2018-01-25work in progress riscv CSR implementation.Robert Norton
2018-01-25Fix more type annotations in rewriterThomas Bauereiss
2018-01-25Add simple conditional processing and file includeAlasdair Armstrong
2018-01-24Have some simple sail programs compiling to CAlasdair Armstrong
2018-01-24Fixed riscv ocaml compilationAlasdair Armstrong
2018-01-24More work on C compilationAlasdair Armstrong
2018-01-24More work on experimental C backendAlasdair Armstrong
2018-01-23Merge branch 'sail2' of https://bitbucket.org/Peter_Sewell/sail into sail2Alasdair Armstrong
2018-01-23Started working on C backend for sailAlasdair Armstrong
2018-01-23Run tests for Lem shallow embeddingThomas Bauereiss
2018-01-23Added additional tests, and fixed ocaml build of ARM testsAlasdair Armstrong
2018-01-22Update Lem shallow embedding to Sail2Thomas Bauereiss
2018-01-22Added rewriter that specializes all function calls in a specification.Alasdair Armstrong
2018-01-22Add regression test for type synonym with constraints inside existential type...Alasdair Armstrong
2018-01-22Update and fix test suiteAlasdair Armstrong
2018-01-19Added RISCV test case to test suiteAlasdair Armstrong
2018-01-19Added C-style single line commentsAlasdair Armstrong
2018-01-19Got riscv spec to typecheck with sail2Alasdair Armstrong
2018-01-19riscv sail2 wip.Robert Norton
2018-01-19Merge branch 'sail2' of https://bitbucket.org/Peter_Sewell/sail into sail2Alasdair Armstrong
2018-01-19Start translating riscv to sail2Alasdair Armstrong
2018-01-19Make merlin aware of findlib packagesBrian Campbell
2018-01-19Update monomorphisation for sail2Brian Campbell
2018-01-18Clean up command line options slightlyAlasdair Armstrong
2018-01-18Merge remote-tracking branch 'origin/experiments' into sail2Alasdair Armstrong
2018-01-18Modified ocaml backend to use ocamlfind for linksem and lemAlasdair Armstrong
2018-01-18Add elf_loader fileAlasdair Armstrong
2018-01-18Modified unification so Type_check.instantiation_of works after sizeof rewritingAlasdair Armstrong
2018-01-18immediate for CIncOffsetImmediate must be treated as signed (fixes test_cp2_r...Robert Norton
2018-01-17Use right effect annotations in early return rewritingThomas Bauereiss
2018-01-17Try to remove early returns more aggressivelyThomas Bauereiss
2018-01-17Rewrite topological sortingThomas Bauereiss
2018-01-17Add generated ARM spec and test cases for itAlasdair Armstrong
2018-01-17Fix use of nexps in type annotations when not using machine wordsThomas Bauereiss
2018-01-16Test the ocaml interpreter with the same tests as the ocaml compilationAlasdair Armstrong
2018-01-16Improve formatting of output when running all test suites.Alasdair Armstrong
2018-01-16Created version of typecheck test suite for sail2 branchAlasdair Armstrong
2018-01-16Fix problem with let-bindings in pattern guardsThomas Bauereiss
2018-01-16Output more type annotations in Lem backendThomas Bauereiss
2018-01-16Handle for loops correctly when rewriting size parametersBrian Campbell
2018-01-16Another useful monomorphisation rewriteBrian Campbell
2018-01-15Add help to interactive mode, and load files incrementallyAlasdair Armstrong
2018-01-15Check monomorphisation case split size once for each patternBrian Campbell
2018-01-15Refactored and improved ocaml interpreterAlasdair Armstrong
2018-01-15Support non-trivial literal patternsBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 21:11:49 +0000