cprover
|
#include "std_expr.h"
#include <cassert>
#include "arith_tools.h"
#include "byte_operators.h"
#include "c_types.h"
#include "pointer_offset_size.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 |
Build an object_descriptor_exprt from a given expr.
Definition at line 63 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(), unary_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 48 of file std_expr.cpp.
References exprt::operands().
Referenced by string_constraint_generatort::add_axioms_for_characters_in_integer_string(), string_constraint_generatort::add_axioms_for_fractional_part(), bmc_all_propertiest::goalt::as_expr(), partial_order_concurrencyt::before(), collect_mcdc_controlling_rec(), acceleration_utilst::do_arrays(), instantiate(), instantiate_quantifier(), instrument_intervals(), interval_domaint::make_expression(), negation_of_not_contains_constraint(), operator-=(), operator|=(), replacement_conjunction(), and goto_checkt::rw_ok_check().
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 24 of file std_expr.cpp.
References exprt::operands().
Referenced by string_constraint_generatort::add_axioms_for_intern(), goto_checkt::address_check(), 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(), is_upper_case(), remove_instanceoft::lower_instanceof(), and float_bvt::mul().