36 if(arguments.size() < 2)
39 log.
error() << identifier <<
" expects at least two arguments"
49 log.
error() << identifier <<
" takes a pointer as first argument"
61 result.add_source_location() = source_location;
75 if(arguments.size() < 3)
78 log.
error() << identifier <<
" expects at least three arguments"
88 log.
error() << identifier <<
" takes a pointer as first argument"
104 result.add_source_location() = source_location;
118 if(arguments.empty())
121 log.
error() << identifier <<
" expects at least one argument"
131 log.
error() << identifier <<
" takes a pointer as first argument"
139 result.add_source_location() = source_location;
153 if(arguments.size() != 2)
165 log.
error() << identifier <<
" takes a pointer as first argument"
175 result.add_source_location() = source_location;
188 if(arguments.size() != 3)
200 log.
error() << identifier <<
" takes a pointer as first argument"
213 result.add_source_location() = source_location;
226 if(arguments.size() != 3)
238 log.
error() << identifier <<
" takes a pointer as first argument"
251 result.add_source_location() = source_location;
265 if(arguments.size() != 3)
275 log.
error() << identifier <<
" takes a pointer as first argument"
283 log.
error() << identifier <<
" takes a pointer as second argument"
296 result.add_source_location() = source_location;
309 if(arguments.size() != 4)
319 log.
error() << identifier <<
" takes a pointer as first argument"
327 log.
error() << identifier <<
" takes a pointer as second argument"
335 log.
error() << identifier <<
" takes a pointer as third argument"
349 result.add_source_location() = source_location;
365 if(arguments.size() != 6)
375 log.
error() << identifier <<
" takes a pointer as first argument"
383 log.
error() << identifier <<
" takes a pointer as second argument"
393 log.
error() << identifier <<
" takes a pointer as third argument"
407 parameters.push_back(
427 if(arguments.size() != 3)
430 log.
error() <<
"__atomic_*_fetch primitives take three arguments"
441 <<
"__atomic_*_fetch primitives take a pointer as first argument"
452 result.add_source_location() = source_location;
464 if(arguments.size() != 3)
467 log.
error() <<
"__atomic_fetch_* primitives take three arguments"
478 <<
"__atomic_fetch_* primitives take a pointer as first argument"
489 result.add_source_location() = source_location;
616 symbol.base_name =
"result";
617 symbol.location = source_location;
618 symbol.is_file_local =
true;
619 symbol.is_lvalue =
true;
620 symbol.is_thread_local =
true;
622 symbol_table.
add(symbol);
771 std::move(arguments),
833 assign.add_source_location() = source_location;
1171 assign.add_source_location() = source_location;
1385 statement.add_source_location() = source_location;
1399 if(identifier ==
"__builtin_shuffle")
1403 if(arguments.size() != 2 && arguments.size() != 3)
1406 error() <<
"__builtin_shuffle expects two or three arguments" <<
eom;
1410 for(
exprt &arg : arguments)
1415 error() <<
"__builtin_shuffle expects vector arguments" <<
eom;
1424 if(arguments.size() == 3)
1429 error() <<
"__builtin_shuffle expects input vectors of the same type"
1433 arg1 = arguments[1];
1435 const exprt &indices = arguments.back();
1445 if(
arg1.has_value())
1455 mod_index.add_source_location() = source_location;
1456 operands.push_back(std::move(
mod_index));
1461 else if(identifier ==
"__builtin_shufflevector")
1464 if(arguments.size() < 2)
1467 error() <<
"__builtin_shufflevector expects two or more arguments" <<
eom;
1472 operands.reserve(arguments.size() - 2);
1474 for(std::size_t i = 0; i < arguments.size(); ++i)
1481 error() <<
"__builtin_shufflevector expects two vectors as argument"
1490 error() <<
"__builtin_shufflevector expects integer index" <<
eom;
1502 operands.back().add_source_location() = source_location;
1505 operands.push_back(
arg_i);
1510 arguments[0], arguments[1], std::move(operands)};
bool is_signed_or_unsigned_bitvector(const typet &type)
This method tests, if the given typet is a signed or unsigned bitvector.
API to expression classes that are internal to the C frontend.
ANSI-C Language Type Checking.
static void instantiate_atomic_exchange_n(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > ¶meter_exprs, symbol_table_baset &symbol_table, code_blockt &block)
static void instantiate_atomic_exchange(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > ¶meter_exprs, code_blockt &block)
static symbol_exprt typecheck_atomic_fetch_op(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
static void instantiate_atomic_op_fetch(const irep_idt &identifier, const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > ¶meter_exprs, symbol_table_baset &symbol_table, code_blockt &block)
static void instantiate_atomic_load(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > ¶meter_exprs, code_blockt &block)
static symbol_exprt typecheck_atomic_compare_exchange(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
static void instantiate_sync_lock_test_and_set(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > ¶meter_exprs, symbol_table_baset &symbol_table, code_blockt &block)
static symbol_exprt typecheck_sync_with_pointer_parameter(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
static void instantiate_atomic_store(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > ¶meter_exprs, code_blockt &block)
static void instantiate_atomic_load_n(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > ¶meter_exprs, symbol_table_baset &symbol_table, code_blockt &block)
static void instantiate_atomic_compare_exchange_n(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > ¶meter_exprs, code_blockt &block)
static symbol_exprt typecheck_atomic_exchange(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
static symbolt result_symbol(const irep_idt &identifier, const typet &type, const source_locationt &source_location, symbol_table_baset &symbol_table)
static void instantiate_sync_val_compare_and_swap(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > ¶meter_exprs, symbol_table_baset &symbol_table, code_blockt &block)
static void instantiate_atomic_compare_exchange(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > ¶meter_exprs, symbol_table_baset &symbol_table, code_blockt &block)
static symbol_exprt typecheck_atomic_op_fetch(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
static symbol_exprt typecheck_atomic_store_n(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
static void instantiate_sync_bool_compare_and_swap(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > ¶meter_exprs, code_blockt &block)
static symbol_exprt typecheck_sync_lock_release(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
static symbol_exprt typecheck_atomic_load_n(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
static symbol_exprt typecheck_atomic_exchange_n(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
static void instantiate_sync_lock_release(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > ¶meter_exprs, code_blockt &block)
static void instantiate_sync_fetch(const irep_idt &identifier, const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > ¶meter_exprs, code_blockt &block)
static void instantiate_atomic_store_n(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > ¶meter_exprs, code_blockt &block)
static symbol_exprt typecheck_sync_compare_swap(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
static void instantiate_atomic_fetch_op(const irep_idt &identifier, const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > ¶meter_exprs, symbol_table_baset &symbol_table, code_blockt &block)
static symbol_exprt typecheck_atomic_load_store(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
signedbv_typet signed_int_type()
pointer_typet pointer_type(const typet &subtype)
bitvector_typet c_index_type()
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A base class for binary expressions.
symbol_table_baset & symbol_table
virtual void make_constant(exprt &expr)
virtual code_blockt instantiate_gcc_polymorphic_builtin(const irep_idt &identifier, const symbol_exprt &function_symbol)
virtual optionalt< symbol_exprt > typecheck_gcc_polymorphic_builtin(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location)
virtual exprt typecheck_shuffle_vector(const side_effect_expr_function_callt &expr)
A codet representing sequential composition of program statements.
code_operandst & statements()
void add(const codet &code)
codet representation of an expression statement.
A codet representing an assignment in the program.
A codet representing the declaration of a local variable.
codet representation of an if-then-else statement.
goto_instruction_codet representation of a "return from a function" statement.
std::vector< parametert > parameterst
Data structure for representing an arbitrary statement in a program.
A constant literal expression.
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
source_locationt & add_source_location()
source_locationt source_location
Class that provides messages with a built-in verbosity 'level'.
message_handlert & get_message_handler()
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
const typet & base_type() const
The type of the data what we point to.
Shuffle elements of one or two vectors, modelled after Clang's __builtin_shufflevector.
A side_effect_exprt representation of a function call side effect.
exprt::operandst & arguments()
Expression to hold a symbol (variable)
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
The symbol table base class interface.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
const std::string & id2string(const irep_idt &d)
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.