summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2018-06-25Check for variables in disjointness checkThomas Bauereiss
2018-06-25Support bitlist representation in Sail2_stringThomas Bauereiss
2018-06-25Fix a bug in pattern guard rewritingThomas Bauereiss
2018-06-25Coq: add typeclass based comparison, and instantiate for enumsBrian Campbell
2018-06-25Coq: automatic cast introductionBrian Campbell
2018-06-25Use getopt rather than argp for Mac compatibility in C runtimeAlasdair Armstrong
2018-06-23Split Sail->ANF translation into its own fileAlasdair
2018-06-22Fix bug in elf_loader: zero memory when segment memsz exceeds size.Prashanth Mundkur
2018-06-22Coq: use simple forms for simple pattern matches in E_internal_letBrian Campbell
2018-06-22add support for new cycle_limit feature in mips.Robert Norton
2018-06-21Add command line option support for Sail->C compiled modelsAlasdair Armstrong
2018-06-21Follow Sail2 renaming in Isabelle libraryThomas Bauereiss
2018-06-21Merge branch 'tracing' into sail2Alasdair Armstrong
2018-06-21Fix MIPS wrt changes to C runtimeAlasdair Armstrong
2018-06-21Simplify the ANF->IR translationAlasdair Armstrong
2018-06-21changes to riscv model to support rmemJon French
2018-06-20Coq: Generate MR when appropriate; syntax fixesBrian Campbell
2018-06-20Coq: add missing existential projection on simple let expressionsBrian Campbell
2018-06-20Coq: Tidy up libraries, export StringBrian Campbell
2018-06-20Coq: print div/mod/abs in nexps; avoid mod as an identifierBrian Campbell
2018-06-20Coq: port handling of effectful and/or from Lem backendBrian Campbell
2018-06-19Minor optimization in ocaml_backend to use ints instead of strings for Big_in...Prashanth Mundkur
2018-06-19Coq: use undefined_bitvectorBrian Campbell
2018-06-19Add elf parsing from AlastairAlasdair Armstrong
2018-06-19Improvements to Sail C for booting LinuxAlasdair Armstrong
2018-06-18Coq: better handling of identifiers, esp infix onesBrian Campbell
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