summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2018-08-24rewrite_defs_pat_lits: rewrite away fewer lits when generating ocaml, for cle...Jon French
2018-08-23Fix interpreter after re-writer changeAlasdair Armstrong
2018-08-23Move vector_string_to_bit_list from its odd place in Rewriter.rewrite_pat to ...Jon French
2018-08-22Fix a bug in nested vector concatenation patternsAlasdair Armstrong
2018-08-22Revert "rewrite_defs_pat_lits: add an explicit type annotation around generat...Jon French
2018-08-22rewrite_defs_pat_lits: add an explicit type annotation around generated id pa...Jon French
2018-08-21C: Correctly handle the kinds of patterns generated by mappingsAlasdair Armstrong
2018-08-20Refactor tuple conversions in Sail to C compilationAlasdair Armstrong
2018-08-20Add some more test cases for C compilationAlasdair Armstrong
2018-08-18Correctly handle specialising polymorphic types in nested unionsAlasdair
2018-08-18Correctly specialise type annotation in polymorphic functionsAlasdair
2018-08-17Improve builtins testsAlasdair Armstrong
2018-08-17Coq: also introduce autocast at type annotationsBrian Campbell
2018-08-17Extend guarded patterns rewriting to exception catchingBrian Campbell
2018-08-16Add the type an expression was checked against to tannots, and use for CoqBrian Campbell
2018-08-16Use Set rather than Hashtbl in graph.mlAlasdair Armstrong
2018-08-16Remove unused ref typeAlasdair Armstrong
2018-08-16Ressurect builtin tests, and add parallel test runner scriptAlasdair Armstrong
2018-08-16Various cleanups to ott grammarAlasdair Armstrong
2018-08-15Temporary fix for RISC-V Lem generationBrian Campbell
2018-08-15Snapshot of Coq from the RISC-V modelBrian Campbell
2018-08-15Get RISC-V on Coq into reasonable state to showBrian Campbell
2018-08-14Coq: attempt a quick proof before an indepth oneBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 01:15:24 +0000