summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-08-02Start working on a solution for correctly monomorphising polymorphic variant ...Alasdair Armstrong
2018-08-01Remove old test directory in src/testAlasdair Armstrong
2018-08-01Coq: implicit range conversions for function arguments, debug tracingBrian Campbell
2018-07-31Add Coq names for more Aarch64 builtinsBrian Campbell
2018-07-28Update INSTALL.mdhirataqdees
2018-07-27Add some missing rv64i instructions, discovered when annotating the riscv isa...Prashanth Mundkur
2018-07-27Add a riscv latex target.Prashanth Mundkur
2018-07-27Remove unused U_effect constructorAlasdair Armstrong
2018-07-27Merge branch 'sail2' of github.com:rems-project/sail into sail2Peter Sewell
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-27Make type annotations abstract in type_check.mliAlasdair Armstrong
2018-07-27wibPeter Sewell
2018-07-27Coq: remove out-of-date todo listBrian Campbell
2018-07-27Coq: patterns on bit literalsBrian Campbell
2018-07-27Check in snapshot of cheri latexAlasdair Armstrong
2018-07-26Some tweaks to not and or patternsAlasdair Armstrong
2018-07-26Patterns: add or and not patternsAlastair Reid
2018-07-26Warnings: deal with all the deprecation warningsAlastair Reid
2018-07-25Remove unused internal AST nodesAlasdair Armstrong
2018-07-24Merge pull request #16 from geo2a/sail2Alasdair Armstrong
2018-07-24Merge branch 'c_fixes' into sail2Alasdair Armstrong
2018-07-24Merge remote-tracking branch 'origin/sail2' into c_fixesAlasdair Armstrong
2018-07-24Move monomorphisation after mapping rewritesBrian Campbell
2018-07-24Fix a tiny typo in INSTALL.mdGeorgy Lukyanov
2018-07-24Now builds mips spec again.Alasdair
2018-07-23RTS: make g_cycle_count publicAlastair Reid
2018-07-23AArch64 patches: EL2 secure not implementedAlastair Reid
2018-07-23Coq: faster MIPS extras without confusing messageBrian Campbell
2018-07-23Coq test for a few non-trivial atom typesBrian Campbell
2018-07-23Coq: make all pattern matches in the output exhaustiveBrian Campbell
2018-07-20Add assorted comments, consistency fixes and cleanup.Prashanth Mundkur
2018-07-18Coq: constraint solving improvementsBrian Campbell
2018-07-17Coq: support effectful function signatures in axiom generationBrian Campbell
2018-07-17Coq: support returning rich integer types from effectful functionsBrian Campbell
2018-07-17Coq: integer shiftsBrian Campbell
2018-07-17Coq: add printing stubsBrian Campbell
2018-07-17Coq: handle E_constraint properlyBrian Campbell
2018-07-16Coq: fix false existential problemBrian Campbell
2018-07-16Coq: we also unfold lengthBrian Campbell
2018-07-16Coq: handle simple type variable matches properly and nat typeBrian Campbell
2018-07-16Coq: add support for more complex atom typesBrian Campbell
2018-07-13prepare for new opam releaseRobert Norton
2018-07-13Merge branch 'sail2' of github.com:rems-project/sail into sail2Brian Campbell
2018-07-13Coq: avoid a couple of common identifiersBrian Campbell
2018-07-12Add missing builtins needed for cheri128 C. Still doesn't build possibly due ...Robert Norton
2018-07-12make unziping freebsd kernel more robust if run again.Robert Norton
2018-07-12Handle failures during interpreting betterAlasdair Armstrong
2018-07-12update arm and mips models for new type of write_ram builtin. Also fix c and ...Robert Norton
2018-07-12Coq: get rid of syntax error on exception handlingBrian Campbell