summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2018-08-01Remove old test directory in src/testAlasdair Armstrong
2018-08-01Coq: implicit range conversions for function arguments, debug tracingBrian Campbell
2018-07-27Remove unused U_effect constructorAlasdair Armstrong
2018-07-27Make type annotations abstract in type_check.mliAlasdair Armstrong
2018-07-27Coq: remove out-of-date todo listBrian Campbell
2018-07-27Coq: patterns on bit literalsBrian Campbell
2018-07-26Some tweaks to not and or patternsAlasdair Armstrong
2018-07-26Patterns: add or and not patternsAlastair Reid
2018-07-26Warnings: deal with all the deprecation warningsAlastair Reid
2018-07-25Remove unused internal AST nodesAlasdair Armstrong
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-20 04:40:46 +0000