CBMC: /home/runner/work/cbmc/cbmc/src/util/std_expr.cpp File Reference
#include "std_expr.h"
#include "arith_tools.h"
#include "config.h"
#include "expr_util.h"
#include "fixedbv.h"
#include "ieee_float.h"
#include "mathematical_types.h"
#include "namespace.h"
#include "pointer_expr.h"
#include "range.h"
#include "rational.h"
#include "rational_tools.h"
#include "substitute_symbols.h"
#include <map>
Go to the source code of this file.
Functions | |
| bool | operator== (const exprt &lhs, bool rhs) |
Return whether the expression lhs is a constant of Boolean type that is representing the Boolean value rhs. | |
| bool | operator!= (const exprt &lhs, bool rhs) |
Return whether the expression lhs is not a constant of Boolean type or is not representing the Boolean value rhs. | |
| bool | operator== (const exprt &lhs, int rhs) |
Return whether the expression lhs is a constant representing the numeric value rhs; only values 0 and 1 are supported for rhs. | |
| bool | operator!= (const exprt &lhs, int rhs) |
| Returns the negation of operator==(const exprt &, int). | |
| bool | operator== (const exprt &lhs, std::nullptr_t rhs) |
Return whether the expression lhs is a constant representing the NULL pointer. | |
| bool | operator!= (const exprt &lhs, std::nullptr_t rhs) |
| Returns the negation of operator==(const exprt &, std::nullptr_t). | |
| exprt | disjunction (const exprt::operandst &op) |
| 1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) returns false otherwise | |
| exprt | conjunction (exprt a, exprt b) |
| Conjunction of two expressions. | |
| exprt | conjunction (const exprt::operandst &op) |
| 1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) returns true otherwise | |
| template<typename T > | |
| auto | component (T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0()) |
◆ component()
◆ conjunction() [1/2]
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) returns true otherwise
Definition at line 275 of file std_expr.cpp.
◆ conjunction() [2/2]
Conjunction of two expressions.
If the second is already an and_exprt add to its operands instead of creating a new expression. If one is true, return the other expression. If one is false returns false.
Definition at line 252 of file std_expr.cpp.
◆ disjunction()
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) returns false otherwise
Definition at line 240 of file std_expr.cpp.
◆ operator!=() [1/3]
Return whether the expression lhs is not a constant of Boolean type or is not representing the Boolean value rhs.
Definition at line 37 of file std_expr.cpp.
◆ operator!=() [2/3]
◆ operator!=() [3/3]
◆ operator==() [1/3]
Return whether the expression lhs is a constant of Boolean type that is representing the Boolean value rhs.
Definition at line 32 of file std_expr.cpp.
◆ operator==() [2/3]
Return whether the expression lhs is a constant representing the numeric value rhs; only values 0 and 1 are supported for rhs.
For value 0 we consider the following types: ID_integer, ID_natural, ID_rational, ID_unsignedbv, ID_signedbv, ID_c_bool, ID_c_bit_field, ID_fixedbv, ID_floatbv, ID_pointer.
For ID_pointer, returns true iff the value is a zero string or a null pointer.
For value 1 we consider the following types: ID_integer, ID_natural, ID_rational, ID_unsignedbv, ID_signedbv, ID_c_bool, ID_c_bit_field, ID_fixedbv, ID_floatbv.
For all other types, return false.
Definition at line 52 of file std_expr.cpp.
◆ operator==() [3/3]
Return whether the expression lhs is a constant representing the NULL pointer.
Definition at line 186 of file std_expr.cpp.