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
smt_is_dynamic_object.h
Go to the documentation of this file.
1
// Author: Diffblue Ltd.
2
3
#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_IS_DYNAMIC_OBJECT_H
4
#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_IS_DYNAMIC_OBJECT_H
5
6
#include <
solvers/smt2_incremental/ast/smt_commands.h
>
7
#include <
solvers/smt2_incremental/ast/smt_terms.h
>
8
14
struct
smt_is_dynamic_objectt
final
15
{
16
smt_is_dynamic_objectt
();
20
smt_declare_function_commandt
declaration
;
22
using
make_applicationt
=
23
smt_function_application_termt::factoryt<smt_command_functiont>
;
24
make_applicationt
make_application
;
27
smt_commandt
28
make_definition
(std::size_t unique_id,
bool
is_dynamic_object)
const
;
29
};
14
struct
smt_is_dynamic_objectt
final {
…
};
30
31
#endif
// CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_IS_DYNAMIC_OBJECT_H
smt_commandt
Definition
smt_commands.h:15
smt_declare_function_commandt
Definition
smt_commands.h:51
smt_function_application_termt::factoryt< smt_command_functiont >
smt_commands.h
smt_terms.h
smt_is_dynamic_objectt
Specifics of how the dynamic object status lookup is implemented in SMT terms.
Definition
smt_is_dynamic_object.h:15
smt_is_dynamic_objectt::make_application
make_applicationt make_application
Definition
smt_is_dynamic_object.h:24
smt_is_dynamic_objectt::smt_is_dynamic_objectt
smt_is_dynamic_objectt()
Definition
smt_is_dynamic_object.cpp:17
smt_is_dynamic_objectt::declaration
smt_declare_function_commandt declaration
The command for declaring the is_dynamic_object function.
Definition
smt_is_dynamic_object.h:20
smt_is_dynamic_objectt::make_definition
smt_commandt make_definition(std::size_t unique_id, bool is_dynamic_object) const
Makes the command to define the resulting is_dynamic_object status for calls to the is_dynamic_object...
Definition
smt_is_dynamic_object.cpp:23
src
solvers
smt2_incremental
smt_is_dynamic_object.h
Generated by
1.9.8
1.9.8