summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-07-24Merge pull request #16 from geo2a/sail2Alasdair Armstrong
Fix a tiny typo in INSTALL.md
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
Fixes monomorphisation on files using mappings. Also extended constant propagation to handle pattern matches on bitvector expressions (because an earlier rewrite replaces the literals). Also moved L_undef rewriting because monomorphisation can handle them but not the replacement functions.
2018-07-24Fix a tiny typo in INSTALL.mdGeorgy Lukyanov
2018-07-24Now builds mips spec again.Alasdair
Some more testing needed to make sure it runs FreeBSD properly and CHERI before merging
2018-07-23RTS: make g_cycle_count publicAlastair Reid
This allows debug messages to include the current cycle count which can be useful for debugging.
2018-07-23AArch64 patches: EL2 secure not implementedAlastair Reid
Several v8.4 tests were failing because they attempted to enter EL2 secure mode (which is supported on v8.4 but not on v8.3). This test detects an attempt to enter EL2 secure and reports an easily diagnosed error message.
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
Uses previous stage to deal with (e.g.) guards. New option -dcoq_warn_nonex tells you where all of the extra default cases were added.
2018-07-20Add assorted comments, consistency fixes and cleanup.Prashanth Mundkur
2018-07-18Coq: constraint solving improvementsBrian Campbell
Use eauto so that user-added hints are more flexible, example with Replicate in aarch64, dropped zbool to prevent slow proof searches (and preprocessing deals with boolean comparisons now). Report failed constraints after preprocessing; Separate preprocessing tactic out.
2018-07-17Coq: support effectful function signatures in axiom generationBrian Campbell
2018-07-17Coq: support returning rich integer types from effectful functionsBrian Campbell
(e.g., coerce_int_nat in aarch64)
2018-07-17Coq: integer shiftsBrian Campbell
2018-07-17Coq: add printing stubsBrian Campbell
2018-07-17Coq: handle E_constraint properlyBrian Campbell
Adds missing constraints for aarch64
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
As a result, add proof to pow2.
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
to code gen issue.
2018-07-12make unziping freebsd kernel more robust if run again.Robert Norton
2018-07-12Handle failures during interpreting betterAlasdair Armstrong
Changes to the interpreter to better support constant folding during compilation mean it can now throw exceptions to the caller, allow the caller to handle the error, rather than simply printing an error. This broke the ARM interpreter test because exit() is handled by throwing an Exit exception in the interpreter.
2018-07-12update arm and mips models for new type of write_ram builtin. Also fix c and ↵Robert Norton
interpreter implementations of same.
2018-07-12Coq: get rid of syntax error on exception handlingBrian Campbell
2018-07-12Coq: handle all bool conjunctions/disjunctionsBrian Campbell
2018-07-12Coq: more autocast insertionBrian Campbell
2018-07-12Coq: tuple matching in loopsBrian Campbell
2018-07-12Coq: remove unnecessary constraint on foreach loopsBrian Campbell
2018-07-12Temporarily remove some paragraphs from the manual for anonymisationAlasdair Armstrong
2018-07-12Coq: more accurate autocast insertionBrian Campbell
2018-07-12Fix bug for large integers in OCaml compilationAlasdair Armstrong
2018-07-12Further anonymise manualAlasdair Armstrong
2018-07-12Minor fix to support OCaml 4.02.3Shaked Flur
2018-07-12Fixed a nested comment issueShaked Flur
2018-07-11Add fixme note about riscv jalr.Prashanth Mundkur
2018-07-11Update the exception code for riscv LR after clarification on isa-dev.Prashanth Mundkur
2018-07-12Fixes for ARM Sail tests, and get_time_ns for interpreterAlasdair
2018-07-11RISC-V model fixes for RMEMJon French
2018-07-11Remove copyright header from generated isabelle for anonymisation. Make sure ↵Robert Norton
to repeat this if re-generating isabelle before submission.
2018-07-11Add FreeBSD boot to mips test suite.Robert Norton
2018-07-11Fixes to Isabelle snapshotThomas Bauereiss
Remove absolute paths, update Aarch64_extras.thy
2018-07-11Note that a suitable HOL version is requiredBrian Campbell
2018-07-11Add ROOTS file to Isabelle snapshotThomas Bauereiss
2018-07-11Update Isabelle and HOL snapshotsThomas Bauereiss
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 12:45:42 +0000