summaryrefslogtreecommitdiff
path: root/mips
AgeCommit message (Expand)Author
2018-09-21Remove cheri and mips specs -- they now have their own repository.Robert Norton
2018-09-03Coq: rework generation of dependent pairs so that they are onlyBrian Campbell
2018-08-28Adapt theory imports for Isabelle 2018Thomas Bauereiss
2018-08-16Add the type an expression was checked against to tannots, and use for CoqBrian Campbell
2018-08-02Coq mips: fix deprecation warningBrian Campbell
2018-08-02Coq: remove type removal holdover from Lem backend, add MIPS lemmaBrian Campbell
2018-07-24Merge remote-tracking branch 'origin/sail2' into c_fixesAlasdair Armstrong
2018-07-24Now builds mips spec again.Alasdair
2018-07-23Coq: faster MIPS extras without confusing messageBrian Campbell
2018-07-12Add missing builtins needed for cheri128 C. Still doesn't build possibly due ...Robert Norton
2018-07-12update arm and mips models for new type of write_ram builtin. Also fix c and ...Robert Norton
2018-07-11Update CHERI code extraction from IsabelleThomas Bauereiss
2018-07-10Make HOL build properly again for all of the modelsBrian Campbell
2018-07-09Tweak bit casting definitions in MIPS to avoid non-exhaustive patternsBrian Campbell
2018-07-09Simplify treating of undefined_bool in Lem libraryThomas Bauereiss
2018-07-07Coq: bbv have reorganised their repositoryBrian Campbell
2018-07-07Coq: precise generic vectorsBrian Campbell
2018-07-06changes to increase MIPS coverage -- remove optional/unused PREF instruction ...Robert Norton
2018-07-05mips: ignore unused functions warnings caused by making some functions static.Robert Norton
2018-07-04mips: move rmem integration instructions into separate file (disabled for now...Robert Norton
2018-07-03cheri: refine lwl/lwr cap length checks to be exact. They were previously a b...Robert Norton
2018-07-03mips: just whitespace.Robert Norton
2018-07-03Fill in a few Coq functions for CHERI from the MIPS preludeBrian Campbell
2018-07-02Coq modulus operation that fits the typeBrian Campbell
2018-07-02Coq building rule in MIPS makefileBrian Campbell
2018-06-29Try to fix some tricky C compilation bugs, break everything insteadAlasdair Armstrong
2018-06-28Add tagged memory to C rts to cheri can be compiled to CAlasdair Armstrong
2018-06-27Add a mips_c_gcov target that builds mips_c model with coverage reporting.Robert Norton
2018-06-27Add a new function cycle_limit_reached that returns bool, allowing for gracef...Robert Norton
2018-06-26mips: fix duplication of cycle_count call that arose due to git merge.Robert Norton
2018-06-26mips: comment out printing of EXCEPTION on every ISA exception.Robert Norton
2018-06-26turn on warnings when compiling mips c then dial back ones that are triggered...Robert Norton
2018-06-25Support bitlist representation in Sail2_stringThomas Bauereiss
2018-06-25Coq: add typeclass based comparison, and instantiate for enumsBrian Campbell
2018-06-25Use getopt rather than argp for Mac compatibility in C runtimeAlasdair Armstrong
2018-06-25add device tree file for mips.Robert Norton
2018-06-25mips: add optional tracing of register writes (commented out).Robert Norton
2018-06-25Fix bugs in mips ldl/ldr that were probably introduced in porting to sail2.Robert Norton
2018-06-22Fix Lem build of MIPS/CHERIThomas Bauereiss
2018-06-22Add current state of mips_extras.vBrian Campbell
2018-06-22Add bitvector size constraints in MIPSBrian Campbell
2018-06-22Add coq builtins for MIPSBrian Campbell
2018-06-22Add coq generation rule for mipsBrian Campbell
2018-06-22add support for new cycle_limit feature in mips.Robert Norton
2018-06-21Remove loading kernel from mips mainAlasdair Armstrong
2018-06-21Merge branch 'tracing' into sail2Alasdair Armstrong
2018-06-21Fix MIPS wrt changes to C runtimeAlasdair Armstrong
2018-06-18Add bitvector length constraints to mips inequalitiesBrian Campbell
2018-06-11More efficient bitfield implementationAlasdair Armstrong
2018-06-08add sail as dependency of mips targets.Robert Norton
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:20:47 +0000