RefinedC merge requestshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests2021-07-16T07:21:13Zhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/95Remove generated files and associated CI checks.2021-07-16T07:21:13ZRodolphe LepigreRemove generated files and associated CI checks.This requires adding an option [--soft] to [refinedc clean] in order
to prevent the [_CoqProject] file to be edited locally when building
or cleaning the examples.
No sure we want to merge that, what do you think @msammler?This requires adding an option [--soft] to [refinedc clean] in order
to prevent the [_CoqProject] file to be edited locally when building
or cleaning the examples.
No sure we want to merge that, what do you think @msammler?https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/94Bitblast: tactics for solving integer equality with bits2021-07-16T11:45:44ZFengmin ZhuBitblast: tactics for solving integer equality with bitshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/93try removing pinning of conf-mpfr2021-07-14T05:05:23ZMichael Sammlertry removing pinning of conf-mpfrhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/92Add CheckOwnInContext2021-07-12T15:08:27ZMichael SammlerAdd CheckOwnInContexthttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/91add forall simpl instances2021-07-12T13:11:47ZMichael Sammleradd forall simpl instanceshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/90change ty_layout to ty_has_layout2021-07-14T06:23:19ZMichael Sammlerchange ty_layout to ty_has_layouthttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/89normalize bool_decide2021-07-09T12:18:22ZMichael Sammlernormalize bool_decidehttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/88WIP: VIP2021-07-15T13:54:51ZMichael SammlerWIP: VIPhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/87make calls extensible2021-07-14T14:06:07ZMichael Sammlermake calls extensiblehttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/86remove array ptr learn2021-07-06T09:02:11ZMichael Sammlerremove array ptr learnhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/85find buddy2021-07-06T17:16:34ZMichael Sammlerfind buddyhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/84Updated early alloc example2021-07-05T10:19:16ZMichael SammlerUpdated early alloc examplehttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/83Time/mem cast2021-07-15T16:57:52ZMichael SammlerTime/mem casthttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/82Provenance in bytes2021-06-25T16:02:29ZMichael SammlerProvenance in byteshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/81check range on int to ptr cast2021-06-24T14:25:03ZMichael Sammlercheck range on int to ptr casthttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/80add type_alive2021-06-22T10:39:22ZMichael Sammleradd type_alivehttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/79add at_value type2021-06-22T09:36:53ZMichael Sammleradd at_value typehttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/78Notation [&tagged] for owned tagged pointers.2021-06-22T08:39:21ZRodolphe LepigreNotation [&tagged] for owned tagged pointers.This is done by generalising the type parser, to allow type names
starting with '&'.This is done by generalising the type parser, to allow type names
starting with '&'.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/77Make integer to pointer casting rule more realistic2021-06-21T12:08:09ZMichael SammlerMake integer to pointer casting rule more realistichttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/76Change rc_copy_alloc_id to do the cast.2021-06-21T09:14:47ZMichael SammlerChange rc_copy_alloc_id to do the cast.