| import org.checkerframework.checker.nullness.qual.*; |
| import org.checkerframework.dataflow.qual.*; |
| |
| public class AssertIfClient { |
| |
| @RequiresNonNull("#1.rpcResponse()") |
| void rpcResponseNonNull(Proxy proxy) { |
| @NonNull Object response = proxy.rpcResponse(); |
| } |
| |
| void rpcResponseNullable(Proxy proxy) { |
| @Nullable Object response = proxy.rpcResponse(); |
| } |
| |
| void rpcResponseTypestate() { |
| Proxy proxy = new Proxy(); |
| // :: error: (assignment) |
| @NonNull Object response1 = proxy.rpcResponse(); |
| // :: error: (contracts.precondition) |
| rpcResponseNonNull(proxy); |
| rpcResponseNullable(proxy); |
| |
| proxy.issueRpc(); |
| @NonNull Object response2 = proxy.rpcResponse(); |
| @NonNull Object response3 = proxy.rpcResponse(); |
| rpcResponseNonNull(proxy); |
| rpcResponseNullable(proxy); |
| } |
| } |
| |
| class Proxy { |
| |
| // the RPC response, or null if not yet received |
| @MonotonicNonNull Object response = null; |
| |
| @SuppressWarnings("contracts.postcondition") |
| @EnsuresNonNull({"response", "rpcResponse()"}) |
| void issueRpc() { |
| response = new Object(); |
| } |
| |
| // If this method returns true, |
| // then response is non-null and rpcResponse() returns non-null |
| @SuppressWarnings("contracts.conditional.postcondition") |
| @EnsuresNonNullIf( |
| expression = {"response", "rpcResponse()"}, |
| result = true) |
| boolean rpcResponseReceived() { |
| return response != null; |
| } |
| |
| // Returns non-null if the response has been received, null otherwise; but an |
| // @AssertNonNullIfNonNull annotation would states the converse, that if the result is non-null |
| // then the response hs been received. See rpcResponseReceived. |
| @Pure |
| @Nullable Object rpcResponse() { |
| return response; |
| } |
| } |