summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2018-06-15Fixes for C RTS for aarch64 no it's split into multiple filesAlasdair Armstrong
2018-06-14rename all lem support files to sail2_foo to avoid conflict with sail1 in rmemJon French
2018-06-14provide impl of int_of_string_opt in Sail_lib to support older Ocaml versionsJon French
2018-06-14Refactor C backend, and split RTS into multiple filesAlasdair
2018-06-13Tracing instrumentation for C backendAlasdair Armstrong
2018-06-13Coq: library updates, informative type errors, fix type aliasesBrian Campbell
2018-06-12Coq: Handle simple top-level type variable definitionsBrian Campbell
2018-06-12Coq: upgrade some errors to report locationsBrian Campbell
2018-06-12Coq: support for range type, along with related existential improvementsBrian Campbell
2018-06-11add 'pat as id' mapping-patternsJon French
2018-06-11More efficient bitfield implementationAlasdair Armstrong
2018-06-11Merge branch 'sail2' into mappingsJon French
2018-06-11change double-caret for string-append-pattern to single caret, since that wou...Jon French
2018-06-11better type inference of union-constructors and mappingsJon French
2018-06-09Fix issue in C_backend, and run C tests with undefined behavior sanitizerAlasdair
2018-06-09Fix issue with catch block return values not being compiled correctlyAlasdair
2018-06-08Fix use of non-tail-recursive calls in elf_loader.Prashanth Mundkur
2018-06-08type checking mappings: allow inferring based on the other side's id inferencesJon French
2018-06-08Coq: some handling of existential types as function return typesBrian Campbell
2018-06-08Coq: add destructuring of atom existentials in patternsBrian Campbell
2018-06-08Coq: track add_typquant changeBrian Campbell
2018-06-08Correct dependencies of bytecode sailBrian Campbell
2018-06-08Coq: existential and constraint solving workBrian Campbell
2018-06-08Coq: some very basic existential supportBrian Campbell
2018-06-08Coq: fix axiom generationBrian Campbell
2018-06-08Coq: update foreach handling, correct field accessesBrian Campbell
2018-06-08Coq: correct failure on unsupported undefined valuesBrian Campbell
2018-06-08Coq: use record update syntax (only single fields work for now)Brian Campbell
2018-06-08Coq: correct implicitness of type arguments in unionsBrian Campbell
2018-06-07Fix bug in add_bits optimizationAlasdair Armstrong
2018-06-07Fix a small bug in monomorphisationThomas Bauereiss
2018-06-06Fix a typo.Yao Li
2018-06-07Add a constant folding optimization passAlasdair
2018-06-06Factor utility functions for IR into separate file and struct update optimiza...Alasdair Armstrong
2018-06-06Some additional fixes to C backend. Re-enable primitive optimizations.Alasdair Armstrong
2018-06-06Some work on improving error messagesAlasdair Armstrong
2018-06-04Fix an issue with riscv_platform involving flow typingAlasdair Armstrong
2018-06-04Fix bug with function return types in C backendAlasdair Armstrong
2018-06-04switch to using a Map data structure for cheri tags in ocaml backend. This so...Robert Norton
2018-06-04Use Util.split_on_char in sail_lib.mlAlasdair Armstrong
2018-05-31Fix for Jenkins buildAlasdair Armstrong
2018-05-31Fixes to get ARM u-boot working in Sail.Alasdair Armstrong
2018-05-31Some tweaks to ocaml compilation and sail_lib for ARM with system registersAlasdair Armstrong
2018-05-28Coq: merge some implicit variables from axioms with argumentsBrian Campbell
2018-05-28Coq: prefer simple binders over patternsBrian Campbell
2018-05-28Coq: add option to produce axioms for unimplemented functionsBrian Campbell
2018-05-28Coq: proper printing of nexpsBrian Campbell
2018-05-25Use paged memory storage for ocaml backend memory. This is slightly slower (<...Robert Norton
2018-05-24Revert "Allow instantiation of type or order type variables without kind decl...Brian Campbell
2018-05-24Check kinds of type variables while checking well-formedness of typesBrian Campbell