summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-11-30Rename Undefined outcome to ChooseThomas Bauereiss
2018-11-29Add separate outcome/event for tagged memory loadsThomas Bauereiss
2018-11-29Add some helper lemmas to Isabelle libThomas Bauereiss
2018-11-20Use nat instead of (list bitU) for addresses in monad outcomesThomas Bauereiss
2018-10-31Add helper functions in Sail Lem libraryThomas Bauereiss
2018-10-31Fix Isabelle libraryThomas Bauereiss
2018-10-31Monad refactoring in Lem shallow embeddingThomas Bauereiss
2018-10-05interpreter: Remove boxes (no longer used)Jon French
2018-10-05RISC-V: encode/decode and assembly mappings for compressed instructionsJon French
2018-10-05fix bug in infer_mpat losing types of identifiers inferred from other_envJon French
2018-10-04Merge branch 'ocaml-instruction-generation' into sail2Brian Campbell
2018-10-04Bit of commentary, proper TODO errorBrian Campbell
2018-10-04rename stringappend ids for more readable generated codeJon French
2018-10-03Drop unnecessary thunking; more trouble than it's worthBrian Campbell
2018-10-02Tidy up some whitespaceBrian Campbell
2018-10-02Clean up generator pretty printingBrian Campbell
2018-10-02Remove some old debugging messagesBrian Campbell
2018-10-02Trigger random generator generation with a command line optionBrian Campbell
2018-10-02Rough code to generate random instructions for testingBrian Campbell
2018-10-01Update Coq RISC-V patch now that the assembler is in good shapeBrian Campbell
2018-10-01Extend Coq pattern match completeness rewrite to let patternsBrian Campbell
2018-10-01New rewriting pass toplevel_string_appendJon French
2018-09-28Add a regression test for bug in commit 88b25e9Alasdair Armstrong
2018-09-28Fix optimisation bug for certain if statementsAlasdair Armstrong
2018-09-27Add new functions in ast_util.ml for working with locationsAlasdair Armstrong
2018-09-27Add an additional type checking testAlasdair Armstrong
2018-09-24Coq: avoid variables called tt (the unit constant)Brian Campbell
2018-09-24Coq: more constraint solutions for aarch64Brian Campbell
2018-09-24Coq: add autocasts at monad returnsBrian Campbell
2018-09-21Remove cheri and mips specs -- they now have their own repository.Robert Norton
2018-09-20Tidy up help text for a few optionsBrian Campbell
2018-09-19Coq: track changes elsewhereBrian Campbell
2018-09-19Coq: more fixes for AArch64Brian Campbell
2018-09-19rewrite_defs_pat_string_append: fix bug with guarded SomeJon French
2018-09-19separate decimal_string_of_bits from string_of_bitsJon French
2018-09-19src/gen_lib/sail2_string.lem: more Lem monomorphisations for hex_bits_N_match...Jon French
2018-09-18Fix issues with tuple Constructors taking multiple argumentsAlasdair Armstrong
2018-09-18Add string mapping functions to interpreterAlasdair Armstrong
2018-09-17Add diffs to sail files for Aarch64 Coq generationBrian Campbell
2018-09-17Coq: fix types in aarch64_extras undefined_vector and casts for argumentsBrian Campbell
2018-09-17Coq: solve some constraint/type errors with AArch64Brian Campbell
2018-09-17Coq: remove an obsolete specialisationBrian Campbell
2018-09-17Coq: make generic_neq work on realBrian Campbell
2018-09-17Rewrites.rewrite_defs_mapping_patterns: emit an explicit type annotation on t...Jon French
2018-09-14Sail_lib.string_of_bits: print in decimal (properly, with bigints) rather tha...Jon French
2018-09-14(oops, should have been with "more hex_bits_N monomorphs")Jon French
2018-09-14Sail_lib.int_of_string_opt: use Big_int.of_string rather than OCaml int_of_st...Jon French
2018-09-14More monomorphisations for hex_bits_N...Jon French
2018-09-14RISCV prelude: fix typo in ocaml extern for negate_*Jon French
2018-09-14Sail_lib and RISCV prelude: functions for bitwise operations on intsJon French
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 09:29:32 +0000