summaryrefslogtreecommitdiff
path: root/cheri
AgeCommit message (Expand)Author
2018-09-21Remove cheri and mips specs -- they now have their own repository.Robert Norton
2018-08-28Basic Makefile support for Coq generation from CHERIBrian Campbell
2018-08-28Adapt theory imports for Isabelle 2018Thomas Bauereiss
2018-07-27clean Makefile target to copy generated LaTeX to cheri-architecturePeter Sewell
2018-07-27Revert "wib" (mistaken delete of sail_latexcc)Peter Sewell
2018-07-27wibPeter Sewell
2018-07-27Check in snapshot of cheri latexAlasdair Armstrong
2018-07-10Make HOL build properly again for all of the modelsBrian Campbell
2018-07-06Change HighestSetBit into a form that can be handled by c backend. There are ...Robert Norton
2018-07-06add gcov option for cheri_c. Add cheri128_c target.Robert Norton
2018-07-03cheri: refine lwl/lwr cap length checks to be exact. They were previously a b...Robert Norton
2018-07-03cheri: update to register file semantics. Most instructions now treat c0 as n...Robert Norton
2018-07-02cheri: the default cap for 256-bits no longer has reserved bits set.Robert Norton
2018-07-02optimise cheri c build.Robert Norton
2018-06-28Add tagged memory to C rts to cheri can be compiled to CAlasdair Armstrong
2018-06-28Add option to build ocaml with bisect_ppx coverage support. Add cheri targets...Robert Norton
2018-06-26turn on warnings when compiling mips c then dial back ones that are triggered...Robert Norton
2018-06-04add missing semi colon in arichardsons patch.Robert Norton
2018-05-31Also dump the cap hwregs in dump_cp2_stateAlexander Richardson
2018-05-21cheri: fix a bug in cfromptr: should give null result when value of rt is zer...Robert Norton
2018-05-18cheri: add support for clc with big immediate (clcbi). This is quite easily d...Robert Norton
2018-05-17Clean out old sequential filesBrian Campbell
2018-05-17Clean up CHERI HOL generation a little tooBrian Campbell
2018-05-17Use an intermediate base_monad type alias in Lem,Brian Campbell
2018-05-11Add Isabelle code generation for sequential CHERI modelThomas Bauereiss
2018-05-11Merge branch 'sail2' into cheri-monoThomas Bauereiss
2018-05-10Document the register_inaccessible function.Robert Norton
2018-05-09Tweaks for sequential CHERI in HOLBrian Campbell
2018-05-09Use latex support for generating cheri documentation and remove sed based hac...Robert Norton
2018-05-09Add targets for counting lines in mips, cheri and riscv. Can use either slocc...Robert Norton
2018-05-09Remove start and end markers that are no longer needed now that sail has late...Robert Norton
2018-05-09Add tests for Isabelle->OCaml generation for CHERI and AArch64Thomas Bauereiss
2018-05-07HOL script generation for library and CHERIBrian Campbell
2018-05-04Add back purely sequential Lem generationThomas Bauereiss
2018-05-04Bit of hackery to MIPS prelude and Makefiles to get monomorphised CHERIBrian Campbell
2018-05-01cheri128: remove unnecessary xor of E with 48. The zeroing of E in memory is ...Robert Norton
2018-05-01cheri256: minor optimisation -- factor out null_cap_bits as top level let.Robert Norton
2018-05-01cheri256: switch to using absolute address (cursor) instead of offset (relati...Robert Norton
2018-05-01remove unneeded commented out code.Robert Norton
2018-05-01Implement new CGetAddr instruction. Note that we should possibly rename funct...Robert Norton
2018-04-27Cheri ISA change in CTestSubset -- ignore sealed bits when testing for subset...Robert Norton
2018-04-23Add a cheri128_trace target.Robert Norton
2018-04-23Fix a discrepancy with spec. about which register number is reported for perm...Robert Norton
2018-04-23Fix a problem with 128-bit setCapBounds function revealed by CBuildCap test -...Robert Norton
2018-04-18fix bug in permissions test of ctestsubset.Robert Norton
2018-04-12remove cheri128 backwards compatibility hack that extended access_system_regs...Robert Norton
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-09cheri: compute virtual address mod 2^64 when doing bounds check to avoid fail...Robert Norton
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:54:48 +0000