26 error_message << identifier <<
" takes exactly 2 arguments, but "
27 << expr.
arguments().size() <<
" were provided";
39 <<
" argument 1 must be string constant (literal), but ("
61 <<
" argument 2 must be a byte-sized integer, but ("
91 error_message << identifier <<
" takes exactly 2 arguments, but "
92 << expr.
arguments().size() <<
" were provided";
108 <<
" argument 1 must be a non-void pointer, but ("
111 <<
"`. Insert a cast to the type that you want to access.";
123 <<
" argument 2 must be string constant (literal), but ("
156 error_message << identifier <<
" takes exactly 3 arguments, but "
157 << expr.
arguments().size() <<
" were provided";
173 <<
" argument 1 must be a non-void pointer, but ("
176 <<
"`. Insert a cast to the type that you want to access.";
188 <<
" argument 2 must be string constant (literal), but ("
206 <<
" argument 3 must be a boolean or of integer value, but ("
232 "expr.function() has to be a symbol_expr");
ANSI-C Language Type Checking.
static symbol_exprt typecheck_get_field(const side_effect_expr_function_callt &expr, const irep_idt &identifier, const namespacet &ns)
Function to typecheck a shadow memory get_field function.
static symbol_exprt typecheck_set_field(const side_effect_expr_function_callt &expr, const irep_idt &identifier, const namespacet &ns)
Function to typecheck a shadow memory set_field function.
static symbol_exprt typecheck_field_decl(const side_effect_expr_function_callt &expr, const irep_idt &identifier, const namespacet &ns)
Function to typecheck a shadow memory field_declaration function.
signedbv_typet signed_int_type()
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
virtual optionalt< symbol_exprt > typecheck_shadow_memory_builtin(const side_effect_expr_function_callt &expr)
Typecheck the function if it is a shadow_memory builtin and return a symbol for it.
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
const source_locationt & source_location() const
source_locationt & add_source_location()
Thrown when we can't handle something in an input source file.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
A side_effect_exprt representation of a function call side effect.
exprt::operandst & arguments()
Expression to hold a symbol (variable)
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const type_with_subtypet & to_type_with_subtype(const typet &type)