RefinedC merge requestshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests2021-08-03T09:25:56Zhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/104Generate [return 0] for main + small refactoring.2021-08-03T09:25:56ZRodolphe LepigreGenerate [return 0] for main + small refactoring.@lgaeher this fixes the problem you mentioned [here](https://gitlab.mpi-sws.org/iris/refinedc/-/issues/30#note_64174).@lgaeher this fixes the problem you mentioned [here](https://gitlab.mpi-sws.org/iris/refinedc/-/issues/30#note_64174).https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/103allow opening invariants around typed_read_end and typed_write_end2021-07-30T08:28:54ZMichael Sammlerallow opening invariants around typed_read_end and typed_write_endhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/101update to coq 8.13.22021-07-27T09:56:04ZMichael Sammlerupdate to coq 8.13.2https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/100More support comparing pointers with 0 in the front end + rules for if and as...2021-08-03T07:31:46ZRodolphe LepigreMore support comparing pointers with 0 in the front end + rules for if and assert on pointers.This also includes support for better error positions.This also includes support for better error positions.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/99parameterise operators with boolean result by the result integer type2021-07-27T07:25:51ZLennard Gähergaeher@mpi-sws.orgparameterise operators with boolean result by the result integer typeThis is a follow-up to https://gitlab.mpi-sws.org/iris/refinedc/-/merge_requests/98.
This PR parameterises Caesium's operators with a "boolean" result (i.e. the comparison operators as well as the derived && and || operators) by a resul...This is a follow-up to https://gitlab.mpi-sws.org/iris/refinedc/-/merge_requests/98.
This PR parameterises Caesium's operators with a "boolean" result (i.e. the comparison operators as well as the derived && and || operators) by a result integer type (which was hard-coded before to i32) as a step to use Caesium for modelling other C-like languages with different modelling of boolean results (e.g. Rust, which uses single-byte booleans).
Concretely, the changes can be summarised as:
* add a parameter `rit` to the affected operators and use that for the operational semantics of these operators, replacing the `i32` used before.
* adapt the existing notations for these operators to reflect this.
* change the Coq codegen to emit the additional parameter as `i32`,
* adapt the typing proofs to work for the changed operators instantiated to `i32`. Possibly, it might be desirable to support other result types even for C and to generalize the proofs accordingly, but I'm not sure.
The existing examples in the repo compile with these changes, but I haven't tested more exhaustively yet.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/97Implement && and || using IfE.2021-07-16T21:31:28ZRodolphe LepigreImplement && and || using IfE.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/96cleanup base.v2021-07-16T10:47:24ZMichael Sammlercleanup base.vhttps://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/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 bytes