summaryrefslogtreecommitdiff
path: root/mips/prelude.sail
AgeCommit message (Expand)Author
2018-09-21Remove cheri and mips specs -- they now have their own repository.Robert Norton
2018-07-24Merge remote-tracking branch 'origin/sail2' into c_fixesAlasdair Armstrong
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-09Tweak bit casting definitions in MIPS to avoid non-exhaustive patternsBrian Campbell
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-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-25Coq: add typeclass based comparison, and instantiate for enumsBrian Campbell
2018-06-25mips: add optional tracing of register writes (commented out).Robert Norton
2018-06-22Fix Lem build of MIPS/CHERIThomas Bauereiss
2018-06-22Add bitvector size constraints in MIPSBrian Campbell
2018-06-22Add coq builtins for MIPSBrian Campbell
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-07Use the vector_dec standard library for mips. This means we get all the c fun...Robert Norton
2018-06-04cheri: print debug trace info to stderr to keep it separate from uart output.Robert Norton
2018-05-17build fixes: add back tag effect skips required for mips. Move UART check in ...Robert Norton
2018-05-17changes to for testing FreeBSD boot on MIPS: allowing loading raw file in oca...Robert Norton
2018-05-17Clean up MIPS for HOL4 a littleBrian Campbell
2018-05-11Merge branch 'sail2' into cheri-monoThomas Bauereiss
2018-05-11Remove buggy bit list comparison functions from Lem libraryThomas Bauereiss
2018-05-09Use latex support for generating cheri documentation and remove sed based hac...Robert Norton
2018-05-04Bit of hackery to MIPS prelude and Makefiles to get monomorphised CHERIBrian Campbell
2018-04-10Porting some minisail changes to sail2 branchAlasdair Armstrong
2018-04-09remove unused functions from cher/mips prelude (step towards using standard p...Robert Norton
2018-04-04Fix another infinite loop in cast bit_to_bool. Following introduction of eq_b...Robert Norton
2018-03-27Fix infinite loop in cheri/mips cast_unit_vec caused by lack of eq_bit in = o...Robert Norton
2018-03-27print IPS after running cheri model.Robert Norton
2018-03-22Fix C compilation for CHERI and MIPSAlasdair Armstrong
2018-03-21Fix Lem generation for MIPSThomas Bauereiss
2018-03-14rename EXTS and EXTZ to sign_extend and zero_extend because it is more obvios...Robert Norton
2018-03-14Fix Lem generation for CHERI-MIPS and Aarch64Thomas Bauereiss
2018-03-08rename mips_new_tc to mipsRobert Norton