RefinedC merge requestshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests2021-02-01T08:57:32Zhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/21Infrastructure for [SimpleSubsumeVal].2021-02-01T08:57:32ZRodolphe LepigreInfrastructure for [SimpleSubsumeVal].https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/22Strengthen the [LocInBounds] infrastructure.2021-02-02T08:58:49ZRodolphe LepigreStrengthen the [LocInBounds] infrastructure.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/23Unfold more definitions in the side condition solver.2021-02-03T08:00:40ZRodolphe LepigreUnfold more definitions in the side condition solver.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/24small steps towards improving subsume_list2021-02-04T16:45:33ZMichael Sammlersmall steps towards improving subsume_listhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/25Make more functions simpl never2021-02-08T14:13:47ZMichael SammlerMake more functions simpl neverhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/26More [loc_in_bounds] infrastructure.2021-02-10T15:48:00ZRodolphe LepigreMore [loc_in_bounds] infrastructure.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/27Refactor rule for arithmetic operators.2021-02-12T09:06:18ZRodolphe LepigreRefactor rule for arithmetic operators.This PR does a bit of refactoring of the rules for binary (arithmetic) operators on integers.
This will probably be useful to @paulzhu, and I needed this first step for the handling of right shifts.
The changes are the following:
- Defin...This PR does a bit of refactoring of the rules for binary (arithmetic) operators on integers.
This will probably be useful to @paulzhu, and I needed this first step for the handling of right shifts.
The changes are the following:
- Define a function `arith_op_result` that, given the two operands and the op computes the result.
- Define a predicate `arith_op_sidecond` that gives the side conditions for a given op.
- Use the above functions in the rule `type_arith_op_int_int`, and factor in the rules for `/` and `%`.
- Give more precise side conditions for the right and left shift operators (this is the goal of this PR). Note that the standard leaves it as implementation-define what is the result of right-shifting a negative number. I thing we should consider that UB.
Some further factoring of code is possible with the operational semantics, but we can do that as a second step.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/28Refactor mpool2021-02-11T08:38:28ZMichael SammlerRefactor mpoolhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/29Add a size to the [ptr] type.2021-02-12T06:16:14ZRodolphe LepigreAdd a size to the [ptr] type.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/30try new version of unification2021-02-12T07:22:02ZMichael Sammlertry new version of unificationhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/31page_alloc2021-02-12T09:26:08ZMichael Sammlerpage_allochttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/32Progress on the verification of [early_alloc.c].2021-02-12T10:59:15ZRodolphe LepigreProgress on the verification of [early_alloc.c].https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/33Case study: quick sort2021-02-26T05:06:45ZFengmin ZhuCase study: quick sortA new example for RefinedC: quick sort implemented using C arrays.A new example for RefinedC: quick sort implemented using C arrays.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/34Check generated files on CI2021-02-12T15:10:40ZMichael SammlerCheck generated files on CIhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/35Progress on the verification of [early_alloc.c].2021-02-12T17:57:07ZRodolphe LepigreProgress on the verification of [early_alloc.c].https://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.https://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/38Some more simplification instances2021-02-17T06:07:21ZMichael SammlerSome more simplification instanceshttps://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/40Autogenerate definition of latch2021-02-19T06:13:13ZMichael SammlerAutogenerate definition of latch