36 const irep_idt &identifier =
function.get_identifier();
39 if(arguments.size()!=2)
42 error() <<
"`" << identifier
43 <<
"' expected to have two arguments" <<
eom;
50 error() <<
"`" << identifier <<
"' expected to have LHS" <<
eom;
57 if(lhs.
type().
id()!=ID_unsignedbv &&
58 lhs.
type().
id()!=ID_signedbv)
61 error() <<
"`" << identifier <<
"' expected other type" <<
eom;
65 if(arguments[0].type().
id()!=lhs.
type().
id() ||
66 arguments[1].type().id()!=lhs.
type().
id())
69 error() <<
"`" << identifier
70 <<
"' expected operands to be of same type as LHS" <<
eom;
74 if(!arguments[0].is_constant() ||
75 !arguments[1].is_constant())
78 error() <<
"`" << identifier
79 <<
"' expected operands to be constant literals" <<
eom;
89 error() <<
"error converting operands" <<
eom;
96 error() <<
"expected lower bound to be smaller or equal to the " 97 <<
"upper bound" <<
eom;
101 rhs.copy_to_operands(arguments[0], arguments[1]);
114 const irep_idt &identifier =
function.get_identifier();
117 if(arguments.size()!=2)
120 error() <<
"`" << identifier <<
"' expected to have two arguments" 128 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();
197 ID_printf, return_type,
function.source_location());
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();
290 assign.add_source_location()=
function.source_location();
299 type,
function.source_location());
322 const exprt &
function,
326 codet input_code(ID_input);
330 if(arguments.size()<2)
333 error() <<
"input takes at least two arguments" <<
eom;
341 const exprt &
function,
345 codet output_code(ID_output);
349 if(arguments.size()<2)
352 error() <<
"output takes at least two arguments" <<
eom;
368 error() <<
"atomic_begin does not expect an LHS" <<
eom;
372 if(!arguments.empty())
375 error() <<
"atomic_begin takes no arguments" <<
eom;
380 t->source_location=
function.source_location();
392 error() <<
"atomic_end does not expect an LHS" <<
eom;
396 if(!arguments.empty())
399 error() <<
"atomic_end takes no arguments" <<
eom;
404 t->source_location=
function.source_location();
415 error() <<
"do_cpp_new without lhs is yet to be implemented" <<
eom;
421 static_cast<const exprt &>(rhs.
find(ID_sizeof));
423 bool new_array=rhs.
get(ID_statement)==ID_cpp_new_array;
429 count=static_cast<const exprt &>(rhs.
find(ID_size));
438 exprt tmp_symbol_expr;
445 ns.
lookup(new_array?
"__new_array":
"__new").symbol_expr();
450 const typet &return_type=
459 tmp_symbol_expr=tmp_symbol.symbol_expr();
466 new_call.
lhs()=tmp_symbol_expr;
469 convert(new_call, dest, ID_cpp);
476 new_array?
"__placement_new_array":
"__placement_new").symbol_expr();
489 tmp_symbol_expr=tmp_symbol.symbol_expr();
497 new_call.
lhs()=tmp_symbol_expr;
500 for(std::size_t i=0; i<code_type.
parameters().size(); i++)
504 convert(new_call, dest, ID_cpp);
509 error() <<
"cpp_new expected to have 0 or 1 operands" <<
eom;
532 static_cast<const exprt &>(rhs.
find(ID_initializer));
555 if(src.
id()==ID_typecast)
561 if(src.
id()!=ID_address_of)
564 error() <<
"expected array-pointer as argument" <<
eom;
570 if(src.
op0().
id()!=ID_index)
573 error() <<
"expected array-element as argument" <<
eom;
582 error() <<
"expected array as argument" <<
eom;
596 if(arguments.size()!=2)
599 error() <<
id <<
" expects two arguments" <<
eom;
603 codet array_op_statement(
id);
604 array_op_statement.
operands()=arguments;
609 if(
id == ID_array_equal)
618 if(expr.
id()==ID_typecast)
622 if(expr.
id()==ID_address_of &&
637 if(
function.get_bool(ID_C_invalid_object))
641 const irep_idt &identifier=
function.get_identifier();
647 error() <<
"error: function `" << identifier <<
"' not found" 652 if(symbol->
type.
id()!=ID_code)
655 error() <<
"error: function `" << identifier
656 <<
"' type mismatch: expected code" <<
eom;
661 identifier==
"__VERIFIER_assume")
663 if(arguments.size()!=1)
666 error() <<
"`" << identifier <<
"' expected to have one argument" 672 t->guard=arguments.front();
673 t->source_location=
function.source_location();
674 t->source_location.set(
"user-provided",
true);
677 if(t->guard.type().id()!=ID_bool)
683 error() << identifier <<
" expected not to have LHS" <<
eom;
687 else if(identifier==
"__VERIFIER_error")
689 if(!arguments.empty())
692 error() <<
"`" << identifier <<
"' expected to have no arguments" 699 t->source_location=
function.source_location();
700 t->source_location.set(
"user-provided",
true);
701 t->source_location.set_property_class(ID_assertion);
706 error() << identifier <<
" expected not to have LHS" <<
eom;
714 a->source_location=
function.source_location();
715 a->source_location.set(
"user-provided",
true);
717 else if(identifier==
"assert" &&
718 !
ns.
lookup(identifier).location.get_function().empty())
720 if(arguments.size()!=1)
723 error() <<
"`" << identifier <<
"' expected to have one argument" 729 t->guard=arguments.front();
730 t->source_location=
function.source_location();
731 t->source_location.set(
"user-provided",
true);
732 t->source_location.set_property_class(ID_assertion);
733 t->source_location.set_comment(
737 if(t->guard.type().id()!=ID_bool)
743 error() << identifier <<
" expected not to have LHS" <<
eom;
750 if(arguments.size()!=2)
753 error() <<
"`" << identifier <<
"' expected to have two arguments" 758 bool is_precondition=
765 t->guard=arguments[0];
766 t->source_location=
function.source_location();
770 t->source_location.set_property_class(ID_precondition);
774 t->source_location.set(
776 !
function.source_location().is_built_in());
777 t->source_location.set_property_class(ID_assertion);
780 t->source_location.set_comment(description);
783 if(t->guard.type().id()!=ID_bool)
789 error() << identifier <<
" expected not to have LHS" <<
eom;
795 if(arguments.size()!=1)
798 error() <<
"`" << identifier <<
"' expected to have one argument" 806 error() << identifier <<
" expected not to have LHS" <<
eom;
811 t->source_location=
function.source_location();
812 t->code=
codet(ID_havoc_object);
813 t->code.add_source_location()=
function.source_location();
814 t->code.copy_to_operands(arguments[0]);
818 do_printf(lhs,
function, arguments, dest);
822 do_scanf(lhs,
function, arguments, dest);
825 identifier==
"__CPROVER::input")
830 error() << identifier <<
" expected not to have LHS" <<
eom;
834 do_input(
function, arguments, dest);
837 identifier==
"__CPROVER::output")
842 error() << identifier <<
" expected not to have LHS" <<
eom;
849 identifier==
"__CPROVER::atomic_begin" ||
850 identifier==
"java::org.cprover.CProver.atomicBegin:()V" ||
851 identifier==
"__VERIFIER_atomic_begin")
856 identifier==
"__CPROVER::atomic_end" ||
857 identifier==
"java::org.cprover.CProver.atomicEnd:()V" ||
858 identifier==
"__VERIFIER_atomic_end")
881 if(lhs.
type().
id()==ID_c_bool)
884 rhs.
set(ID_C_identifier, identifier);
890 rhs.
set(ID_C_identifier, identifier);
906 assignment.add_source_location()=
function.source_location();
911 do_array_op(ID_array_equal, lhs,
function, arguments, dest);
915 do_array_op(ID_array_set, lhs,
function, arguments, dest);
919 do_array_op(ID_array_copy, lhs,
function, arguments, dest);
923 do_array_op(ID_array_replace, lhs,
function, arguments, dest);
925 else if(identifier==
"printf")
932 do_printf(lhs,
function, arguments, dest);
934 else if(identifier==
"__assert_fail" ||
935 identifier==
"_assert" ||
936 identifier==
"__assert_c99" ||
937 identifier==
"_wassert")
958 if(arguments.size()!=4 &&
962 error() <<
"`" << identifier <<
"' expected to have four arguments" 972 t->source_location=
function.source_location();
973 t->source_location.set(
"user-provided",
true);
974 t->source_location.set_property_class(ID_assertion);
975 t->source_location.set_comment(description);
978 else if(identifier==
"__assert_rtn" ||
979 identifier==
"__assert")
990 if(arguments.size()==4)
995 else if(arguments.size()==3)
1003 error() <<
"`" << identifier <<
"' expected to have four arguments" 1010 t->source_location=
function.source_location();
1011 t->source_location.set(
"user-provided",
true);
1012 t->source_location.set_property_class(ID_assertion);
1013 t->source_location.set_comment(description);
1016 else if(identifier==
"__assert_func")
1021 if(arguments.size()!=4)
1024 error() <<
"`" << identifier <<
"' expected to have four arguments" 1039 description=
"assertion";
1044 t->source_location=
function.source_location();
1045 t->source_location.set(
"user-provided",
true);
1046 t->source_location.set_property_class(ID_assertion);
1047 t->source_location.set_comment(description);
1052 if(arguments.empty())
1055 error() <<
"`" << identifier
1056 <<
"' expected to have at least one argument" <<
eom;
1061 t->source_location=
function.source_location();
1062 t->code.set(ID_statement, ID_fence);
1067 t->code.set(kind,
true);
1070 else if(identifier==
"__builtin_prefetch")
1074 else if(identifier==
"__builtin_unreachable")
1078 else if(identifier==ID_gcc_builtin_va_arg)
1086 if(arguments.size()!=1)
1089 error() <<
"`" << identifier <<
"' expected to have one argument" 1098 ID_gcc_builtin_va_arg_next,
1102 rhs.set(ID_C_va_arg_type,
to_code_type(
function.type()).return_type());
1104 t1->source_location=
function.source_location();
1113 rhs.add_source_location()=
function.source_location();
1115 t2->source_location=
function.source_location();
1119 else if(identifier==
"__builtin_va_copy")
1121 if(arguments.size()!=2)
1124 error() <<
"`" << identifier <<
"' expected to have two arguments" 1135 error() <<
"va_copy argument expected to be lvalue" <<
eom;
1140 t->source_location=
function.source_location();
1143 else if(identifier==
"__builtin_va_start")
1147 if(arguments.size()!=2)
1150 error() <<
"`" << identifier <<
"' expected to have two arguments" 1162 error() <<
"va_start argument expected to be lvalue" <<
eom;
1167 t->source_location=
function.source_location();
1170 else if(identifier==
"__builtin_va_end")
1173 if(arguments.size()!=1)
1176 error() <<
"`" << identifier <<
"' expected to have one argument" 1186 error() <<
"va_end argument expected to be lvalue" <<
eom;
1194 t->source_location=
function.source_location();
1201 else if(identifier==
"__sync_fetch_and_add" ||
1202 identifier==
"__sync_fetch_and_sub" ||
1203 identifier==
"__sync_fetch_and_or" ||
1204 identifier==
"__sync_fetch_and_and" ||
1205 identifier==
"__sync_fetch_and_xor" ||
1206 identifier==
"__sync_fetch_and_nand")
1211 if(arguments.size()<2)
1214 error() <<
"`" << identifier
1215 <<
"' expected to have at least two arguments" <<
eom;
1219 if(arguments[0].type().
id()!=ID_pointer)
1222 error() <<
"`" << identifier <<
"' expected to have pointer argument" 1231 t1->source_location=
function.source_location();
1237 t2->source_location=
function.source_location();
1239 if(t2->code.op0().type()!=t2->code.op1().type())
1240 t2->code.op1().make_typecast(t2->code.op0().type());
1244 identifier==
"__sync_fetch_and_add"?ID_plus:
1245 identifier==
"__sync_fetch_and_sub"?ID_minus:
1246 identifier==
"__sync_fetch_and_or"?ID_bitor:
1247 identifier==
"__sync_fetch_and_and"?ID_bitand:
1248 identifier==
"__sync_fetch_and_xor"?ID_bitxor:
1249 identifier==
"__sync_fetch_and_nand"?ID_bitnand:
1254 if(op_expr.op1().type()!=op_expr.type())
1258 t3->source_location=
function.source_location();
1263 t4->source_location=
function.source_location();
1264 t4->code=
codet(ID_fence);
1265 t4->code.set(ID_WRfence,
true);
1268 t5->source_location=
function.source_location();
1270 else if(identifier==
"__sync_add_and_fetch" ||
1271 identifier==
"__sync_sub_and_fetch" ||
1272 identifier==
"__sync_or_and_fetch" ||
1273 identifier==
"__sync_and_and_fetch" ||
1274 identifier==
"__sync_xor_and_fetch" ||
1275 identifier==
"__sync_nand_and_fetch")
1280 if(arguments.size()<2)
1283 error() <<
"`" << identifier
1284 <<
"' expected to have at least two arguments" <<
eom;
1288 if(arguments[0].type().
id()!=ID_pointer)
1291 error() <<
"`" << identifier
1292 <<
"' expected to have pointer argument" <<
eom;
1300 t1->source_location=
function.source_location();
1303 identifier==
"__sync_add_and_fetch"?ID_plus:
1304 identifier==
"__sync_sub_and_fetch"?ID_minus:
1305 identifier==
"__sync_or_and_fetch"?ID_bitor:
1306 identifier==
"__sync_and_and_fetch"?ID_bitand:
1307 identifier==
"__sync_xor_and_fetch"?ID_bitxor:
1308 identifier==
"__sync_nand_and_fetch"?ID_bitnand:
1313 if(op_expr.op1().type()!=op_expr.type())
1317 t3->source_location=
function.source_location();
1324 t2->source_location=
function.source_location();
1326 if(t2->code.op0().type()!=t2->code.op1().type())
1327 t2->code.op1().make_typecast(t2->code.op0().type());
1332 t4->source_location=
function.source_location();
1333 t4->code=
codet(ID_fence);
1334 t4->code.set(ID_WRfence,
true);
1337 t5->source_location=
function.source_location();
1339 else if(identifier==
"__sync_bool_compare_and_swap")
1353 if(arguments.size()<3)
1356 error() <<
"`" << identifier
1357 <<
"' expected to have at least three arguments" <<
eom;
1361 if(arguments[0].type().
id()!=ID_pointer)
1364 error() <<
"`" << identifier
1365 <<
"' expected to have pointer argument" <<
eom;
1373 t1->source_location=
function.source_location();
1384 t2->source_location=
function.source_location();
1386 if(t2->code.op0().type()!=t2->code.op1().type())
1387 t2->code.op1().make_typecast(t2->code.op0().type());
1391 if_exprt if_expr(equal, arguments[2], deref_ptr, deref_ptr.
type());
1392 if(if_expr.op1().type()!=if_expr.type())
1396 t3->source_location=
function.source_location();
1401 t4->source_location=
function.source_location();
1402 t4->code=
codet(ID_fence);
1403 t4->code.set(ID_WRfence,
true);
1406 t5->source_location=
function.source_location();
1408 else if(identifier==
"__sync_val_compare_and_swap")
1412 if(arguments.size()<3)
1415 error() <<
"`" << identifier
1416 <<
"' expected to have at least three arguments" <<
eom;
1420 if(arguments[0].type().
id()!=ID_pointer)
1423 error() <<
"`" << identifier
1424 <<
"' expected to have pointer argument" <<
eom;
1432 t1->source_location=
function.source_location();
1438 t2->source_location=
function.source_location();
1440 if(t2->code.op0().type()!=t2->code.op1().type())
1441 t2->code.op1().make_typecast(t2->code.op0().type());
1450 if_exprt if_expr(equal, arguments[2], deref_ptr, deref_ptr.
type());
1451 if(if_expr.op1().type()!=if_expr.type())
1455 t3->source_location=
function.source_location();
1460 t4->source_location=
function.source_location();
1461 t4->code=
codet(ID_fence);
1462 t4->code.set(ID_WRfence,
true);
1465 t5->source_location=
function.source_location();
1467 else if(identifier==
"__sync_lock_test_and_set")
1480 else if(identifier==
"__sync_lock_release")
1490 else if(identifier==
"__builtin_isgreater" ||
1491 identifier==
"__builtin_isgreater" ||
1492 identifier==
"__builtin_isgreaterequal" ||
1493 identifier==
"__builtin_isless" ||
1494 identifier==
"__builtin_islessequal" ||
1495 identifier==
"__builtin_islessgreater" ||
1496 identifier==
"__builtin_isunordered")
1500 if(arguments.size()!=2 ||
1507 error() <<
"`" << identifier
1508 <<
"' expected to have two float/double arguments" 1515 bool use_double=arguments[0].type()==
double_type();
1516 if(arguments[0].type()!=arguments[1].type())
1519 new_arguments[1].make_typecast(arguments[0].type());
1522 new_arguments[0].make_typecast(arguments[1].type());
1529 const typet &a_t=new_arguments[0].type();
1536 name+=use_double?
'd':
'f';
1540 new_function.
type()=f_type;
1549 new_symbol.
name=name;
1550 new_symbol.
type=f_type;
1551 new_symbol.
location=
function.source_location();
The type of an expression, extends irept.
irep_idt get_string_constant(const exprt &expr)
irep_idt name
The unique identifier.
Semantic type conversion.
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'
Deprecated expression utility functions.
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 typet to a code_typet.
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
#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 p to *this. p 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.
typet & type()
Return the type of the expression.
unsignedbv_typet size_type()
#define CHECK_RETURN(CONDITION)
bool is_lvalue(const exprt &expr)
Returns true iff the argument is (syntactically) an lvalue.
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
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
void do_input(const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
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 base class for binary expressions.
instructionst::iterator targett
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
const exprt & op1() const =delete
source_locationt source_location
Operator to dereference a pointer.
const irep_idt & get(const irep_namet &name) const
void do_output(const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
A side_effect_exprt that returns a non-deterministically chosen value.
bool has_prefix(const std::string &s, const std::string &prefix)
const exprt & size() const
codet representation of a function call statement.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
void do_prob_uniform(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
bitvector_typet index_type()
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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.
std::vector< exprt > operandst
const source_locationt & source_location() const
A generic container class for the GOTO intermediate representation of one function.
floatbv_typet float_type()
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
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 typet to an array_typet.
Base class for all expressions.
floatbv_typet double_type()
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
#define UNREACHABLE
This should be used to mark dead code.
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 an 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)
Data structure for representing an arbitrary statement in a program.
const typet & subtype() const
An expression containing a side effect.
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
static void replace_new_object(const exprt &object, exprt &dest)
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 documentation for namespace_baset::lookup().
A codet representing an assignment in the program.
void set(const irep_namet &name, const irep_idt &value)
const irep_idt & get_statement() const