CBMC
Toggle main menu visibility
Main Page
Related Pages
Namespaces
Namespace List
Namespace Members
All
a
c
d
e
f
g
j
l
m
r
t
w
Functions
a
c
d
f
g
r
t
w
Typedefs
Enumerations
Classes
Class List
Class Hierarchy
Class Members
All
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
x
y
z
~
Functions
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
x
y
z
~
Variables
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
x
y
z
Typedefs
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
Enumerations
a
b
c
d
e
f
g
i
k
l
m
o
p
r
s
t
u
v
w
Enumerator
a
b
c
d
e
f
h
i
k
l
m
n
o
p
q
r
s
t
u
v
Related Symbols
b
c
d
e
g
i
j
m
n
o
s
t
u
v
Files
File List
File Members
All
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
x
y
z
Functions
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
r
s
t
u
v
w
x
y
z
Variables
_
a
b
c
d
e
f
g
i
l
m
n
o
p
r
s
t
u
w
y
Typedefs
_
a
b
c
d
e
f
g
h
i
j
l
m
n
o
p
r
s
t
u
v
w
Enumerations
_
a
b
c
d
f
g
i
l
m
p
r
s
t
u
v
w
Enumerator
_
a
c
d
e
f
g
h
i
l
m
n
o
p
r
s
t
u
v
w
Macros
_
a
b
c
d
e
f
g
h
i
j
l
m
n
o
p
q
r
s
t
u
v
w
x
y
•
All
Classes
Namespaces
Files
Functions
Variables
Typedefs
Enumerations
Enumerator
Friends
Macros
Modules
Pages
Loading...
Searching...
No Matches
Related Pages
Here is a list of all related documentation pages:
[detail level
1
2
3
4
5
6
]
▼
Code Contracts in CBMC
▼
Code Contracts User Documentation
Function Contracts
Loop Contracts
Requires and Ensures Clauses
Assigns Clauses
Frees Clauses
Loop Invariant Clauses
Decreases Clauses
Memory Predicates
Function Pointer Predicates
History Variables
Quantifiers
Command Line Interface for Code Contracts
▼
Code Contracts Developer Documentation
▼
Code Contracts Transformation Specification
Function Contracts Reminder
Program Transformation Overview
Generating GOTO Functions From Contract Clauses
Rewriting Declarative Assign and Frees Specification Functions
Rewriting User-Defined Memory Predicates
▼
Dynamic Frame Condition Checking
Write Set Representation
▼
GOTO Function Instrumentation
Rewriting Calls to __CPROVER_is_freeable and __CPROVER_was_freed Predicates
Rewriting Calls to the __CPROVER_is_fresh Predicate
Rewriting Calls to the __CPROVER_obeys_contract Predicate
Rewriting Calls to the __CPROVER_pointer_in_range_dfcc Predicate
Rewriting Calls to the __CPROVER_pointer_equals Predicate
Proof Harness Intrumentation
Checking a Contract Against a Function
Checking a Contract Against a Recursive Function
Replacing a Function by a Contract
Code Contracts Software Architecture
The CPROVER C++ API
Libcprover-rust
Symex and GOTO program instructions
Deprecated List
Generated by
1.9.8
1.9.8