summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2018-07-08Add -static flag that controls whether generated C functions are staticAlasdair
2018-07-07Coq: precise generic vectorsBrian Campbell
2018-07-07Coq: supply index constraint in for loopsBrian Campbell
2018-07-06Coq: support assertions inside and outside of blocksBrian Campbell
2018-07-06Coq: avoid nexp simplification when deciding whether a cast is neededBrian Campbell
2018-07-06Coq: Avoid clashes with the monad name, MBrian Campbell
2018-07-06Coq: feed assertions into the contextBrian Campbell
2018-07-06Coq: reduce use of sumbool_of_bool to relevant constraintsBrian Campbell
2018-07-06Coq: missing existential building for rangesBrian Campbell
2018-07-06Coq: turn off partial support for dropping true constraints, fix stringsBrian Campbell
2018-07-05Fix equality comparisons for variants in CAlasdair
2018-07-05Fix equality comparisons for structsAlasdair
2018-07-05Passes all tests and now builds mips and cheri againAlasdair
2018-07-05Fix CHERI test that was failing when compiled to CAlasdair Armstrong
2018-07-05make many generated c functions static -- this gives the compiler a chance to...Robert Norton
2018-07-05restore missing RISC-V fence types in sail2; ignore io bits in fences more cl...Jon French
2018-07-03Fix a bug in foreach loopsAlasdair Armstrong
2018-07-03Fix letbind_effects on LEXP_deref with an effectful subexpressionBrian Campbell
2018-07-02Fix get_recursive_functions to not only pick up non-mutually recursive functionsAlasdair Armstrong
2018-07-02Coq: tidy up a bit of printingBrian Campbell
2018-07-02Coq: multiple record field updatesBrian Campbell
2018-07-02Work around Coq issue with pattern bindersBrian Campbell
2018-06-29Constant folding improvementsAlasdair
2018-06-29Try to fix some tricky C compilation bugs, break everything insteadAlasdair Armstrong
2018-06-28Add tagged memory to C rts to cheri can be compiled to CAlasdair Armstrong
2018-06-28Add option to build ocaml with bisect_ppx coverage support. Add cheri targets...Robert Norton
2018-06-28Deduplicate arguments for different constructors in undefined fnsBrian Campbell
2018-06-27Fix reading reals from strings in C libAlasdair Armstrong
2018-06-27RTS: Add support for __ListConfigAlastair Reid
2018-06-27RTS: Delete __SetConfig stub functionAlastair Reid
2018-06-27Make sure __SetConfig gets included in generated codeAlasdair Armstrong
2018-06-26Add configuration registers so __SetConfig ASL can be translatedAlasdair Armstrong
2018-06-26In guarded pattern rewriting, irrefutable patterns subsume wildcardsBrian Campbell
2018-06-26In elf_loader don't attempt to convert paddr to int64 because on MIPS it is q...Robert Norton
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-20 09:56:32 +0000