39 const irep_idt &identifier =
function.get_identifier();
42 if(arguments.size() != 2)
45 error() <<
"'" << identifier <<
"' expected to have two arguments" <<
eom;
52 error() <<
"'" << identifier <<
"' expected to have LHS" <<
eom;
59 if(lhs.
type().
id() != ID_unsignedbv && lhs.
type().
id() != ID_signedbv)
62 error() <<
"'" << identifier <<
"' expected other type" <<
eom;
67 arguments[0].type().
id() != lhs.
type().
id() ||
68 arguments[1].type().id() != lhs.
type().
id())
71 error() <<
"'" << identifier
72 <<
"' expected operands to be of same type as LHS" <<
eom;
79 error() <<
"'" << identifier
80 <<
"' expected operands to be constant literals" <<
eom;
91 error() <<
"error converting operands" <<
eom;
98 error() <<
"expected lower bound to be smaller or equal to the "
99 <<
"upper bound" <<
eom;
103 rhs.add_to_operands(
exprt{arguments[0]},
exprt{arguments[1]});
116 const irep_idt &identifier =
function.get_identifier();
119 if(arguments.size() != 2)
122 error() <<
"'" << identifier <<
"' expected to have two arguments" <<
eom;
129 error() <<
"'" << identifier <<
"' expected to have LHS" <<
eom;
138 error() <<
"'" << identifier <<
"' expected bool" <<
eom;
142 if(arguments[0].type().
id() != ID_unsignedbv || !arguments[0].
is_constant())
145 error() <<
"'" << identifier <<
"' expected first operand to be "
146 <<
"a constant literal of type unsigned long" <<
eom;
150 if(arguments[1].type().
id() != ID_unsignedbv || !arguments[1].
is_constant())
153 error() <<
"'" << identifier <<
"' expected second operand to be "
154 <<
"a constant literal of type unsigned long" <<
eom;
165 error() <<
"error converting operands" <<
eom;
172 error() <<
"probability has to be smaller than 1" <<
eom;
179 error() <<
"denominator may not be zero" <<
eom;
183 rationalt numerator(num), denominator(den);
184 rationalt prob = numerator / denominator;
199 const irep_idt &f_id =
function.get_identifier();
203 codet printf_code(ID_printf, arguments,
function.source_location());
213 const irep_idt &f_id =
function.get_identifier();
217 if(arguments.empty())
220 error() <<
"scanf takes at least one argument" <<
eom;
232 std::size_t argument_number = 1;
234 for(
const auto &t : token_list)
240 if(argument_number < arguments.size())
246 if(type->id() == ID_array)
255 *type,
"scanf_string", dest,
function.source_location());
263 codet array_copy_statement;
265 array_copy_statement.
operands().resize(2);
266 array_copy_statement.
op0()=ptr;
267 \ array_copy_statement.
op1()=rhs;
269 function.source_location();
288 *type,
function.source_location());
311 const exprt &
function,
315 if(arguments.size() < 2)
318 error() <<
"input takes at least two arguments" <<
eom;
326 const exprt &
function,
330 if(arguments.size() < 2)
333 error() <<
"output takes at least two arguments" <<
eom;
349 error() <<
"atomic_begin does not expect an LHS" <<
eom;
353 if(!arguments.empty())
356 error() <<
"atomic_begin takes no arguments" <<
eom;
372 error() <<
"atomic_end does not expect an LHS" <<
eom;
376 if(!arguments.empty())
379 error() <<
"atomic_end takes no arguments" <<
eom;
394 error() <<
"do_cpp_new without lhs is yet to be implemented" <<
eom;
401 bool new_array = rhs.
get(ID_statement) == ID_cpp_new_array;
416 exprt tmp_symbol_expr;
423 ns.
lookup(new_array ?
"__new_array" :
"__new").symbol_expr();
431 "new has one or two parameters");
444 new_call.
lhs() = tmp_symbol_expr;
447 convert(new_call, dest, ID_cpp);
453 ns.
lookup(new_array ?
"__placement_new_array" :
"__placement_new")
462 "placement new has two or three parameters");
476 new_call.
lhs() = tmp_symbol_expr;
479 for(std::size_t i = 0; i < code_type.
parameters().size(); i++)
485 convert(new_call, dest, ID_cpp);
490 error() <<
"cpp_new expected to have 0 or 1 operands" <<
eom;
515 exprt initializer =
static_cast<const exprt &
>(rhs.
find(ID_initializer));
539 if(src.
id() == ID_typecast)
542 if(src.
id() != ID_address_of)
545 error() <<
"expected array-pointer as argument" <<
eom;
551 if(address_of_expr.object().id() != ID_index)
554 error() <<
"expected array-element as argument" <<
eom;
558 const auto &index_expr =
to_index_expr(address_of_expr.object());
560 if(index_expr.array().type().id() != ID_array)
563 error() <<
"expected array as argument" <<
eom;
567 return index_expr.array();
577 if(arguments.size() != 2)
580 error() <<
id <<
" expects two arguments" <<
eom;
584 codet array_op_statement(
id);
585 array_op_statement.
operands() = arguments;
590 if(
id == ID_array_equal)
601 if(result.
id() == ID_address_of)
605 result = address_of_expr.object();
608 while(result.
type().
id() == ID_array &&
628 auto source_location =
function.find_source_location();
629 source_location.add_pragma(
"disable:pointer-check");
630 source_location.add_pragma(
"disable:pointer-overflow-check");
631 source_location.add_pragma(
"disable:pointer-primitive-check");
634 if(arguments.size() != 2)
637 error() <<
"'" << identifier <<
"' expected to have two arguments" <<
eom;
642 if(arguments[0].type().
id() != ID_pointer)
645 error() <<
"'" << identifier
646 <<
"' first argument expected to have `void *` type" <<
eom;
650 if(arguments[1].type().
id() != ID_unsignedbv)
653 error() <<
"'" << identifier
654 <<
"' second argument expected to have `size_t` type" <<
eom;
662 error() <<
"'" << identifier <<
"' not expected to have a LHS" <<
eom;
674 annotated_location.
set(
"user-provided",
false);
677 "assertion havoc_slice " +
from_expr(
ns, identifier, ok_expr));
682 const symbolt &nondet_contents =
683 new_tmp_symbol(array_type,
"nondet_contents", dest, source_location, mode);
692 codet array_replace(ID_array_replace, {arg0, arg1}, source_location);
713 error() <<
"'alloca' function called, but 'alloca' has not been declared "
714 <<
"with expected 'void *' return type." <<
eom;
718 alloca_type.parameters().size() != 1 ||
719 alloca_type.parameters()[0].type() !=
size_type())
722 error() <<
"'alloca' function called, but 'alloca' has not been declared "
723 <<
"with expected single 'size_t' parameter." <<
eom;
735 alloca_type.return_type(),
"alloca", dest, source_location, mode)
749 function.source_location().get_function() ==
"alloca" || !
targets.
prefix ||
760 alloca_type.return_type(),
761 id2string(
function.source_location().get_function()),
782 this_alloca_ptr, std::move(rhs), source_location));
791 exprt alloca_result =
798 std::move(alloca_result)};
800 std::move(dead_object_sym), std::move(not_null), source_location);
816 if(
function.get_bool(ID_C_invalid_object))
820 const irep_idt &identifier =
function.get_identifier();
826 error() <<
"function '" << identifier <<
"' not found" <<
eom;
830 if(symbol->
type.
id() != ID_code)
833 error() <<
"function '" << identifier <<
"' type mismatch: expected code"
871 identifier ==
CPROVER_PREFIX "assume" || identifier ==
"__VERIFIER_assume")
873 if(arguments.size() != 1)
876 error() <<
"'" << identifier <<
"' expected to have one argument" <<
eom;
882 annotated_location.
set(
"user-provided",
true);
885 annotated_location));
890 error() << identifier <<
" expected not to have LHS" <<
eom;
894 else if(identifier ==
"__VERIFIER_error")
896 if(!arguments.empty())
899 error() <<
"'" << identifier <<
"' expected to have no arguments" <<
eom;
904 annotated_location.
set(
"user-provided",
true);
911 error() << identifier <<
" expected not to have LHS" <<
eom;
917 annotated_location =
function.source_location();
918 annotated_location.
set(
"user-provided",
true);
920 dest.
instructions.back().labels.push_back(
"__VERIFIER_abort");
923 identifier ==
"assert" &&
926 if(arguments.size() != 1)
929 error() <<
"'" << identifier <<
"' expected to have one argument" <<
eom;
935 annotated_location.
set(
"user-provided",
true);
938 "assertion " +
from_expr(
ns, identifier, arguments.front()));
941 annotated_location));
946 error() << identifier <<
" expected not to have LHS" <<
eom;
955 if(arguments.size() != 2)
958 error() <<
"'" << identifier <<
"' expected to have two arguments" <<
eom;
962 bool is_precondition = identifier ==
CPROVER_PREFIX "precondition";
963 bool is_postcondition = identifier ==
CPROVER_PREFIX "postcondition";
973 else if(is_postcondition)
979 annotated_location.
set(
980 "user-provided", !
function.source_location().is_built_in());
988 annotated_location));
993 error() << identifier <<
" expected not to have LHS" <<
eom;
999 if(arguments.size() != 1)
1002 error() <<
"'" << identifier <<
"' expected to have one argument" <<
eom;
1009 error() << identifier <<
" expected not to have LHS" <<
eom;
1013 codet havoc(ID_havoc_object);
1021 do_printf(lhs,
function, arguments, dest);
1025 do_scanf(lhs,
function, arguments, dest);
1028 identifier ==
CPROVER_PREFIX "input" || identifier ==
"__CPROVER::input")
1033 error() << identifier <<
" expected not to have LHS" <<
eom;
1037 do_input(
function, arguments, dest);
1040 identifier ==
CPROVER_PREFIX "output" || identifier ==
"__CPROVER::output")
1045 error() << identifier <<
" expected not to have LHS" <<
eom;
1053 identifier ==
"__CPROVER::atomic_begin" ||
1054 identifier ==
"java::org.cprover.CProver.atomicBegin:()V" ||
1055 identifier ==
"__VERIFIER_atomic_begin")
1061 identifier ==
"__CPROVER::atomic_end" ||
1062 identifier ==
"java::org.cprover.CProver.atomicEnd:()V" ||
1063 identifier ==
"__VERIFIER_atomic_end")
1087 if(lhs.
type().
id() == ID_c_bool)
1090 rhs.
set(ID_C_identifier, identifier);
1096 rhs.
set(ID_C_identifier, identifier);
1109 if(
function.type().get_bool(ID_C_incomplete))
1112 error() <<
"'" << identifier <<
"' is not declared, "
1113 <<
"missing type information required to construct call to "
1114 <<
"uninterpreted function" <<
eom;
1120 for(
const auto ¶meter : function_call_type.
parameters())
1121 domain.push_back(parameter.type());
1128 assignment.add_source_location() =
function.source_location();
1133 do_array_op(ID_array_equal, lhs,
function, arguments, dest);
1137 do_array_op(ID_array_set, lhs,
function, arguments, dest);
1141 do_array_op(ID_array_copy, lhs,
function, arguments, dest);
1145 do_array_op(ID_array_replace, lhs,
function, arguments, dest);
1148 identifier ==
"__assert_fail" || identifier ==
"_assert" ||
1149 identifier ==
"__assert_c99" || identifier ==
"_wassert")
1170 if(arguments.size() != 4 && arguments.size() != 3)
1173 error() <<
"'" << identifier <<
"' expected to have four arguments"
1182 annotated_location.
set(
"user-provided",
true);
1188 else if(identifier ==
"__assert_rtn" || identifier ==
"__assert")
1199 if(arguments.size() == 4)
1203 else if(arguments.size() == 3)
1210 error() <<
"'" << identifier <<
"' expected to have four arguments"
1216 annotated_location.
set(
"user-provided",
true);
1223 identifier ==
"__assert_func" || identifier ==
"__assert2" ||
1224 identifier ==
"__assert13")
1231 if(arguments.size() != 4)
1234 error() <<
"'" << identifier <<
"' expected to have four arguments"
1249 description =
"assertion";
1253 annotated_location.
set(
"user-provided",
true);
1261 if(arguments.empty())
1264 error() <<
"'" << identifier <<
"' expected to have at least one argument"
1269 codet fence(ID_fence);
1271 for(
const auto &argument : arguments)
1276 else if(identifier ==
"__builtin_prefetch")
1280 else if(identifier ==
"__builtin_unreachable")
1284 else if(identifier == ID_gcc_builtin_va_arg)
1292 if(arguments.size() != 1)
1295 error() <<
"'" << identifier <<
"' expected to have one argument" <<
eom;
1303 exprt list_arg_cast = list_arg;
1305 list_arg.
type().
id() == ID_pointer &&
1323 ID_C_va_arg_type,
to_code_type(
function.type()).return_type());
1325 std::move(assign),
function.source_location()));
1327 else if(identifier ==
"__builtin_va_copy")
1329 if(arguments.size() != 2)
1332 error() <<
"'" << identifier <<
"' expected to have two arguments" <<
eom;
1342 error() <<
"va_copy argument expected to be lvalue" <<
eom;
1347 dest_expr, src_expr,
function.source_location()));
1349 else if(identifier ==
"__builtin_va_start" || identifier ==
"__va_start")
1353 if(arguments.size() != 2)
1356 error() <<
"'" << identifier <<
"' expected to have two arguments" <<
eom;
1365 error() <<
"va_start argument expected to be lvalue" <<
eom;
1370 dest_expr.
type().
id() == ID_pointer &&
1379 rhs.add_to_operands(
1383 std::move(dest_expr), std::move(rhs),
function.source_location()));
1385 else if(identifier ==
"__builtin_va_end")
1388 if(arguments.size() != 1)
1391 error() <<
"'" << identifier <<
"' expected to have one argument" <<
eom;
1400 error() <<
"va_end argument expected to be lvalue" <<
eom;
1405 if(dest_expr.
type().
id() == ID_pointer)
1411 dest_expr, *zero,
function.source_location()));
1415 identifier ==
"__builtin_isgreater" ||
1416 identifier ==
"__builtin_isgreaterequal" ||
1417 identifier ==
"__builtin_isless" || identifier ==
"__builtin_islessequal" ||
1418 identifier ==
"__builtin_islessgreater" ||
1419 identifier ==
"__builtin_isunordered")
1424 arguments.size() != 2 ||
1431 error() <<
"'" << identifier
1432 <<
"' expected to have two float/double arguments" <<
eom;
1438 bool use_double = arguments[0].type() ==
double_type();
1439 if(arguments[0].type() != arguments[1].type())
1456 const typet &a_t = new_arguments[0].type();
1463 name += use_double ?
'd' :
'f';
1467 "builtin declaration should match constructed type");
1471 new_function.
type() = f_type;
1478 else if(identifier ==
"alloca" || identifier ==
"__builtin_alloca")
1480 do_alloca(lhs,
function, arguments, dest, mode);
exprt make_va_list(const exprt &expr)
floatbv_typet float_type()
signedbv_typet signed_int_type()
pointer_typet pointer_type(const typet &subtype)
signedbv_typet pointer_diff_type()
bitvector_typet char_type()
bitvector_typet c_index_type()
floatbv_typet double_type()
Operator to return the address of an object.
const typet & element_type() const
The type of the elements of the array.
const exprt & size() const
A goto_instruction_codet representing an assignment in the program.
goto_instruction_codet representation of a function call statement.
A goto_instruction_codet representing the declaration that an output of a particular description has ...
std::vector< parametert > parameterst
const typet & return_type() const
const parameterst & parameters() const
Data structure for representing an arbitrary statement in a program.
void set_statement(const irep_idt &statement)
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
Base class for all expressions.
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
std::vector< exprt > operandst
bool is_one() const
Return whether the expression is a constant representing 1.
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
source_locationt & add_source_location()
const source_locationt & source_location() const
typet & type()
Return the type of the expression.
The Boolean constant false.
Application of (mathematical) function.
void do_havoc_slice(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
symbol_table_baset & symbol_table
void do_input(const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void do_array_op(const irep_idt &id, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
irep_idt get_string_constant(const exprt &expr)
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
void do_prob_coin(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
struct goto_convertt::targetst targets
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)
void do_atomic_end(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
virtual void do_function_call_symbol(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
add function calls to function queue for later processing
void do_output(const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void cpp_new_initializer(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
builds a goto program for object initialization after new
void do_printf(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
exprt get_array_argument(const exprt &src)
void do_alloca(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
alloca allocates memory that is freed when leaving the function (and not the block,...
void do_scanf(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
void do_atomic_begin(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
static void replace_new_object(const exprt &object, exprt &dest)
virtual void do_cpp_new(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
clean_expr_resultt clean_expr(exprt &expr, const irep_idt &mode, bool result_is_used=true)
void do_prob_uniform(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
instructionst instructions
The list of instructions in the goto program.
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
static instructiont make_other(const goto_instruction_codet &_code, const source_locationt &l=source_locationt::nil())
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
The trinary if-then-else operator.
bool get_bool(const irep_idt &name) const
const irept & find(const irep_idt &name) const
const irep_idt & get(const irep_idt &name) const
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
A type for mathematical functions (do not confuse with functions/methods in code)
std::vector< typet > domaint
source_locationt source_location
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The null pointer constant.
The plus expression Associativity is not specified.
const typet & base_type() const
The type of the data what we point to.
A base class for a predicate that indicates that an address range is ok to read or write or both.
A side_effect_exprt that returns a non-deterministically chosen value.
An expression containing a side effect.
const irep_idt & get_statement() const
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
Expression to hold a symbol (variable)
void set_identifier(const irep_idt &identifier)
symbol_exprt & with_source_location(source_locationt location) &
Add the source location from location, if it is non-nil.
const irep_idt & get_identifier() const
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
exprt value
Initial value of symbol.
const typet & subtype() const
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
const source_locationt & source_location() const
source_locationt & add_source_location()
const exprt & op1() const =delete
void destruct_locals(const std::list< irep_idt > &vars, goto_programt &dest, const namespacet &ns)
std::optional< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Expression Initialization.
bool is_assignable(const exprt &expr)
Returns true iff the argument is one of the following:
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Deprecated expression utility functions.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
const std::string & id2string(const irep_idt &d)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
API to expression classes for 'mathematical' expressions.
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
exprt object_size(const exprt &pointer)
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
const codet & to_code(const exprt &expr)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
std::list< irep_idt > temporaries
Identifiers of temporaries introduced while cleaning an expression.
void add(clean_expr_resultt &&other)
void add_temporary(const irep_idt &id)
goto_programt side_effects
Statements implementing side effects of the expression that was subject to cleaning.
const type_with_subtypet & to_type_with_subtype(const typet &type)