summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-07-09Log some timing info at the end of riscv execution.Prashanth Mundkur
2018-07-09Lem: prefer type variables to constants when looking for equivalent nexpsBrian Campbell
2018-07-09Add no_devices.sail to be compatible with latest AArch64 prelude andAlasdair Armstrong
2018-07-09anonymise another github link.Robert Norton
2018-07-09anonymise github link in sail manual.Robert Norton
2018-07-09Remove awkward constraints on GetSlice_int for nowBrian Campbell
2018-07-09Changes for anonymisation. Ensure headers are in correct format. Remove some ...Robert Norton
2018-07-09Tweak bit casting definitions in MIPS to avoid non-exhaustive patternsBrian Campbell
2018-07-09Coq: remove some unnecessary castsBrian Campbell
2018-07-09Support building an anonymised version of manual. Fix sail example in manual....Robert Norton
2018-07-09Update gitignoreThomas Bauereiss
2018-07-09Fix bug in rewriting of try-catch-blocks with variable updatesThomas Bauereiss
2018-07-09Tweak rewriting of literal patterns for LemThomas Bauereiss
2018-07-09Add explanatory comment to guard rewritingThomas Bauereiss
2018-07-09Update CHERI code generation from IsabelleThomas Bauereiss
2018-07-09Add some syntactic sugar for IsabelleThomas Bauereiss
2018-07-09Patch some potential uses of uninitialised variables in AArch64Thomas Bauereiss
2018-07-09Simplify treating of undefined_bool in Lem libraryThomas Bauereiss
2018-07-09add riscv_analysis.sail to SAIL_SRCSJon French
2018-07-09add LOADRES, STORECON, AMO to analysisJon French
2018-07-09Bits for bits of aarch64 in coqBrian Campbell
2018-07-09Support writes to misa.C in riscv.Prashanth Mundkur
2018-07-08Make the riscv fetch-execute loop return instead of exiting when done.Prashanth Mundkur
2018-07-08Move the riscv analysis function into its own file for coverage purposes.Prashanth Mundkur
2018-07-08Add a riscv coverage target using bisect-ppx.Prashanth Mundkur
2018-07-08Add -static flag that controls whether generated C functions are staticAlasdair
2018-07-07Add reservation traces to riscv tracecmp tool.Prashanth Mundkur
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