claim -> property

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3909 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

Author: kroening

doc/html-manual/cbmc.shtml

@@ -45,13 +45,13 @@ Now, run CBMC as follows:
 </p>
 
 <code>
-&nbsp;&nbsp;cbmc file1.c --show-claims --bounds-check --pointer-check
+&nbsp;&nbsp;cbmc file1.c --show-properties --bounds-check --pointer-check
 </code>
 
 <p class="justified">The two options <code>--bounds-check</code> and <code>--pointer-check</code>
 instruct CBMC to look for errors related to pointers and array bounds.
 CBMC will print the list of properties it checks. Note that it prints a
-claim labeled with "array argv upper bound" together with the
+property labeled with "array argv upper bound" together with the
 location of the faulty array access. As you can see, CBMC largely
 determines the property it needs to check itself. This is realized
 by means of a preliminary static analysis, which relies on computing a fixed
@@ -60,10 +60,10 @@ domains</a>. More detail on automatically generated properties
 is provided <a href="properties.shtml">here</a>.</p>
 
 <p class="justified">
-Note that automatically generated claims
-need not necessarily correspond to bugs &ndash; these are just <i>potential</i>
-flaws. Whether one of these claims corresponds to a bug needs to be
-determined by further analysis.
+Note that automatically generated properties need not necessarily correspond
+to bugs &ndash; these are just <i>potential</i> flaws.  Whether one of these
+properties holds or corresponds to a bug needs to be determined by
+further analysis.
 </p>
 
 <p class="justified">

doc/html-manual/modeling-assertions.shtml

@@ -35,7 +35,7 @@ to specify assertions, using the built-in function __CPROVER_assert:</p>
 
 <p class="justified">The (mandatory) string that is passed as the
 second argument provides an informal description of the assertion.
-It is shown in the list of claims together with the condition.</p>
+It is shown in the list of properties together with the condition.</p>
 
 <p class="justified">The assertion language of the CPROVER tools is
 identical to the language used for expressions.  Note that <a

doc/html-manual/properties.shtml

@@ -14,7 +14,7 @@ cover this topic in more detail in this section.</p>
 
 <p class="justified">
 Both CBMC and SATABS use <i><a href="http://en.wikipedia.org/wiki/Assertion_(computing)">
-assertions</a></i> to specify program properties. Assertions are claims about
+assertions</a></i> to specify program properties. Assertions are properties of
 the state of the program when the program reaches a particular program
 location. Assertions are often written by the programmer by means of the
 <code>assert</code> macro.</p>
@@ -167,7 +167,7 @@ as follows:
 
 <p>
 <code>
-&nbsp;&nbsp;goto-instrument out.gb --show-claims
+&nbsp;&nbsp;goto-instrument out.gb --show-properties
 </code>
 </p>
 

doc/html-manual/satabs-aeon.shtml

@@ -50,11 +50,11 @@ Aeon:
 </p>
 
 <p>
-<code>satabs *.c --pointer-check --bounds-check --show-claims</code>
+<code>satabs *.c --pointer-check --bounds-check --show-properties</code>
 </p>
 
 <p class="justified">
-SATABS will show about 300 claims in various functions
+SATABS will show about 300 properties in various functions
 (read <a href="properties.shtml">this</a> for more information
 on the property instrumentation).
 Now consider the first few lines of the <code>main</code> function 
@@ -126,7 +126,7 @@ matches  the  string  at <code>NAME</code>. If a variable name matches,
 SATABS has no information whatsoever about the content of
 <code>environ</code>. Even if SATABS could access the
 en&shy;vi&shy;ron&shy;ment variables on your computer, a successful verification
-of <code>Aeon</code> would then only guarantee that the claims for
+of <code>Aeon</code> would then only guarantee that the properties for
 this program hold on your computer with a specific set of
 en&shy;vi&shy;ron&shy;ment variables. We have to assume that <code>environ</code>
 contains en&shy;vi&shy;ron&shy;ment variables that have an arbitrary content
@@ -137,10 +137,10 @@ can be modified by the user.  The approximation of the behavior of
 content of the string.</p>
 
 <p class="justified">
-Now let us have another look at the claims that SATABS generates for the
+Now let us have another look at the properties that SATABS generates for the
 models of the the string library and for <code>getenv</code>.  Most of these
-claims require that we verify that the upper and lower bounds of buffers or
-arrays are not violated.  Let us look at one of the claims that SATABS
+properties require that we verify that the upper and lower bounds of buffers or
+arrays are not violated.  Let us look at one of the properties that SATABS
 generates for the code in function <code>getConfig</code>:
 </p>
 
@@ -156,12 +156,12 @@ Claim getConfig.3:<br>
 <p class="justified">The model of the function <code>strcpy</code>
 dereferences the pointer returned by <code>getenv</code>, which may
 return a NULL pointer. This possibility is detected by the static
-analysis, and thus a corresponding claim is generated. Let us 
-check this specific claim:
+analysis, and thus a corresponding property is generated. Let us 
+check this specific property:
 </p>
 
 <p>
-<code>satabs *.c --pointer-check --bounds-check --claim getConfig.3</code>
+<code>satabs *.c --pointer-check --bounds-check --property getConfig.3</code>
 </p>
 
 <p class="justified">SATABS immediately returns a counterexample path
@@ -171,7 +171,7 @@ bug in this program: it requires that the environment variable
 HOME is set, and crashes otherwise.
 </p>
 
-<p class="justified">Let us examine one more claim in the
+<p class="justified">Let us examine one more property in the
 same function:</p>
 
 <p><code>
@@ -182,7 +182,7 @@ Claim getConfig.7:<br>
 </code></p>
 
 <p class="justified">
-This claim asserts that the upper bound of the array <code>home</code>
+This property asserts that the upper bound of the array <code>home</code>
 is not violated. The variable <code>home</code>
 looks familiar: We encountered it in the function <code>getConfig</code>
 given above. The function <code>getenv</code> in combination with functions
@@ -192,7 +192,7 @@ to check the upper bound of the array <code>home</code>:
 </p>
 
 <p>
-<code>satabs *.c --pointer-check --bounds-check --claim getConfig.7</code>
+<code>satabs *.c --pointer-check --bounds-check --property getConfig.7</code>
 </p>
 
 <p class="justified">
@@ -212,7 +212,7 @@ such loops and will therefore unroll the loop body as often as necessary.
 The array <code>home</code> has <code>MAX_LEN</code> elements, and 
 <code>MAX_LEN</code> is defined to be 512 in <code>aeon.h</code>. 
 Therefore, SATABS would have to run through at least 512 iterations, only to
-verify (or reject) one of the more than 300 claims! Does this fact
+verify (or reject) one of the more than 300 properties! Does this fact
 defeat the purpose of static verification?
 </p>
 
@@ -242,7 +242,7 @@ use BOPPO instead of the default model checker SMV:
 </p>
 
 <p>
-<code>satabs --claim 5 --modelchecker boppo --loop-detection \</code><br>
+<code>satabs --property 5 --modelchecker boppo --loop-detection \</code><br>
 <code>&nbsp;&nbsp;aeon.c base64.c lib_aeon.c</code>
 </p>
 

doc/html-manual/satabs-driver.shtml

@@ -195,11 +195,11 @@ will eventually consider it.
 </p>
 
 <p>
-If we ask SATABS to show us the verification claims with
+If we ask SATABS to show us the properties it verifies with
 </p>
 
 <center>
-<code>satabs driver.c spec.c --show-claims</code>
+<code>satabs driver.c spec.c --show-properties</code>
 </center>
 
 <p>
@@ -227,20 +227,20 @@ Claim dummy_open.1:<br>
 </ol>
 
 <p class="justified">
-It seems obvious that the claim dummy_open.1
+It seems obvious that the property dummy_open.1
 can never be violated. SATABS confirms
 this assumption: We call
 </p>
 
 <center>
-<code>satabs driver.c spec.c --claim dummy_open.1</code>
+<code>satabs driver.c spec.c --property dummy_open.1</code>
 </center>
 
 <p class="justified">
 and SATABS reports <code>VERIFICATION SUCCESSFUL</code> after a few iterations.
 </p>
 
-<p class="justified"> If we try to verify claim unregister_chrdev.1, SATABS
+<p class="justified"> If we try to verify property unregister_chrdev.1, SATABS
 reports that the property in line 18 in file spec.c is violated (i.e., the
 assertion does not hold, therefore the <code>VERIFICATION FAILED</code>). 
 Furthermore, SATABS provides a detailed description of the problem in the

doc/html-manual/satabs.shtml

@@ -77,20 +77,20 @@ CBMC</a> will never terminate.</p>
 <h3>Working with Claims</h3>
 
 <p class="justified">
-The two assertions will give rise to two <i>claims</i>.
-Each claim is associated to a specific line of code, i.e., a claim is violated when the
+The two assertions will give rise to two <i>properties</i>.
+Each property is associated to a specific line of code, i.e., a property is violated when
 some condition can become false at the corresponding program location.
-SATABS will generate a list of all claims for the programs as follows:
+SATABS will generate a list of all properties for the programs as follows:
 </p>
 
 <center>
 <code>
-satabs lock-example-fixed.c --show-claims
+satabs lock-example-fixed.c --show-properties
 </code>
 </center>
 
-<p>SATABS will list two claims; each claim corresponds to one of the
-two assertions. We can use SATABS to verify both claims
+<p>SATABS will list two properties; each property corresponds to one of the
+two assertions. We can use SATABS to verify both properties
 as follows:
 </p>
 
@@ -106,13 +106,13 @@ assertions hold for execution traces of any length.
 </p>
 
 <p class="justified">
-By default, SATABS attempts to verify all claims at once.
-A single claim can be verified (or refuted) by using the
-<code>--claim <i>id</i></code> option of SATABS,
-where <code><i>id</i></code> denotes the identifier of the claim in the list
-obtained by calling SATABS with the <code>--show-claims</code> flag. Whenever
-a claim is violated, SATABS reports a feasible path that leads to a state
-in which the condition that corresponds to the violated claim evaluates to
+By default, SATABS attempts to verify all properties at once.
+A single property can be verified (or refuted) by using the
+<code>--property <i>id</i></code> option of SATABS,
+where <code><i>id</i></code> denotes the identifier of the property in the list
+obtained by calling SATABS with the <code>--show-properties</code> flag. Whenever
+a property is violated, SATABS reports a feasible path that leads to a state
+in which the condition that corresponds to the violated property evaluates to
 false.
 </p>
 
@@ -159,7 +159,7 @@ achieve <b>full</b> path and state coverage (due to the fact that
 predicate abstraction implicitly detects equivalence classes).
 However, it is not guaranteed that SATABS terminates in all cases.
 Keep in mind that you must not make any assumptions about the
-validity of the claims if SATABS did not run to completion!
+validity of the properties if SATABS did not run to completion!
 </p>
 
 <div class="box1">