gauravpartha
gauravpartha
Currently, the following code verifies: ``` method testLabel(x: Ref) requires acc(x.f) { label dummy invariant acc(x.f, 1/2) assert acc(x.f) assert false } ``` The semantics of labels with invariants that...
This pull request adds explicit havocs to scoped variables. Previously, havocs were omitted, which is sound because Carbon introduces a unique Boogie variable for each scoped variable and thus the...
The following example verifies in Carbon but not in Silicon (there is an analogous example for fold): ``` field f: Int predicate P(x: Ref, y: Ref) { acc(x.f, 2/1) &&...
There are various cases where Carbon does well-definedness checks in an unexpected order. Some of these issues have been fixed in https://github.com/viperproject/carbon/pull/429, but there are still some issues left. This...
Carbon omits well-definedness checks for inhale and exhale of assertions in cases where Carbon has already checked that those assertions are self-framing. For example, Carbon emits a single self-framing check...
The pull request https://github.com/viperproject/carbon/pull/457 changed the exhale implementation to perform well-definedness checks during the exhale instead of doing them before the exhale, which was required for a proper handling of...
The following PR implements a new function axiomatization approach (developed with @marcoeilers), where function axioms are guarded by an uninterpreted function instead of the concrete function precondition. The goal of...
Carbon verifies the following program currently: ``` method unexpected(x: Ref) { inhale acc(x.f,1/2) && x.f == 2 inhale x.f == 3 || (x.f < 0 ==> unfolding P(x) in true)...
Quasihavoc statements are soon to be merged as a feature into Silver. Silicon will have full support for these statements from the start. Carbon will initially have support only for...
Consider ``` var b: Bool := true while (b) // adding this invariant makes it verify in Carbon // invariant b { goto end b := false } assert false...