summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-05-15Really don't remove those filesBrian Campbell
2018-05-15Fix the ebreak instruction to trap, and remove the now obsolete internal ↵Prashanth Mundkur
exception. This should fix the sbreak test.
2018-05-14import new build of riscv tests including some new ones that are expected to ↵Robert Norton
pass.
2018-05-14Ignore built files in HOL4 snapshotBrian Campbell
2018-05-14Add missing HOL4 files (and disable overzealous cleaning)Brian Campbell
2018-05-12Add ROOT filesThomas Bauereiss
2018-05-12Add link to README.mdThomas Bauereiss
2018-05-12Update RISC-V snapshotThomas Bauereiss
2018-05-12Fix bug in handling of registers with option typeThomas Bauereiss
Also add test cases and Isabelle lemmas
2018-05-12add -APeter Sewell
2018-05-11Add links in Isabelle snapshot READMEThomas Bauereiss
2018-05-11Add Isabelle snapshot of AArch64 with Brian's monomorphisationThomas Bauereiss
2018-05-11Fix last few links in README.mdAlasdair Armstrong
2018-05-11Fix some links and be more clear about licensingAlasdair Armstrong
2018-05-11Try to fix relative links in README.mdAlasdair Armstrong
2018-05-11Add updated README fileAlasdair Armstrong
2018-05-11Add snapshot of HOL4 output for CHERI and RISC-VBrian Campbell
2018-05-11Add missing document list example to repositoryAlasdair Armstrong
2018-05-11Update and alphabetise author list in manualAlasdair Armstrong
2018-05-11More builtin names in constant propagationBrian Campbell
2018-05-11Temporary hacks for monomorphisationBrian Campbell
Mostly introducing type variables for regsize in valspecs
2018-05-11Make nexp simplification a little smarterBrian Campbell
(should really make the Lem pretty printer use the solver properly, but this is a useful stopgap)
2018-05-11Actually use the correct type for singleton rewriting this timeBrian Campbell
2018-05-11Be much more careful to introduce the right bitvector casts to the right sizesBrian Campbell
2018-05-11Handle automatic existential unpacking in function application in mono analysisBrian Campbell
2018-05-11Use type from funcl in singleton rewritingBrian Campbell
The pattern types may be subtypes, using those caused it to try rewriting int parameters and failing
2018-05-11Add link to Thomas's Sail/Isabelle documentation in manualAlasdair Armstrong
Replace the old manual with new version in repository root
2018-05-11More work on documentationAlasdair Armstrong
Should have all the main language features covered in at least some detail now.
2018-05-11Work around Lem generation problem in RISC-VThomas Bauereiss
"sum" is an existing constant in Isabelle, and the Lem constant avoiding mechanism does not seem to pick it up when used as the name of a function parameter.
2018-05-11Add snapshot of generated Isabelle theoriesThomas Bauereiss
Currently contains Lem and Sail libraries, and RISC-V and CHERI-MIPS specs.
2018-05-11add .git to dev-repo in opam file to satisfy opam-publish.Robert Norton
2018-05-11prepare sail 0.2 releaseRobert Norton
2018-05-11Add uart stub with registers based on ARM uart specAlasdair Armstrong
2018-05-11Remove buggy bit list comparison functions from Lem libraryThomas Bauereiss
Found bugs by running CHERI test suite on Isabelle-exported model: signed less-than for bit lists was missing negations for the two's complement, and unsigned less-than compared the reverse lists. Since all other backends implement this in Sail, it seems best to just remove this code. Also add support for infix operators to Lem backend, by z-encoding their identifiers like the other backends do.
2018-05-11Remove unneeded _sail suffix from latex files.Robert Norton
2018-05-11Avoid generating latex files that differ only by case because this causes ↵Robert Norton
confusion on case insensitive file systems (e.g. mac).
2018-05-10latex: don't include the prefix in the label. This means we have the option ↵Robert Norton
of omitting valspec in documentation if it is deemed too verbose and still have hyperlinks work. The caveat is that it could result in multiply defined labels.
2018-05-10Document the register_inaccessible function.Robert Norton
2018-05-09Remove unused definitions.Prashanth Mundkur
2018-05-09remove redundant cloc targets.Robert Norton
2018-05-09add loc for arm full.Robert Norton
2018-05-09Add full translated aarch64 spec including vector instructionsAlasdair Armstrong
2018-05-09Use latex support for generating cheri documentation and remove sed based ↵Robert Norton
hack. Also some minor code cleanups and comments.
2018-05-09Add 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-09Remove start and end markers that are no longer needed now that sail has ↵Robert Norton
latex output.
2018-05-09Add language=sail option in listings command for latex output. This helps ↵Robert Norton
with documents containing listings in multiple languages.
2018-05-09Fix an issue with C compilationAlasdair Armstrong
2018-05-09Fix printing of hex strings in LemThomas Bauereiss
2018-05-09Adapt Isabelle code generation to Byte_sequence changesThomas Bauereiss
2018-05-09Add tests for Isabelle->OCaml generation for CHERI and AArch64Thomas Bauereiss
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 15:02:04 +0000