RefinedC merge requestshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests2021-04-09T08:16:07Zhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/55Refactoring around the val_[to|of]_* functions2021-04-09T08:16:07ZRodolphe LepigreRefactoring around the val_[to|of]_* functionsThis MR introduces the following changes:
- Simplification of `val_[to|of]_loc` using an `EqDecision` instance for `mbyte`.
- Renaming of the `val_[to|of]_int` functions into `val_[to|of]_Z`.
@paulzhu you may need to adapt your code wit...This MR introduces the following changes:
- Simplification of `val_[to|of]_loc` using an `EqDecision` instance for `mbyte`.
- Renaming of the `val_[to|of]_int` functions into `val_[to|of]_Z`.
@paulzhu you may need to adapt your code with the latter (this can be easily done with `sed`, see the commit message).https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/54Generalisation of pointer fragments.2021-04-08T13:52:39ZRodolphe LepigreGeneralisation of pointer fragments.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/53Generalisation of pointer fragments.2021-04-08T09:46:45ZRodolphe LepigreGeneralisation of pointer fragments.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/52make lang.base depend on lithium.base2021-04-08T09:19:32ZMichael Sammlermake lang.base depend on lithium.basehttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/51WIP allocation stack2021-11-02T15:05:08ZRodolphe LepigreWIP allocation stackhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/50Add a [heap_state] invariant.2021-03-09T14:07:03ZRodolphe LepigreAdd a [heap_state] invariant.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/49Error improvements2021-03-02T15:05:01ZMichael SammlerError improvementshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/48semantics and typing rule for NotIntOp2021-03-04T11:14:25ZFengmin Zhusemantics and typing rule for NotIntOphttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/47Cleaning up around [lang.v]2021-03-02T12:30:18ZRodolphe LepigreCleaning up around [lang.v]https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/46Tactic based on lia and autorewrite to solve location equality2021-02-24T10:46:20ZRodolphe LepigreTactic based on lia and autorewrite to solve location equalityhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/45Find hypothesis by semantic equality2021-02-23T07:51:55ZMichael SammlerFind hypothesis by semantic equalityhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/44move normalize_and_simpl_goal to the beginning of unprepared_solve_goal2021-02-22T10:37:33ZMichael Sammlermove normalize_and_simpl_goal to the beginning of unprepared_solve_goalhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/43Finished [early_alloc.c].2021-02-22T11:34:43ZRodolphe LepigreFinished [early_alloc.c].https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/42Draft: Case study: page table2021-08-19T11:50:13ZFengmin ZhuDraft: Case study: page tableCase study: page tableCase study: page tablehttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/41New [bitwise] abstraction used for [uninit] and [zeroed].2021-02-19T15:05:34ZRodolphe LepigreNew [bitwise] abstraction used for [uninit] and [zeroed].https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/40Autogenerate definition of latch2021-02-19T06:13:13ZMichael SammlerAutogenerate definition of latchhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/39make structs proof irrelevant2021-02-18T11:33:50ZMichael Sammlermake structs proof irrelevanthttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/38Some more simplification instances2021-02-17T06:07:21ZMichael SammlerSome more simplification instanceshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/37make subsumption on uninit more complete2021-02-16T12:34:37ZMichael Sammlermake subsumption on uninit more completehttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/36Ci/bits2021-02-19T11:05:16ZFengmin ZhuCi/bitsBitwise operators semantics and bound checking.Bitwise operators semantics and bound checking.