summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2018-09-04Add a rewrite to minimise the number of functions marked as recursiveBrian Campbell
2018-09-04Coq: fix early returns with rich typesBrian Campbell
2018-09-03Coq: solver should split earlierBrian Campbell
2018-09-03Coq: get top-level value definitions to work nicely againBrian Campbell
2018-09-03Coq: update RISC-V patch againBrian Campbell
2018-09-03Coq: rework generation of dependent pairs so that they are onlyBrian Campbell
2018-08-31Some C stubs for platform bits for RISC-V.Prashanth Mundkur
2018-08-31rewrite_defs_pat_string_append: only guard the innermost recursive pattern, a...Jon French
2018-08-31mappings: Support for unidirectional mapping clausesJon French
2018-08-31riscv prelude: yet more manual monomorphisations for hex_bitsJon French
2018-08-31fix some compiler warningsJon French
2018-08-31sync and centralise the two .merlin filesJon French
2018-08-30Annotate the RISC-V prelude for C builtins.Prashanth Mundkur
2018-08-30C: Fix a bug where function argument type becomes more specific due to flow t...Alasdair Armstrong
2018-08-30Add a C header containing declarations needed by RISC-V.Prashanth Mundkur
2018-08-30Allow additional includes to be specified for C backend.Prashanth Mundkur
2018-08-30Coq: correct endianness reversal bugBrian Campbell
2018-08-30C: Fix an issue with struct field being generalised inside polymorphic constr...Alasdair Armstrong
2018-08-29C: Fix some issues with tuples as arguments to polymorphic constructorsAlasdair Armstrong
2018-08-29Updated snapshots for Isabelle 2018Thomas Bauereiss
2018-08-28Coq: make some library definitions computeBrian Campbell
2018-08-28Coq snapshot: make some library definitions computeBrian Campbell
2018-08-28Basic Makefile support for Coq generation from CHERIBrian Campbell
2018-08-28fix some compiler not-matched warnings about Typ_bidir and Typ_internal_unknownJon French
2018-08-28add __POS__ argument to Err_unreachable for better error reportingJon French
2018-08-28Adapt theory imports for Isabelle 2018Thomas Bauereiss
2018-08-28fix bug in RISCV assembly mapping, incorrect order of FENCE pred/succ bitsJon French
2018-08-24Fix rewriter issuesAlasdair Armstrong
2018-08-24parser: emit actual unit for an ident() pattern, not wildcard which causes un...Jon French
2018-08-24fix a couple of pretty print inaccuraciesJon French
2018-08-24support for P_or and P_not patterns in rewrite_defs_mapping_patternsJon French
2018-08-24rewrite_defs_mapping_patterns: support for referring to mapping arguments in ...Jon French
2018-08-24pat_to_exp support for vector and string concat patterns; fix typing in exp_o...Jon French
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 15:42:23 +0000