| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-09-21 | Remove cheri and mips specs -- they now have their own repository. | Robert Norton | |
| 2018-08-28 | Adapt theory imports for Isabelle 2018 | Thomas Bauereiss | |
| Requires a recent Lem version that supports generating session-qualified imports, e.g. revision rems-project/lem@d92b077f1781765a65082c815ff363ef79499860 | |||
| 2018-07-24 | Merge remote-tracking branch 'origin/sail2' into c_fixes | Alasdair Armstrong | |
| 2018-07-24 | Now builds mips spec again. | Alasdair | |
| Some more testing needed to make sure it runs FreeBSD properly and CHERI before merging | |||
| 2018-07-10 | Make HOL build properly again for all of the models | Brian Campbell | |
| 2018-07-07 | Coq: bbv have reorganised their repository | Brian Campbell | |
| 2018-07-05 | mips: ignore unused functions warnings caused by making some functions static. | Robert Norton | |
| 2018-07-02 | Coq building rule in MIPS makefile | Brian Campbell | |
| 2018-06-29 | Try to fix some tricky C compilation bugs, break everything instead | Alasdair Armstrong | |
| 2018-06-27 | Add a mips_c_gcov target that builds mips_c model with coverage reporting. | Robert Norton | |
| 2018-06-26 | turn on warnings when compiling mips c then dial back ones that are ↵ | Robert Norton | |
| triggered by generated code (probably false positives). Fix some warnings in rts.c | |||
| 2018-06-25 | add device tree file for mips. | Robert Norton | |
| 2018-06-22 | Add coq generation rule for mips | Brian Campbell | |
| 2018-06-21 | Fix MIPS wrt changes to C runtime | Alasdair Armstrong | |
| This plus changes to bitfield internals is enough to run some MIPS tests at 1Mhz. | |||
| 2018-06-08 | add sail as dependency of mips targets. | Robert Norton | |
| 2018-06-07 | add mips_c target. | Robert Norton | |
| 2018-06-04 | Add mips.c target in Makefile. Currently triggers assertion failure in ↵ | Robert Norton | |
| c_backend. still need to merge changes to prelude.sail. | |||
| 2018-05-17 | Clean up MIPS for HOL4 a little | Brian Campbell | |
| Move mono_rewrites into lib | |||
| 2018-05-11 | Merge branch 'sail2' into cheri-mono | Thomas Bauereiss | |
| In order to use up-to-date sequential CHERI model for test suite | |||
| 2018-05-09 | remove redundant cloc targets. | Robert Norton | |
| 2018-05-09 | Add targets for counting lines in mips, cheri and riscv. Can use either ↵ | Robert Norton | |
| sloccount or cloc. sloccount seems to be reliable but lacks a way to tell it that sail files can be treated like ocaml without renaming the files. cloc has a nicer interface is lower quality in other regards like broken ocaml support in versions shipped with Ubuntu (e.g. treats {...} as comment, no nested comments support). For sail2 syntax this is OK because we use the C parser instead which gives the same results as sloccount. | |||
| 2018-05-04 | Bit of hackery to MIPS prelude and Makefiles to get monomorphised CHERI | Brian Campbell | |
| 2018-04-04 | Fix another infinite loop in cast bit_to_bool. Following introduction of ↵ | Robert Norton | |
| eq_bool this was preferred over eq_bit when compiling the match on bit in bit_to_bool... Fix is to overload == before including flow.sail but feels a bit inelegant. | |||
| 2018-03-21 | Patch AST datatypes in generated Isabelle theories | Thomas Bauereiss | |
| Deactivate plugins of the datatype package except for the size plugin in order to keep processing time reasonable. This is currently only needed for the big AST datatypes, so we just patch this using a sed command. | |||
| 2018-03-14 | Fix Lem generation for CHERI-MIPS and Aarch64 | Thomas Bauereiss | |
| - Update Lem bindings and extras files - Rewrite Nexp_var's if they are bound to a constant, similar to Nexp_id's (used for cap_size in the CHERI spec) - Add Lem and Isabelle Makefile targets for CHERI | |||
| 2018-03-08 | rename mips_new_tc to mips | Robert Norton | |
| 2018-03-08 | Remove files in mips directory prior to copying in files from mips_new_tc. ↵ | Robert Norton | |
| Hopefully thiis will help git to spot the rename and hence preserve history. | |||
| 2017-11-30 | match what rmem (ppcmem2) expects from ISA Makefiles | Shaked Flur | |
| 2016-05-31 | delete obsolete Makefile (src/Makefile currently hanldes mips build). | Robert Norton | |
| 2015-12-22 | More make file goo, and fixing a typo in run_with_elf | Kathy Gray | |
| 2015-12-22 | More gluing mips to interpreter | Kathy Gray | |
| 2015-12-17 | Remove external functions that the library provides, having added them to ↵ | Kathy Gray | |
| the type environment finally. (Also small cleaning of the new makefile) | |||
| 2015-12-17 | First bit of gluing mips onto interpreter and eventually ppcmem infrastructure | Kathy Gray | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |