summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2018-07-12Handle failures during interpreting betterAlasdair Armstrong
2018-07-12update arm and mips models for new type of write_ram builtin. Also fix c and ...Robert Norton
2018-07-12Fix bug for large integers in OCaml compilationAlasdair Armstrong
2018-07-12Minor fix to support OCaml 4.02.3Shaked Flur
2018-07-12Fixes for ARM Sail tests, and get_time_ns for interpreterAlasdair
2018-07-11RISC-V model fixes for RMEMJon French
2018-07-11Partially revert change to add_vec_int et alThomas Bauereiss
2018-07-11Fix some signedness bugsThomas Bauereiss
2018-07-10fix constructor typoJon French
2018-07-10Only put static qualifier on valspecs when -static flag is usedAlasdair Armstrong
2018-07-10disable printing when compiling to Lem to keep rmem happyJon French
2018-07-10Aarch64 mono script updateBrian Campbell
2018-07-09Initialize fresh memory to 0 in the OCaml backend.Prashanth Mundkur
2018-07-09Lem: prefer type variables to constants when looking for equivalent nexpsBrian Campbell
2018-07-09Changes for anonymisation. Ensure headers are in correct format. Remove some ...Robert Norton
2018-07-09Coq: remove some unnecessary castsBrian Campbell
2018-07-09Fix bug in rewriting of try-catch-blocks with variable updatesThomas Bauereiss
2018-07-09Tweak rewriting of literal patterns for LemThomas Bauereiss
2018-07-09Add explanatory comment to guard rewritingThomas Bauereiss
2018-07-09Add some syntactic sugar for IsabelleThomas Bauereiss
2018-07-09Simplify treating of undefined_bool in Lem libraryThomas Bauereiss
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-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-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