| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-12-28 | use ocamlfind to locate lem and zarith | Shaked Flur | |
| 2017-12-16 | compatibility with OCaml 4.06.0; | Shaked Flur | |
| imported new version of PPrint (20171003) | |||
| 2017-12-13 | find zarith using ocamlfind instead of using the one in ocaml-lib which is ↵ | Shaked Flur | |
| no longer there | |||
| 2017-12-05 | add Ed | Peter Sewell | |
| 2017-12-05 | Update header files on master | Alasdair Armstrong | |
| 2017-11-02 | remove a lot of dead code form run_with_elf_cheri* | Robert Norton | |
| 2017-11-02 | reset inCCallDelay in code that is not dead. | Robert Norton | |
| 2017-11-01 | added RISC-V "fence r,r" | Shaked Flur | |
| 2017-10-31 | cheri: throw an exception if there is an attempt to access C26/IDC in the ↵ | Robert Norton | |
| delay slot of a ccall selector 1 call. | |||
| 2017-10-24 | fix default cap value on cheri128 following previous changes -- E stored in ↵ | Robert Norton | |
| registers is no longer xored with 48 so need to initialise it. Also use E and T values used by CHERI hw and adjust decoding functions appropriately. Fix shift functions for ocaml shallow embedding which failed to handle shifts greater than vector length. | |||
| 2017-10-09 | add translations for missing read/write kinds. | Robert Norton | |
| 2017-10-09 | add translation of IK_mem_rmw interp_inter_imp. TODO: could we get rid of ↵ | Robert Norton | |
| this and use shallow embedding conversion? | |||
| 2017-10-06 | move nias_of_instruction into RMEM so that it can use shallow embedding ast ↵ | Robert Norton | |
| and not obsolete interp_interface one. | |||
| 2017-09-29 | fix those build errors | Christopher Pulte | |
| 2017-09-29 | fix deep_shallow_convert, stop using interp_interface.instruction for most ↵ | Christopher Pulte | |
| things, SF and CP bugfixing | |||
| 2017-09-26 | fixes | Christopher Pulte | |
| 2017-09-21 | wib | Shaked Flur | |
| 2017-09-21 | added a comment to the x86 lock'd read and write | Shaked Flur | |
| 2017-09-20 | add support for x86 lock prefix (also remove unused Read/Write_tag kind in ↵ | Robert Norton | |
| etc/regfp.sail. | |||
| 2017-09-19 | fix | Christopher Pulte | |
| 2017-09-15 | x86: implement regfp analysis function (no control flow yet) | Robert Norton | |
| 2017-09-15 | reinstate deep/shallow conversion | Christopher Pulte | |
| 2017-09-03 | added RISC-V strong-acquire/release | Shaked Flur | |
| 2017-08-31 | add EnumerationType type class: if a type is a member you get Ord membership ↵ | Christopher Pulte | |
| and Set membership for free | |||
| 2017-08-31 | added RISC-V AMOs | Shaked Flur | |
| 2017-08-30 | typeclass instance Ord(opcode) | Christopher Pulte | |
| 2017-08-24 | typo | Shaked Flur | |
| 2017-08-24 | typo | Shaked Flur | |
| 2017-08-24 | added barrier-kind for x86 MFENCE; | Shaked Flur | |
| fixed some compare functions; | |||
| 2017-08-22 | Merge branch 'master' of https://bitbucket.org/Peter_Sewell/sail | Christopher Pulte | |
| 2017-08-22 | and fix that other places | Christopher Pulte | |
| 2017-08-22 | added RISC-V "fence w,w" and "fence.i"; | Shaked Flur | |
| fixed the interpreter nias analysis; | |||
| 2017-08-22 | adapt state.lem to RISCV additions | Christopher Pulte | |
| 2017-08-19 | RISC-V store-release | Shaked Flur | |
| 2017-08-17 | added RISC-V load-acquire | Shaked Flur | |
| 2017-08-17 | fixed the RISC-V fences (3 types: "rw,rw"/"r,rw"/"rw,w") | Shaked Flur | |
| 2017-08-16 | lem_interp: remove broken val_to_string_internal functions, replace with ↵ | Jon French | |
| string_of_value as used everywhere else | |||
| 2017-08-12 | Resolve ambiguity between negation of integers and bools | Thomas Bauereiss | |
| 2017-08-12 | Fix compilation issue for 32-bit systems | Thomas Bauereiss | |
| 2017-08-02 | fix sail library test interpreter glue for API change. Also fix ↵ | Robert Norton | |
| build_context val spec which was out of dated although lem did not complain for some reason... | |||
| 2017-08-02 | fix run_with_elf*.ml with changed lem_interp api | Jon French | |
| 2017-07-24 | interpreter: optionally print debugging traces | Jon French | |
| 2017-07-24 | vector parts of interpreter now evaluate all arguments of expression before ↵ | Jon French | |
| exiting due to one of them being unknown; fixes incorrect exhaustive analysis for footprints | |||
| 2017-07-24 | move value type definitions to ott, and introduce new E_internal_value ast ↵ | Jon French | |
| node for passing around encapsulated evaluated values; change Interp.to_exp to now just wrap values in this node | |||
| 2017-07-19 | split library tests into separate files to avoid risk of sail compiler stack ↵ | Robert Norton | |
| overflow. | |||
| 2017-07-19 | borrow some of aa's bash code to convert library test suite output to junit ↵ | Robert Norton | |
| xml for jenkins. | |||
| 2017-07-06 | Tests for (almost) all sail builtins. Many interesting things discovered. ↵ | Robert Norton | |
| Library in need of rationalisation. | |||
| 2017-07-06 | fix off by one in type of add_vec builtin function. There are many more ↵ | Robert Norton | |
| dubious types but will wait for library rationalisation to fix. | |||
| 2017-07-06 | fix interpreter version of get_min/max_representable which similarly broken ↵ | Robert Norton | |
| to ocaml version. TODO: also fix copies in sail_values.lem and sail_values_word.lem. | |||
| 2017-07-06 | fix interpreter lteq/gteq for range/vec. | Robert Norton | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |