CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
nondet_padding.h
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2
5
6#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_ENCODING_NONDET_PADDING_H
7#define CPROVER_SOLVERS_SMT2_INCREMENTAL_ENCODING_NONDET_PADDING_H
8
10#include <util/expr.h>
11#include <util/invariant.h>
12
15
21{
22public:
24
30};
31
32template <>
34{
36}
37
39{
42 "Nondet padding is expected to pad a bit vector type.");
43}
44
45#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_ENCODING_NONDET_PADDING_H
Pre-defined bitvector types.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:344
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
const irep_idt & id() const
Definition irep.h:388
This expression serves as a placeholder for the bits which have non deterministic value in a larger b...
nondet_padding_exprt(typet type)
static const irep_idt ID_nondet_padding
The type of an expression, extends irept.
Definition type.h:29
STL namespace.
bool can_cast_expr< nondet_padding_exprt >(const exprt &base)
void validate_expr(const nondet_padding_exprt &padding)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423