summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-04-18Use the generated num_of_E function for enum E instead of defining one by hand.Prashanth Mundkur
2018-04-18Add generated PDF of documentation draft --- comments welcomeThomas Bauereiss
Placed in lib/isabelle/manual/document.pdf Also fixed a few typos.
2018-04-18Update mono test scriptBrian Campbell
2018-04-18Add first draft of Isabelle library documentationThomas Bauereiss
2018-04-18Add a simple Hoare logic for sequential reasoning to the libraryThomas Bauereiss
2018-04-18Fix bug in pretty-printing loops to LemThomas Bauereiss
2018-04-18Add some lemmas about bitvectorsThomas Bauereiss
Also clean up some library functions a bit, and add some missing failure handling variants of division operations on bitvectors.
2018-04-18Move a few printing functions to sail_values.lemThomas Bauereiss
They are used in various specs and test cases.
2018-04-18Fix another reference to BK_natAlastair Reid
2018-04-18Add a test case for using enum to number function as a castAlasdair Armstrong
2018-04-18Fix build on linuxAlasdair Armstrong
Turns out that BSD sed is not a subset of GNU sed, GNU sed doesn't allow a space after the -i option.
2018-04-18Port to Mac: BSD sed != GNU sedAlastair Reid
For GNU sed, the extension is optional in sed -i ... But in BSD sed, the extension is mandatory sed -i .bak ...
2018-04-18Move Lem shl_int, shr_int implementations from aarch64_extras to sail libBrian Campbell
(note that they're already declared in lib/arith.sail)
2018-04-18Rename BK_nat to BK_int to be consistent with source syntaxAlasdair Armstrong
2018-04-18Updates to latex mode for documentationAlasdair Armstrong
2018-04-18Merge branch 'sail2' of github.com:rems-project/sail into sail2Robert Norton
2018-04-18fix bug in permissions test of ctestsubset.Robert Norton
2018-04-17Implement sret.Prashanth Mundkur
2018-04-17Hook in the delegated trap handler and remove the old one.Prashanth Mundkur
2018-04-17Add platform initialization for the new bits of machine state.Prashanth Mundkur
2018-04-17Separate out the trap handler, and make it use the delegatee privilege.Prashanth Mundkur
2018-04-17Define exception handler delegation.Prashanth Mundkur
2018-04-17Enable mono builtins test, tweak test outputBrian Campbell
2018-04-17Fix slicing in constant propagationBrian Campbell
2018-04-17Move some Lem library vector operations so that we also have mword versionsBrian Campbell
2018-04-16Implement the s-mode views of mie/mip, and their legalizers.Prashanth Mundkur
2018-04-16Add the satp legalizer.Prashanth Mundkur
2018-04-13Add <=_u to riscv prelude.Prashanth Mundkur
2018-04-13Add some checks of current state, and use for the xepc write legalizer.Prashanth Mundkur
2018-04-13Some initial legalizers for writes to S-mode CSRs.Prashanth Mundkur
2018-04-13Define legalizers for writes to M-mode CSRs, and hook these writes to use them.Prashanth Mundkur
2018-04-13Move riscv memory definitions into a separate file.Prashanth Mundkur
2018-04-13Fix access checks to riscv CSRs.Prashanth Mundkur
2018-04-13Add a few more generated file to gitignoreBrian Campbell
2018-04-13Update aarch64 no vector monomorphisation source for current type checkerBrian Campbell
2018-04-13Check all patterns inside functions with -dsanityBrian Campbell
2018-04-12Fill in some minor missing cases in monomorphisationBrian Campbell
2018-04-12remove cheri128 backwards compatibility hack that extended ↵Robert Norton
access_system_regs perm into bits 14-11 -- it looks like spec is heading that way.
2018-04-12implement new permit_unseal used for CUnseal instead of permit_seal.Robert Norton
2018-04-12add a cheri_trace target for conveniently building a debug build.Robert Norton
2018-04-12Add implementations of CReadHwr and CWriteHwrRobert Norton
2018-04-12Add missing read of UserLocal register using dmtc0 4, sel 2. Write was ↵Robert Norton
present but read was missing except via rdhwr.
2018-04-11Initial bits of supervisor state.Prashanth Mundkur
2018-04-11Add some misc informational m-mode registers that are used in a test.Prashanth Mundkur
2018-04-11More structured riscv trap vector handling.Prashanth Mundkur
2018-04-11Fix test preludeBrian Campbell
2018-04-11Avoid unnecessary rechecking in remove numeral pats rewriteBrian Campbell
(especially as the environment previously used was a bit dodgy)
2018-04-11Use more robust method of finding deps of new tyvars in mono analysisBrian Campbell
2018-04-11Make the atom to singleton type rewriter replace literals with guardsBrian Campbell
(previously the typechecker did this for all literal patterns, but now it's only necessary for the rewritten arguments)
2018-04-11Fix neq_range in flow.sailAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 22:12:34 +0000