RefinedC merge requestshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests2021-12-01T12:57:58Zhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/114Add boolean op-type + [builtin_boolean] type.2021-12-01T12:57:58ZRodolphe LepigreAdd boolean op-type + [builtin_boolean] type.Fixes #45Fixes #45https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/125Clean up letbinding infrastructure2021-11-24T12:42:59ZMichael SammlerClean up letbinding infrastructurehttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/124improve liWand performance2021-11-23T15:06:35ZMichael Sammlerimprove liWand performancehttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/123bail out early for trivial sideconditions2021-11-17T10:16:51ZMichael Sammlerbail out early for trivial sideconditionshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/122bail out early for trivial hyps2021-11-17T09:43:49ZMichael Sammlerbail out early for trivial hypshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/120enable record update2021-10-21T16:07:17ZFengmin Zhuenable record update1. Add dependency: coq-record-update
2. Use this library to simplify annotations for `pgtable.c`1. Add dependency: coq-record-update
2. Use this library to simplify annotations for `pgtable.c`https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/119upgrade to coq 8.14.02021-10-19T12:39:05ZMichael Sammlerupgrade to coq 8.14.0https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/118More simpl instances for bf_cons2021-10-15T07:15:34ZFengmin ZhuMore simpl instances for bf_cons1. Instances for a singleton `bf_cons` compare with 0
2. Instance for solving equality of two `bf_cons` with the same shape (field indices)
3. Case study `pgtable.c` is updated accordingly, removing usages of the heuristic tactic `simpl_...1. Instances for a singleton `bf_cons` compare with 0
2. Instance for solving equality of two `bf_cons` with the same shape (field indices)
3. Case study `pgtable.c` is updated accordingly, removing usages of the heuristic tactic `simpl_bool_hyp`https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/117add SimplExist and SimplForall2021-10-13T15:07:27ZMichael Sammleradd SimplExist and SimplForallhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/116dynamic alloc/free2021-10-06T08:26:17ZLennard Gähergaeher@mpi-sws.orgdynamic alloc/freeThis MR adds dynamic memory allocation to the core language. We require this for RefinedRust, but RefinedC can just keep on not using it.
This is implemented in terms of a fairly canonical `Alloc` expression and `Free` statement, using t...This MR adds dynamic memory allocation to the core language. We require this for RefinedRust, but RefinedC can just keep on not using it.
This is implemented in terms of a fairly canonical `Alloc` expression and `Free` statement, using the existing `free_block` and `alloc_new_block` definitions.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/115remove constraints on z3 in gitlab-ci.yml2021-09-22T06:10:13ZMichael Sammlerremove constraints on z3 in gitlab-ci.ymlhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/113Better handling of Coq paths in the frontend.2021-09-20T09:27:23ZRodolphe LepigreBetter handling of Coq paths in the frontend.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/112Generalize the [boolean] type.2021-09-16T14:32:03ZRodolphe LepigreGeneralize the [boolean] type.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/111Add [cast_to_bool] and factorise "if" rules.2021-09-13T16:26:27ZRodolphe LepigreAdd [cast_to_bool] and factorise "if" rules.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/109Bit-wise reasoning2021-08-27T10:39:06ZFengmin ZhuBit-wise reasoning1. Introduce new `bitvec` and `bitvec_raw` types, and their typing rules.
2. Rewriting rules for normalizing bit vectors (by customized constructors).
3. Case study: `pgtable.c`1. Introduce new `bitvec` and `bitvec_raw` types, and their typing rules.
2. Rewriting rules for normalizing bit vectors (by customized constructors).
3. Case study: `pgtable.c`https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/110change implementation of via_vm_compute and add negb simpl instances2021-08-25T07:25:47ZMichael Sammlerchange implementation of via_vm_compute and add negb simpl instanceshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/108Control better which sideconditions get shelved2021-08-19T06:36:09ZMichael SammlerControl better which sideconditions get shelvedhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/107Use multisuccess of typeclasses eauto to get rid of n parameter in FindInContext2021-08-05T14:57:38ZMichael SammlerUse multisuccess of typeclasses eauto to get rid of n parameter in FindInContexthttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/106add via_vm_compute2021-08-05T07:07:24ZMichael Sammleradd via_vm_computehttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/105split out heap_loc_eq2021-08-03T11:18:18ZMichael Sammlersplit out heap_loc_eq