use highlight
This commit is contained in:
parent
02d04204da
commit
1447f0030d
|
@ -18,8 +18,7 @@ href="http://en.wikipedia.org/wiki/Assert.h">assert.h</a>, which offers a
|
|||
macro <code>assert(cond)</code>. When executing a statement such
|
||||
as</p>
|
||||
|
||||
<pre><code>
|
||||
assert(p!=NULL);
|
||||
<pre><code> assert(p!=NULL);
|
||||
</code></pre>
|
||||
|
||||
<p class="justified">the execution is aborted with an error message if the
|
||||
|
@ -33,8 +32,7 @@ using the <code>--no-assertions</code> command line option.</p>
|
|||
<p class="justified">In addition, there is a CPROVER-specific way
|
||||
to specify assertions, using the built-in function __CPROVER_assert:</p>
|
||||
|
||||
<pre><code>
|
||||
__CPROVER_assert(p!=NULL, "p is not NULL");
|
||||
<pre><code> __CPROVER_assert(p!=NULL, "p is not NULL");
|
||||
</code></pre>
|
||||
|
||||
<p class="justified">The (mandatory) string that is passed as the
|
||||
|
@ -91,20 +89,19 @@ a nondeterministic choice that returns a number from 1 to 100. There
|
|||
is no integer type with this range. We therefore use __CPROVER_assume
|
||||
to restrict the range of a nondeterministically chosen integer:</p>
|
||||
|
||||
<code>
|
||||
unsigned int nondet_uint();<br>
|
||||
<br>
|
||||
unsigned int one_to_hundred()<br>
|
||||
{<br>
|
||||
unsigned int result=nondet_uint();<br>
|
||||
__CPROVER_assume(result>=1 && result<=100);<br>
|
||||
return result;<br>
|
||||
}</code>
|
||||
<pre><code>unsigned int nondet_uint();
|
||||
|
||||
unsigned int one_to_hundred()
|
||||
{
|
||||
unsigned int result=nondet_uint();
|
||||
__CPROVER_assume(result>=1 && result<=100);
|
||||
return result;
|
||||
}</code></pre>
|
||||
|
||||
<p class="justified">The function above returns the desired integer from 1
|
||||
to 100. <font color="#ef2020">You must ensure that the condition given as an assumption is
|
||||
actually satisfiable by some nondeterministic choice, or otherwise
|
||||
the model checking step will pass vacuously.</font></p>
|
||||
to 100. <font color="#ef2020">You must ensure that the condition given as
|
||||
an assumption is actually satisfiable by some nondeterministic choice, or
|
||||
otherwise the model checking step will pass vacuously.</font></p>
|
||||
|
||||
<p class="justified">Also note that assumptions are never retroactive: They
|
||||
only affect assertions (or other properties) that follow them in program
|
||||
|
@ -113,45 +110,43 @@ the assumption has no effect on the assertion, which means that
|
|||
the assertion will fail:
|
||||
</p>
|
||||
|
||||
<code>
|
||||
x=nondet_uint();<br>
|
||||
assert(x==100);<br>
|
||||
__CPROVER_assume(x==100);<br>
|
||||
</code>
|
||||
<pre><code>x=nondet_uint();
|
||||
assert(x==100);
|
||||
__CPROVER_assume(x==100);
|
||||
</code></pre>
|
||||
|
||||
<p class="justified">
|
||||
Assumptions do restrict the search space, but only for assertions that follow.
|
||||
As an example, the following program will pass:</p>
|
||||
|
||||
<code>
|
||||
int main() {<br>
|
||||
int x;<br>
|
||||
<br>
|
||||
__CPROVER_assume(x>=1 && x<=100000);<br>
|
||||
<br>
|
||||
x*=-1;<br>
|
||||
<br>
|
||||
__CPROVER_assert(x<0, "x is negative");<br>
|
||||
<pre><code>int main() {
|
||||
int x;
|
||||
|
||||
__CPROVER_assume(x>=1 && x<=100000);
|
||||
|
||||
x*=-1;
|
||||
|
||||
__CPROVER_assert(x<0, "x is negative");
|
||||
}
|
||||
</code>
|
||||
</code></pre>
|
||||
|
||||
<p class="justified">Beware that nondeterminism cannot be used to obtain
|
||||
the effect of universal quantification in assumptions. As an example,
|
||||
</p>
|
||||
|
||||
<code>
|
||||
int main() {<br>
|
||||
int a[10], x, y;<br>
|
||||
<br>
|
||||
x=nondet_int();<br>
|
||||
y=nondet_int();<br>
|
||||
__CPROVER_assume(x>=0 && x<10 && y>=0 && y<10);<br>
|
||||
<br>
|
||||
__CPROVER_assume(a[x]>=0);<br>
|
||||
<br>
|
||||
assert(a[y]>=0);<br>
|
||||
<pre><code>
|
||||
int main() {
|
||||
int a[10], x, y;
|
||||
|
||||
x=nondet_int();
|
||||
y=nondet_int();
|
||||
__CPROVER_assume(x>=0 && x<10 && y>=0 && y<10);
|
||||
|
||||
__CPROVER_assume(a[x]>=0);
|
||||
|
||||
assert(a[y]>=0);
|
||||
}
|
||||
</code>
|
||||
</code></pre>
|
||||
|
||||
<p class="justified">fails, as there is a choice of x and y which
|
||||
results in a counterexample (any choice in which x and y are different).
|
||||
|
|
Loading…
Reference in New Issue