35 const irep_idt &identifier =
function.get_identifier();
38 if(arguments.size()!=2)
41 error() <<
"`" << identifier
42 <<
"' expected to have two arguments" <<
eom;
49 error() <<
"`" << identifier <<
"' expected to have LHS" <<
eom;
56 if(lhs.
type().
id()!=ID_unsignedbv &&
57 lhs.
type().
id()!=ID_signedbv)
60 error() <<
"`" << identifier <<
"' expected other type" <<
eom;
64 if(arguments[0].type().
id()!=lhs.
type().
id() ||
65 arguments[1].type().id()!=lhs.
type().
id())
68 error() <<
"`" << identifier
69 <<
"' expected operands to be of same type as LHS" <<
eom;
73 if(!arguments[0].is_constant() ||
74 !arguments[1].is_constant())
77 error() <<
"`" << identifier
78 <<
"' expected operands to be constant literals" <<
eom;
88 error() <<
"error converting operands" <<
eom;
95 error() <<
"expected lower bound to be smaller or equal to the " 96 <<
"upper bound" <<
eom;
100 rhs.copy_to_operands(arguments[0], arguments[1]);
113 const irep_idt &identifier =
function.get_identifier();
116 if(arguments.size()!=2)
119 error() <<
"`" << identifier <<
"' expected to have two arguments" 127 error() <<
"`" << identifier <<
"' expected to have LHS" <<
eom;
137 error() <<
"`" << identifier <<
"' expected bool" <<
eom;
141 if(arguments[0].type().
id()!=ID_unsignedbv ||
142 arguments[0].
id()!=ID_constant)
145 error() <<
"`" << identifier <<
"' expected first operand to be " 146 <<
"a constant literal of type unsigned long" <<
eom;
156 error() <<
"error converting operands" <<
eom;
163 error() <<
"probability has to be smaller than 1" <<
eom;
170 error() <<
"denominator may not be zero" <<
eom;
174 rationalt numerator(num), denominator(den);
175 rationalt prob = numerator / denominator;
190 const irep_idt &f_id =
function.get_identifier();
196 static_cast<const typet &
>(
function.type().find(ID_return_type));
210 printf_code.
id(ID_code);
225 const irep_idt &f_id =
function.get_identifier();
229 if(arguments.empty())
232 error() <<
"scanf takes at least one argument" <<
eom;
244 std::size_t argument_number=1;
246 for(
const auto &t : token_list)
252 if(argument_number<arguments.size())
258 if(type.
id()==ID_array)
267 type,
"scanf_string", dest,
function.source_location());
275 codet array_copy_statement;
277 array_copy_statement.
operands().resize(2);
278 array_copy_statement.
op0()=ptr;
279 \ array_copy_statement.
op1()=rhs;
281 function.source_location();
289 assign.add_source_location()=
function.source_location();
310 function_call.
lhs()=lhs;
324 const exprt &
function,
333 if(arguments.size()<2)
336 error() <<
"input takes at least two arguments" <<
eom;
345 const exprt &
function,
354 if(arguments.size()<2)
357 error() <<
"output takes at least two arguments" <<
eom;
373 error() <<
"atomic_begin does not expect an LHS" <<
eom;
377 if(!arguments.empty())
380 error() <<
"atomic_begin takes no arguments" <<
eom;
385 t->source_location=
function.source_location();
397 error() <<
"atomic_end does not expect an LHS" <<
eom;
401 if(!arguments.empty())
404 error() <<
"atomic_end takes no arguments" <<
eom;
409 t->source_location=
function.source_location();
420 error() <<
"do_cpp_new without lhs is yet to be implemented" <<
eom;
426 static_cast<const exprt &
>(rhs.
find(ID_sizeof));
428 bool new_array=rhs.
get(ID_statement)==ID_cpp_new_array;
434 count=
static_cast<const exprt &
>(rhs.
find(ID_size));
443 exprt tmp_symbol_expr;
450 ns.
lookup(new_array?
"__new_array":
"__new").symbol_expr();
455 const typet &return_type=
464 tmp_symbol_expr=tmp_symbol.symbol_expr();
472 new_call.
lhs()=tmp_symbol_expr;
475 convert(new_call, dest, ID_cpp);
482 new_array?
"__placement_new_array":
"__placement_new").symbol_expr();
495 tmp_symbol_expr=tmp_symbol.symbol_expr();
504 new_call.
lhs()=tmp_symbol_expr;
507 for(std::size_t i=0; i<code_type.
parameters().size(); i++)
511 convert(new_call, dest, ID_cpp);
516 error() <<
"cpp_new expected to have 0 or 1 operands" <<
eom;
539 static_cast<const exprt &
>(rhs.
find(ID_initializer));
562 if(src.
id()==ID_typecast)
568 if(src.
id()!=ID_address_of)
571 error() <<
"expected array-pointer as argument" <<
eom;
577 if(src.
op0().
id()!=ID_index)
580 error() <<
"expected array-element as argument" <<
eom;
589 error() <<
"expected array as argument" <<
eom;
603 if(arguments.size()!=2)
606 error() <<
id <<
" expects two arguments" <<
eom;
610 codet array_op_statement;
612 array_op_statement.
operands()=arguments;
617 if(
id == ID_array_equal)
625 if(expr.
id()==ID_index)
627 else if(expr.
id()==ID_member)
629 else if(expr.
id()==ID_dereference)
631 else if(expr.
id()==ID_symbol)
640 if(expr.
id()==ID_typecast)
644 if(expr.
id()==ID_address_of &&
659 if(
function.get_bool(
"#invalid_object"))
663 const irep_idt &identifier=
function.get_identifier();
669 error() <<
"error: function `" << identifier <<
"' not found" 674 if(symbol->
type.
id()!=ID_code)
677 error() <<
"error: function `" << identifier
678 <<
"' type mismatch: expected code" <<
eom;
683 identifier==
"__VERIFIER_assume")
685 if(arguments.size()!=1)
688 error() <<
"`" << identifier <<
"' expected to have one argument" 694 t->guard=arguments.front();
695 t->source_location=
function.source_location();
696 t->source_location.set(
"user-provided",
true);
699 if(t->guard.type().id()!=ID_bool)
705 error() << identifier <<
" expected not to have LHS" <<
eom;
709 else if(identifier==
"__VERIFIER_error")
711 if(!arguments.empty())
714 error() <<
"`" << identifier <<
"' expected to have no arguments" 721 t->source_location=
function.source_location();
722 t->source_location.set(
"user-provided",
true);
723 t->source_location.set_property_class(ID_assertion);
728 error() << identifier <<
" expected not to have LHS" <<
eom;
736 a->source_location=
function.source_location();
737 a->source_location.set(
"user-provided",
true);
739 else if(identifier==
"assert" &&
740 !
ns.
lookup(identifier).location.get_function().empty())
742 if(arguments.size()!=1)
745 error() <<
"`" << identifier <<
"' expected to have one argument" 751 t->guard=arguments.front();
752 t->source_location=
function.source_location();
753 t->source_location.set(
"user-provided",
true);
754 t->source_location.set_property_class(ID_assertion);
755 t->source_location.set_comment(
759 if(t->guard.type().id()!=ID_bool)
765 error() << identifier <<
" expected not to have LHS" <<
eom;
772 if(arguments.size()!=2)
775 error() <<
"`" << identifier <<
"' expected to have two arguments" 780 bool is_precondition=
787 t->guard=arguments[0];
788 t->source_location=
function.source_location();
792 t->source_location.set_property_class(ID_precondition);
796 t->source_location.set(
798 !
function.source_location().is_built_in());
799 t->source_location.set_property_class(ID_assertion);
802 t->source_location.set_comment(description);
805 if(t->guard.type().id()!=ID_bool)
811 error() << identifier <<
" expected not to have LHS" <<
eom;
817 if(arguments.size()!=1)
820 error() <<
"`" << identifier <<
"' expected to have one argument" 828 error() << identifier <<
" expected not to have LHS" <<
eom;
833 t->source_location=
function.source_location();
834 t->code=
codet(ID_havoc_object);
835 t->code.add_source_location()=
function.source_location();
836 t->code.copy_to_operands(arguments[0]);
840 do_printf(lhs,
function, arguments, dest);
844 do_scanf(lhs,
function, arguments, dest);
847 identifier==
"__CPROVER::input")
849 do_input(lhs,
function, arguments, dest);
852 identifier==
"__CPROVER::output")
854 do_output(lhs,
function, arguments, dest);
857 identifier==
"__CPROVER::atomic_begin" ||
858 identifier==
"__VERIFIER_atomic_begin")
863 identifier==
"__CPROVER::atomic_end" ||
864 identifier==
"__VERIFIER_atomic_end")
887 if(lhs.
type().
id()==ID_c_bool)
891 rhs.
set(ID_C_identifier, identifier);
898 rhs.
set(ID_C_identifier, identifier);
923 do_array_op(ID_array_equal, lhs,
function, arguments, dest);
927 do_array_op(ID_array_set, lhs,
function, arguments, dest);
931 do_array_op(ID_array_copy, lhs,
function, arguments, dest);
935 do_array_op(ID_array_replace, lhs,
function, arguments, dest);
937 else if(identifier==
"printf")
944 do_printf(lhs,
function, arguments, dest);
946 else if(identifier==
"__assert_fail" ||
947 identifier==
"_assert" ||
948 identifier==
"__assert_c99" ||
949 identifier==
"_wassert")
970 if(arguments.size()!=4 &&
974 error() <<
"`" << identifier <<
"' expected to have four arguments" 984 t->source_location=
function.source_location();
985 t->source_location.set(
"user-provided",
true);
986 t->source_location.set_property_class(ID_assertion);
987 t->source_location.set_comment(description);
990 else if(identifier==
"__assert_rtn" ||
991 identifier==
"__assert")
1002 if(arguments.size()==4)
1007 else if(arguments.size()==3)
1015 error() <<
"`" << identifier <<
"' expected to have four arguments" 1022 t->source_location=
function.source_location();
1023 t->source_location.set(
"user-provided",
true);
1024 t->source_location.set_property_class(ID_assertion);
1025 t->source_location.set_comment(description);
1028 else if(identifier==
"__assert_func")
1033 if(arguments.size()!=4)
1036 error() <<
"`" << identifier <<
"' expected to have four arguments" 1051 description=
"assertion";
1056 t->source_location=
function.source_location();
1057 t->source_location.set(
"user-provided",
true);
1058 t->source_location.set_property_class(ID_assertion);
1059 t->source_location.set_comment(description);
1064 if(arguments.empty())
1067 error() <<
"`" << identifier
1068 <<
"' expected to have at least one argument" <<
eom;
1073 t->source_location=
function.source_location();
1074 t->code.set(ID_statement, ID_fence);
1079 t->code.set(kind,
true);
1082 else if(identifier==
"__builtin_prefetch")
1086 else if(identifier==
"__builtin_unreachable")
1090 else if(identifier==ID_gcc_builtin_va_arg)
1098 if(arguments.size()!=1)
1101 error() <<
"`" << identifier <<
"' expected to have one argument" 1111 rhs.set(ID_C_va_arg_type,
to_code_type(
function.type()).return_type());
1113 t1->source_location=
function.source_location();
1122 rhs.add_source_location()=
function.source_location();
1124 t2->source_location=
function.source_location();
1128 else if(identifier==
"__builtin_va_copy")
1130 if(arguments.size()!=2)
1133 error() <<
"`" << identifier <<
"' expected to have two arguments" 1144 error() <<
"va_copy argument expected to be lvalue" <<
eom;
1149 t->source_location=
function.source_location();
1152 else if(identifier==
"__builtin_va_start")
1156 if(arguments.size()!=2)
1159 error() <<
"`" << identifier <<
"' expected to have two arguments" 1171 error() <<
"va_start argument expected to be lvalue" <<
eom;
1176 t->source_location=
function.source_location();
1179 else if(identifier==
"__builtin_va_end")
1182 if(arguments.size()!=1)
1185 error() <<
"`" << identifier <<
"' expected to have one argument" 1195 error() <<
"va_end argument expected to be lvalue" <<
eom;
1203 t->source_location=
function.source_location();
1213 else if(identifier==
"__sync_fetch_and_add" ||
1214 identifier==
"__sync_fetch_and_sub" ||
1215 identifier==
"__sync_fetch_and_or" ||
1216 identifier==
"__sync_fetch_and_and" ||
1217 identifier==
"__sync_fetch_and_xor" ||
1218 identifier==
"__sync_fetch_and_nand")
1223 if(arguments.size()<2)
1226 error() <<
"`" << identifier
1227 <<
"' expected to have at least two arguments" <<
eom;
1231 if(arguments[0].type().
id()!=ID_pointer)
1234 error() <<
"`" << identifier <<
"' expected to have pointer argument" 1243 t1->source_location=
function.source_location();
1249 t2->source_location=
function.source_location();
1251 if(t2->code.op0().type()!=t2->code.op1().type())
1252 t2->code.op1().make_typecast(t2->code.op0().type());
1256 identifier==
"__sync_fetch_and_add"?ID_plus:
1257 identifier==
"__sync_fetch_and_sub"?ID_minus:
1258 identifier==
"__sync_fetch_and_or"?ID_bitor:
1259 identifier==
"__sync_fetch_and_and"?ID_bitand:
1260 identifier==
"__sync_fetch_and_xor"?ID_bitxor:
1261 identifier==
"__sync_fetch_and_nand"?ID_bitnand:
1266 if(op_expr.op1().type()!=op_expr.type())
1270 t3->source_location=
function.source_location();
1275 t4->source_location=
function.source_location();
1276 t4->code=
codet(ID_fence);
1277 t4->code.set(ID_WRfence,
true);
1280 t5->source_location=
function.source_location();
1282 else if(identifier==
"__sync_add_and_fetch" ||
1283 identifier==
"__sync_sub_and_fetch" ||
1284 identifier==
"__sync_or_and_fetch" ||
1285 identifier==
"__sync_and_and_fetch" ||
1286 identifier==
"__sync_xor_and_fetch" ||
1287 identifier==
"__sync_nand_and_fetch")
1292 if(arguments.size()<2)
1295 error() <<
"`" << identifier
1296 <<
"' expected to have at least two arguments" <<
eom;
1300 if(arguments[0].type().
id()!=ID_pointer)
1303 error() <<
"`" << identifier
1304 <<
"' expected to have pointer argument" <<
eom;
1312 t1->source_location=
function.source_location();
1315 identifier==
"__sync_add_and_fetch"?ID_plus:
1316 identifier==
"__sync_sub_and_fetch"?ID_minus:
1317 identifier==
"__sync_or_and_fetch"?ID_bitor:
1318 identifier==
"__sync_and_and_fetch"?ID_bitand:
1319 identifier==
"__sync_xor_and_fetch"?ID_bitxor:
1320 identifier==
"__sync_nand_and_fetch"?ID_bitnand:
1325 if(op_expr.op1().type()!=op_expr.type())
1329 t3->source_location=
function.source_location();
1336 t2->source_location=
function.source_location();
1338 if(t2->code.op0().type()!=t2->code.op1().type())
1339 t2->code.op1().make_typecast(t2->code.op0().type());
1344 t4->source_location=
function.source_location();
1345 t4->code=
codet(ID_fence);
1346 t4->code.set(ID_WRfence,
true);
1349 t5->source_location=
function.source_location();
1351 else if(identifier==
"__sync_bool_compare_and_swap")
1365 if(arguments.size()<3)
1368 error() <<
"`" << identifier
1369 <<
"' expected to have at least three arguments" <<
eom;
1373 if(arguments[0].type().
id()!=ID_pointer)
1376 error() <<
"`" << identifier
1377 <<
"' expected to have pointer argument" <<
eom;
1385 t1->source_location=
function.source_location();
1396 t2->source_location=
function.source_location();
1398 if(t2->code.op0().type()!=t2->code.op1().type())
1399 t2->code.op1().make_typecast(t2->code.op0().type());
1403 if_exprt if_expr(equal, arguments[2], deref_ptr, deref_ptr.
type());
1404 if(if_expr.op1().type()!=if_expr.type())
1408 t3->source_location=
function.source_location();
1413 t4->source_location=
function.source_location();
1414 t4->code=
codet(ID_fence);
1415 t4->code.set(ID_WRfence,
true);
1418 t5->source_location=
function.source_location();
1420 else if(identifier==
"__sync_val_compare_and_swap")
1424 if(arguments.size()<3)
1427 error() <<
"`" << identifier
1428 <<
"' expected to have at least three arguments" <<
eom;
1432 if(arguments[0].type().
id()!=ID_pointer)
1435 error() <<
"`" << identifier
1436 <<
"' expected to have pointer argument" <<
eom;
1444 t1->source_location=
function.source_location();
1450 t2->source_location=
function.source_location();
1452 if(t2->code.op0().type()!=t2->code.op1().type())
1453 t2->code.op1().make_typecast(t2->code.op0().type());
1462 if_exprt if_expr(equal, arguments[2], deref_ptr, deref_ptr.
type());
1463 if(if_expr.op1().type()!=if_expr.type())
1467 t3->source_location=
function.source_location();
1472 t4->source_location=
function.source_location();
1473 t4->code=
codet(ID_fence);
1474 t4->code.set(ID_WRfence,
true);
1477 t5->source_location=
function.source_location();
1479 else if(identifier==
"__sync_lock_test_and_set")
1492 else if(identifier==
"__sync_lock_release")
1502 else if(identifier==
"__builtin_isgreater" ||
1503 identifier==
"__builtin_isgreater" ||
1504 identifier==
"__builtin_isgreaterequal" ||
1505 identifier==
"__builtin_isless" ||
1506 identifier==
"__builtin_islessequal" ||
1507 identifier==
"__builtin_islessgreater" ||
1508 identifier==
"__builtin_isunordered")
1512 if(arguments.size()!=2 ||
1519 error() <<
"`" << identifier
1520 <<
"' expected to have two float/double arguments" 1527 bool use_double=arguments[0].type()==
double_type();
1528 if(arguments[0].type()!=arguments[1].type())
1531 new_arguments[1].make_typecast(arguments[0].type());
1534 new_arguments[0].make_typecast(arguments[1].type());
1541 const typet &a_t=new_arguments[0].type();
1548 name+=use_double?
'd':
'f';
1552 new_function.
type()=f_type;
1555 function_call.
lhs()=lhs;
1556 function_call.
function()=new_function;
1557 function_call.
arguments()=new_arguments;
1564 new_symbol.
name=name;
1565 new_symbol.
type=f_type;
1566 new_symbol.
location=
function.source_location();
1578 function_call.
lhs()=lhs;
The type of an expression.
irep_idt get_string_constant(const exprt &expr)
irep_idt name
The unique identifier.
const std::string & id2string(const irep_idt &d)
pointer_typet pointer_type(const typet &subtype)
application of (mathematical) function
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
void do_input(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
bool is_lvalue(const exprt &expr)
void do_printf(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
void copy_to_operands(const exprt &expr)
#define forall_expr(it, expr)
void do_atomic_begin(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::vector< parametert > parameterst
void do_atomic_end(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
void destructive_append(goto_programt &p)
Appends the given program, which is destroyed.
virtual void do_function_call_symbol(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
add function calls to function queue for later processing
The trinary if-then-else operator.
bitvector_typet double_type()
unsignedbv_typet size_type()
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
static mstreamt & eom(mstreamt &m)
Expression Initialization.
void do_array_op(const irep_idt &id, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
exprt make_va_list(const exprt &expr)
exprt object_size(const exprt &pointer)
const irep_idt & id() const
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
void clean_expr(exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true)
virtual void do_cpp_new(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
A generic base class for binary expressions.
bitvector_typet float_type()
instructionst::iterator targett
const source_locationt & find_source_location() const
source_locationt source_location
Operator to dereference a pointer.
const irep_idt & get(const irep_namet &name) const
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
A side effect that returns a non-deterministically chosen value.
bool has_prefix(const std::string &s, const std::string &prefix)
const exprt & size() const
const typet & follow(const typet &) const
void do_prob_uniform(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
bitvector_typet index_type()
Operator to return the address of an object.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
exprt get_array_argument(const exprt &src)
The boolean constant false.
symbol_exprt & function()
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
std::vector< exprt > operandst
const source_locationt & source_location() const
A generic container class for the GOTO intermediate representation of one function.
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
message_handlert & get_message_handler()
void do_output(const exprt &lhs, 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 set_statement(const irep_idt &statement)
targett add_instruction()
Adds an instruction at the end.
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Base class for all expressions.
const parameterst & parameters() const
irep_idt base_name
Base (non-scoped) name.
void do_prob_coin(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
const source_locationt & source_location() const
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
symbol_table_baset & symbol_table
void set_identifier(const irep_idt &identifier)
source_locationt & add_source_location()
const codet & to_code(const exprt &expr)
Expression to hold a symbol (variable)
void do_scanf(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Extract class identifier.
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
A statement in a programming language.
const typet & subtype() const
An expression containing a side effect.
void make_typecast(const typet &_type)
static void replace_new_object(const exprt &object, exprt &dest)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
const irept & find(const irep_namet &name) const
const typet & return_type() const
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
void set(const irep_namet &name, const irep_idt &value)
const irep_idt & get_statement() const