Skip to content

Updated language use in cbmc-tutorial.md #3532

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Dec 5, 2018
Merged

Updated language use in cbmc-tutorial.md #3532

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
25 changes: 12 additions & 13 deletions doc/cprover-manual/cbmc-tutorial.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,13 +2,13 @@

### Example: Buffer Overflows

In order to give a brief overview of the capabilities of CBMC
we start with a small example. The issue of *[buffer
To give a brief overview of the capabilities of CBMC
we start with a simple example. The issue of *[buffer
overflows](http://en.wikipedia.org/wiki/Buffer_overflow)* has obtained
wide public attention. A buffer is a contiguously-allocated chunk of
wide public attention. A buffer is a contiguously allocated chunk of
memory, represented by an array or a pointer in C. Programs written in C
do not provide automatic bounds checking on the buffer, which means a
program can – accidentally or maliciously – write past a buffer. The
program can – accidentally or deliberately – write beyond a buffer. The
following example is a perfectly valid C program (in the sense that a
compiler compiles it without any errors):

Expand All @@ -25,7 +25,7 @@ region can lead to unexpected behavior. In particular, such bugs can be
exploited to overwrite the return address of a function, thus enabling
the execution of arbitrary user-induced code. CBMC is able
to detect this problem and reports that the "upper bound property" of
the buffer is violated. CBMC is capable of checking these
the buffer has been violated. CBMC is capable of checking these
lower and upper bounds, even for arrays with dynamic size. A detailed
discussion of the properties that CBMC can check
automatically is \ref man_instrumentation-properties "here".
Expand Down Expand Up @@ -58,7 +58,7 @@ int main(int argc, char **argv)

Of course, this program is faulty, as the `argv` array might have fewer
than three elements, and then the array access `argv[2]` is out of
bounds. Now, run CBMC as follows:
bounds. Now, run CBMC:

```
cbmc file1.c --show-properties --bounds-check --pointer-check
Expand Down Expand Up @@ -106,8 +106,7 @@ to a SAT solver (more background on this step is in the book on
[Decision Procedures](http://www.decision-procedures.org/)). It then
determines which of the properties that it has generated for the program
hold and which do not. Using the SAT solver, CBMC detects that the
property for the object bounds of `argv` does not hold, and will thus
print a line as follows:
property for the object bounds of `argv` does not hold, and will display:

```plaintext
[main.pointer_dereference.6] dereference failure: pointer outside object bounds in argv[(signed long int)2]: FAILURE
Expand All @@ -117,11 +116,11 @@ print a line as follows:

Let us have a closer look at this property and why it fails. To aid the
understanding of the problem, CBMC can generate a *counterexample trace*
for failed properties. To obtain this trace, run
for failed properties. To obtain this trace, run:

cbmc file1.c --bounds-check --trace

CBMC then prints a counterexample trace, i.e., a program trace that
CBMC then prints a counterexample trace, that is, a program trace that
begins with `main` and ends in a state which violates the property. In
our example, the program trace ends in the faulty array access. It also
gives the values the input variables must have for the bug to occur. In
Expand Down Expand Up @@ -149,7 +148,7 @@ int sum() {
}
```

In order to set the entry point to the `sum` function, run
To set the entry point to the `sum` function, run:

```plaintext
cbmc file2.c --function sum --bounds-check
Expand Down Expand Up @@ -274,7 +273,7 @@ the argument is too small, CBMC will detect that not enough unwinding is
done reports that an unwinding assertion has failed.

Reconsider the example. For a loop unwinding bound of one, no bug is
found. But already for a bound of two, CBMC detects a trace that
found. But for a bound of two, CBMC detects a trace that
violates an assertion. Without unwinding assertions, or when using the
`--depth` command line switch, CBMC does not prove the program correct,
but it can be helpful to find program bugs. The various command line
Expand All @@ -292,7 +291,7 @@ requirements:
contain *declarations* of the functions that are to be used.
2. Appropriate *definitions* have to be provided.

Most C compilers come with header files for the ANSI-C library
Most C compilers come with header files for the ANSI C library
functions. We briefly discuss how to obtain/install these library files.

#### Linux
Expand Down