Changes between Version 16 and Version 17 of VerificationWithContracts

Timestamp:

01/31/16 23:29:26 (10 years ago)

Author:

ziqing

Comment:

--

VerificationWithContracts

@@ -40 +40 @@
 For example:
 {{{
+/*@ requires (\valid(p) || !\valid(p) ) && \valid(q);
+*/
+foo(int * p, int * q);
+}}}
+The construction of an initial state seems to be irrelevant to if the pointer p is valid or not, but when CIVL recursively analyzes the requirement
+predicate, it's hard to know if it's relevant or not. Thus my rough solution is :
+  1. Making `\valid` expressions uninterpreted functions;
+  2. Pointer "p" should be valid initially only if {{{ requirement => valid_of_p }}};
+  3. Vice versa, pointer "p" should be undefined initially only if {{{ requirement => !valid_of_p }}};
+  4. Otherwise, it's a non-deterministic choice.
 
+Considering pointer alias, I'm planning such an approach:
+  First, there is an outer scope outside of the source function which is going to be verified. It can be used to represent a set of all visible 
+  scopes from the source function. Thus, for each pointer argument, creating a unique unconstraint array element in the outer scope. 
+{{{
+$input int X[2];  // one for each pointer
 
+/*@ requires \valid(p) && \valid(q);
+*/
+foo(int *p, int *q);
 }}}
+For this example, considering aliasing, the context can be 
+{{{
+( ( \valid(p) && \valid(q) ) => \valid(p) ) => (exists i, 0 <= i < 2 such that *p == X[i] );
+}}}
+