summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-07-07Cancel riscv reservation before i/o scheduling, tweak reservation tracing.Prashanth Mundkur
2018-07-07Add the lrsc tests from riscv-tests.Prashanth Mundkur
2018-07-07An initial fix to riscv lr/sc, needs a review.Prashanth Mundkur
2018-07-07Add some tracing to riscv address translation.Prashanth Mundkur
2018-07-07Coq: bbv have reorganised their repositoryBrian Campbell
2018-07-07Coq: precise generic vectorsBrian Campbell
2018-07-07Coq: supply index constraint in for loopsBrian Campbell
2018-07-07Coq: eq_range should take proofsBrian Campbell
2018-07-06Coq: support assertions inside and outside of blocksBrian Campbell
2018-07-06Coq: avoid nexp simplification when deciding whether a cast is neededBrian Campbell
2018-07-06Coq: Avoid clashes with the monad name, MBrian Campbell
2018-07-06Coq: feed assertions into the contextBrian Campbell
2018-07-06Coq: use List.In predicates in constraint solving; make other bits robustBrian Campbell
2018-07-06Coq: reduce use of sumbool_of_bool to relevant constraintsBrian Campbell
2018-07-06Coq: missing existential building for rangesBrian Campbell
2018-07-06Coq: turn off partial support for dropping true constraints, fix stringsBrian 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-06changes to increase MIPS coverage -- remove optional/unused PREF instruction ...Robert Norton
2018-07-05Fix printing of aq/rl flags in risc-v lr/sc.Prashanth Mundkur
2018-07-05Fix equality comparisons for variants in CAlasdair
2018-07-05Coq: get index_list rightBrian Campbell
2018-07-05Fix equality comparisons for structsAlasdair
2018-07-05Passes all tests and now builds mips and cheri againAlasdair
2018-07-05Fix CHERI test that was failing when compiled to CAlasdair Armstrong
2018-07-05mips: ignore unused functions warnings caused by making some functions static.Robert Norton
2018-07-05make many generated c functions static -- this gives the compiler a chance to...Robert Norton
2018-07-05support acquire/release loads/stores in RISCV initial_analysisJon French
2018-07-05print to stdout not stderr to stop upsetting rmem regression testsJon French
2018-07-05restore missing RISC-V fence types in sail2; ignore io bits in fences more cl...Jon French
2018-07-04mips: move rmem integration instructions into separate file (disabled for now...Robert Norton
2018-07-04AArch64 Prelude: Move cycle count primop to preludeAlastair Reid
2018-07-03Add htif tohost to the riscv tracecmp tool.Prashanth Mundkur
2018-07-03Allow the riscv htif_tohost mmio port to be readable, and ack writes to that ...Prashanth Mundkur
2018-07-03Fix a bug in foreach loopsAlasdair Armstrong
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-03Fix letbind_effects on LEXP_deref with an effectful subexpressionBrian Campbell
2018-07-03Fill in a few Coq functions for CHERI from the MIPS preludeBrian Campbell
2018-07-03Main: fix SEE handlingAlastair Reid
2018-07-03cheri: update to register file semantics. Most instructions now treat c0 as n...Robert Norton
2018-07-02Fix get_recursive_functions to not only pick up non-mutually recursive functionsAlasdair Armstrong
2018-07-02Coq: add some string functionsBrian Campbell
2018-07-02Coq: tidy up a bit of printingBrian Campbell
2018-07-02Coq modulus operation that fits the typeBrian Campbell
2018-07-02Coq: replace simpl in a tactic with a more precise "change"Brian Campbell
2018-07-02Coq: multiple record field updatesBrian Campbell
2018-07-02Work around Coq issue with pattern bindersBrian Campbell
2018-07-02Coq building rule in MIPS makefileBrian Campbell
2018-07-02cheri: the default cap for 256-bits no longer has reserved bits set.Robert Norton
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 00:53:47 +0000