summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2018-07-24Merge branch 'c_fixes' into sail2Alasdair Armstrong
2018-07-24Merge remote-tracking branch 'origin/sail2' into c_fixesAlasdair Armstrong
2018-07-24Move monomorphisation after mapping rewritesBrian Campbell
2018-07-24Now builds mips spec again.Alasdair
2018-07-23Coq: make all pattern matches in the output exhaustiveBrian Campbell
2018-07-17Coq: support effectful function signatures in axiom generationBrian Campbell
2018-07-17Coq: support returning rich integer types from effectful functionsBrian Campbell
2018-07-17Coq: handle E_constraint properlyBrian Campbell
2018-07-16Coq: fix false existential problemBrian Campbell
2018-07-16Coq: we also unfold lengthBrian Campbell
2018-07-16Coq: handle simple type variable matches properly and nat typeBrian Campbell
2018-07-16Coq: add support for more complex atom typesBrian Campbell
2018-07-13Merge branch 'sail2' of github.com:rems-project/sail into sail2Brian Campbell
2018-07-13Coq: avoid a couple of common identifiersBrian Campbell
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-12Coq: get rid of syntax error on exception handlingBrian Campbell
2018-07-12Coq: handle all bool conjunctions/disjunctionsBrian Campbell
2018-07-12Coq: more autocast insertionBrian Campbell
2018-07-12Coq: tuple matching in loopsBrian Campbell
2018-07-12Coq: more accurate autocast insertionBrian Campbell
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 11:30:52 +0000