summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
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-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
2018-05-24Coq: need None special case here, tooBrian Campbell
2018-05-24Coq: record conditionals in the context for constraint solvingBrian Campbell
2018-05-23Coq: Implement the most basic merging of type- and term-level parametersBrian Campbell
2018-05-22Fix one part of cast introduction, leave another for laterBrian Campbell
2018-05-22Fix for E_cons not being compiled correctly into OCamlAlasdair Armstrong
2018-05-21Add an -ocaml-nobuild option to avoid building the generated ocaml by default...Prashanth Mundkur
2018-05-18Make named theorem collections of state monad more fine-grainedThomas Bauereiss
2018-05-18Fix bug in rewriting variable updatesThomas Bauereiss
2018-05-18Avoid split_on_char function that was introduced in OCaml 4.04. Use Util vers...Robert Norton
2018-05-17changes to for testing FreeBSD boot on MIPS: allowing loading raw file in oca...Robert Norton
2018-05-17Merge branch 'cheri-mono' into sail2Brian Campbell
2018-05-17Remove sequential code againBrian Campbell
2018-05-17Use an intermediate base_monad type alias in Lem,Brian Campbell
2018-05-16Declare hol automatic termination in sail_valuesRamana Kumar
2018-05-12Fix bug in handling of registers with option typeThomas Bauereiss