cprover
|
#include "std_expr.h"
#include <cassert>
#include "arith_tools.h"
#include "byte_operators.h"
#include "c_types.h"
#include "namespace.h"
#include "pointer_offset_size.h"
#include "std_types.h"
Go to the source code of this file.
Functions | |
exprt | disjunction (const exprt::operandst &op) |
exprt | conjunction (const exprt::operandst &op) |
static void | build_object_descriptor_rec (const namespacet &ns, const exprt &expr, object_descriptor_exprt &dest) |
Build an object_descriptor_exprt from a given expr. More... | |
static constant_exprt | integer_constant (unsigned v) |
|
static |
Build an object_descriptor_exprt from a given expr.
Definition at line 65 of file std_expr.cpp.
References index_exprt::array(), irept::id(), index_exprt::index(), index_type(), irept::is_not_nil(), member_offset_expr(), object_descriptor_exprt::object(), object_descriptor_exprt::offset(), byte_extract_exprt::op(), typecast_exprt::op(), size_of_expr(), member_exprt::struct_op(), to_byte_extract_expr(), to_index_expr(), to_member_expr(), to_typecast_expr(), and exprt::type().
Referenced by object_descriptor_exprt::build().
exprt conjunction | ( | const exprt::operandst & | ) |
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) returns true otherwise
Definition at line 50 of file std_expr.cpp.
References exprt::operands().
Referenced by and_exprt::and_exprt(), bmc_all_propertiest::goalt::as_expr(), path_symext::assign_rec(), partial_order_concurrencyt::before(), collect_mcdc_controlling_rec(), acceleration_utilst::do_arrays(), instantiate_quantifier(), instrument_intervals(), interval_domaint::make_expression(), bmc_covert::operator()(), operator-=(), operator|=(), and replacement_conjunction().
exprt disjunction | ( | const exprt::operandst & | ) |
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) returns false otherwise
Definition at line 26 of file std_expr.cpp.
References exprt::operands().
Referenced by bmc_covert::goalt::as_expr(), cover_goalst::constraint(), symex_target_equationt::convert_assertions(), character_refine_preprocesst::expr_of_is_defined(), character_refine_preprocesst::expr_of_is_title_case(), character_refine_preprocesst::expr_of_is_unicode_identifier_part(), character_refine_preprocesst::expr_of_is_whitespace(), character_refine_preprocesst::in_list_expr(), instantiate_quantifier(), remove_instanceoft::lower_instanceof(), or_exprt::or_exprt(), and goto_checkt::pointer_validity_check().
|
static |
Definition at line 138 of file std_expr.cpp.
References constant_exprt::constant_exprt().
Referenced by extractbits_exprt::extractbits_exprt().