summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2018-09-14Type_check: allow mappings to contain escape effectsJon French
2018-09-13C: Fix an issue with assigning to unitialized variables at end of blocksAlasdair Armstrong
2018-09-13Coq: real built-ins for AArch64Brian Campbell
2018-09-12Jenkins: Fix deprecation warningsAlasdair Armstrong
2018-09-12Coq: update RISC-V patchBrian Campbell
2018-09-12Coq: fix type annotations for early returnBrian Campbell
2018-09-12Coq: make generic_eq work on more typesBrian Campbell
2018-09-12Coq: avoid some use of pattern binders to help Coq's type checkerBrian Campbell
2018-09-12Coq: print more type information for existentially typed vectorsBrian Campbell
2018-09-12Coq: remove extra "True"s from constraintsBrian Campbell
2018-09-11Coq: some basic handling for more existentialsBrian Campbell
2018-09-11Coq: remove a bunch of Lem-ismsBrian Campbell
2018-09-11Update coq-riscv snapshot patch and READMEBrian Campbell
2018-09-10RISC-V: move the PC and minstret updates into the step function, to better lo...Prashanth Mundkur
2018-09-10C: Add documentation for C compilation in manual.texAlasdair Armstrong
2018-09-10Various fixesAlasdair Armstrong
2018-09-07C: Support RISC-V in elf loader.Prashanth Mundkur
2018-09-07C: add a usage message to the rts.Prashanth Mundkur
2018-09-07Jenkins: Fix Jenkins issue with RISC-V test suiteAlasdair Armstrong
2018-09-07RISCV: Run RISC-V tests using version compiled to CAlasdair Armstrong
2018-09-06C: Fix a bug with shadowing in nested let-bindingsAlasdair
2018-09-06Coq: update RISC-V snapshotBrian Campbell
2018-09-06Coq: fill in a few more RISC-V axiomsBrian Campbell
2018-09-06Coq: more string handlingBrian Campbell
2018-09-06Coq: fix up some barrier/memory definitions for RISC-VBrian Campbell
2018-09-06RISCV: Get enough of the RISCV platform into C to run some testsAlasdair Armstrong
2018-09-06Allow options to be set in the interactive modeAlasdair Armstrong
2018-09-05Coq: fill in trivial ranges in constraint solverBrian Campbell
2018-09-04C: add an option to control generation of main().Prashanth Mundkur
2018-09-04C: split out setup/init and teardown functions from main().Prashanth Mundkur
2018-09-04C: Tweaks to RISC-V to get compiling to CAlasdair Armstrong
2018-09-04Improve error messages for include and ifdef statementsAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 12:21:30 +0000