From 1447f0030d9f577dc0ab8463ead88c8fadba04ac Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 13 Jun 2016 12:08:03 +0100 Subject: [PATCH] use highlight --- doc/html-manual/modeling-assertions.shtml | 81 +++++++++++------------ 1 file changed, 38 insertions(+), 43 deletions(-) diff --git a/doc/html-manual/modeling-assertions.shtml b/doc/html-manual/modeling-assertions.shtml index c346f616f2..be6b88796e 100644 --- a/doc/html-manual/modeling-assertions.shtml +++ b/doc/html-manual/modeling-assertions.shtml @@ -18,8 +18,7 @@ href="http://en.wikipedia.org/wiki/Assert.h">assert.h, which offers a macro assert(cond). When executing a statement such as

-

-  assert(p!=NULL);
+
  assert(p!=NULL);
 

 
 
the execution is aborted with an error message if the
@@ -33,8 +32,7 @@ using the --no-assertions command line option.

 
In addition, there is a CPROVER-specific way
 to specify assertions, using the built-in function __CPROVER_assert:

 
-

-  __CPROVER_assert(p!=NULL, "p is not NULL");
+
  __CPROVER_assert(p!=NULL, "p is not NULL");
 

 
 
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:

 
-
-unsigned int nondet_uint();

-

-unsigned int one_to_hundred()

-{

-  unsigned int result=nondet_uint();

-  __CPROVER_assume(result>=1 && result<=100);

-  return result;

-}
+
unsigned int nondet_uint();
+
+unsigned int one_to_hundred()
+{
+  unsigned int result=nondet_uint();
+  __CPROVER_assume(result>=1 && result<=100);
+  return result;
+}

 
 
The function above returns the desired integer from 1
-to 100.  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.

+to 100.  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.

 
 
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:
 

 
-
-  x=nondet_uint();

-  assert(x==100);

-  __CPROVER_assume(x==100);

-
+
x=nondet_uint();
+  assert(x==100);
+  __CPROVER_assume(x==100);
+

 
 

 Assumptions do restrict the search space, but only for assertions that follow.
 As an example, the following program will pass:

 
-
-int main() {

-  int x;

-

-  __CPROVER_assume(x>=1 && x<=100000);

-

-  x*=-1;

-

-  __CPROVER_assert(x<0, "x is negative");

+
int main() {
+  int x;
+
+  __CPROVER_assume(x>=1 && x<=100000);
+
+  x*=-1;
+
+  __CPROVER_assert(x<0, "x is negative");
 }
-
+

 
 
Beware that nondeterminism cannot be used to obtain
 the effect of universal quantification in assumptions. As an example,
 

 
-
-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);

+

+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);
 }
-
+

 
 
fails, as there is a choice of x and y which
 results in a counterexample (any choice in which x and y are different).