Go to the documentation of this file.
37 const irep_idt &identifier =
function.get_identifier();
40 if(arguments.size()!=2)
43 error() <<
"'" << identifier <<
"' 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;
78 error() <<
"'" << identifier
79 <<
"' expected operands to be constant literals" <<
eom;
90 error() <<
"error converting operands" <<
eom;
97 error() <<
"expected lower bound to be smaller or equal to the "
98 <<
"upper bound" <<
eom;
102 rhs.copy_to_operands(arguments[0], arguments[1]);
115 const irep_idt &identifier =
function.get_identifier();
118 if(arguments.size()!=2)
121 error() <<
"'" << identifier <<
"' expected to have two arguments" <<
eom;
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;
151 arguments[1].type().
id() != ID_unsignedbv ||
152 arguments[1].
id() != ID_constant)
155 error() <<
"'" << identifier <<
"' expected second operand to be "
156 <<
"a constant literal of type unsigned long" <<
eom;
167 error() <<
"error converting operands" <<
eom;
174 error() <<
"probability has to be smaller than 1" <<
eom;
181 error() <<
"denominator may not be zero" <<
eom;
185 rationalt numerator(num), denominator(den);
186 rationalt prob = numerator / denominator;
201 const irep_idt &f_id =
function.get_identifier();
205 codet printf_code(ID_printf, arguments,
function.source_location());
215 const irep_idt &f_id =
function.get_identifier();
219 if(arguments.empty())
222 error() <<
"scanf takes at least one argument" <<
eom;
234 std::size_t argument_number=1;
236 for(
const auto &t : token_list)
242 if(argument_number<arguments.size())
248 if(type->id() == ID_array)
257 *type,
"scanf_string", dest,
function.source_location());
265 codet array_copy_statement;
267 array_copy_statement.
operands().resize(2);
268 array_copy_statement.
op0()=ptr;
269 \ array_copy_statement.
op1()=rhs;
271 function.source_location();
278 type->subtype(),
function.source_location());
289 *type,
function.source_location());
312 const exprt &
function,
316 if(arguments.size()<2)
319 error() <<
"input takes at least two arguments" <<
eom;
327 const exprt &
function,
331 if(arguments.size()<2)
334 error() <<
"output takes at least two arguments" <<
eom;
350 error() <<
"atomic_begin does not expect an LHS" <<
eom;
354 if(!arguments.empty())
357 error() <<
"atomic_begin takes no arguments" <<
eom;
373 error() <<
"atomic_end does not expect an LHS" <<
eom;
377 if(!arguments.empty())
380 error() <<
"atomic_end takes no arguments" <<
eom;
395 error() <<
"do_cpp_new without lhs is yet to be implemented" <<
eom;
401 static_cast<const exprt &
>(rhs.
find(ID_sizeof));
403 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();
428 const typet &return_type=
444 new_call.
lhs()=tmp_symbol_expr;
447 convert(new_call, dest, ID_cpp);
454 new_array?
"__placement_new_array":
"__placement_new").symbol_expr();
475 new_call.
lhs()=tmp_symbol_expr;
478 for(std::size_t i=0; i<code_type.
parameters().size(); i++)
484 convert(new_call, dest, ID_cpp);
489 error() <<
"cpp_new expected to have 0 or 1 operands" <<
eom;
512 static_cast<const exprt &
>(rhs.
find(ID_initializer));
535 if(src.
id()==ID_typecast)
538 if(src.
id()!=ID_address_of)
541 error() <<
"expected array-pointer as argument" <<
eom;
547 if(address_of_expr.object().id() != ID_index)
550 error() <<
"expected array-element as argument" <<
eom;
554 const auto &index_expr =
to_index_expr(address_of_expr.object());
556 if(index_expr.array().type().id() != ID_array)
559 error() <<
"expected array as argument" <<
eom;
563 return index_expr.array();
573 if(arguments.size()!=2)
576 error() <<
id <<
" expects two arguments" <<
eom;
580 codet array_op_statement(
id);
581 array_op_statement.
operands()=arguments;
586 if(
id == ID_array_equal)
597 if(result.
id() == ID_address_of)
601 result = address_of_expr.object();
604 while(result.
type().
id() == ID_array &&
620 const auto enum_expr = arguments.front();
621 const auto enum_type =
622 type_try_dynamic_cast<c_enum_tag_typet>(enum_expr.type());
628 for(
const auto &enum_value : enum_values)
631 disjuncts.push_back(
equal_exprt(enum_expr, std::move(val)));
646 if(
function.get_bool(ID_C_invalid_object))
650 const irep_idt &identifier=
function.get_identifier();
656 error() <<
"error: function '" << identifier <<
"' not found" <<
eom;
660 if(symbol->
type.
id()!=ID_code)
663 error() <<
"error: function '" << identifier
664 <<
"' type mismatch: expected code" <<
eom;
685 identifier==
"__VERIFIER_assume")
687 if(arguments.size()!=1)
690 error() <<
"'" << identifier <<
"' expected to have one argument" <<
eom;
697 function.source_location()));
699 t->source_location.set(
"user-provided",
true);
704 error() << identifier <<
" expected not to have LHS" <<
eom;
708 else if(identifier==
"__VERIFIER_error")
710 if(!arguments.empty())
713 error() <<
"'" << identifier <<
"' expected to have no arguments" <<
eom;
720 t->source_location.set(
"user-provided",
true);
721 t->source_location.set_property_class(ID_assertion);
726 error() << identifier <<
" expected not to have LHS" <<
eom;
734 a->source_location.set(
"user-provided",
true);
737 identifier ==
"assert" &&
740 if(arguments.size()!=1)
743 error() <<
"'" << identifier <<
"' expected to have one argument" <<
eom;
750 function.source_location()));
751 t->source_location.set(
"user-provided",
true);
752 t->source_location.set_property_class(ID_assertion);
753 t->source_location.set_comment(
754 "assertion " +
from_expr(
ns, identifier, arguments.front()));
759 error() << identifier <<
" expected not to have LHS" <<
eom;
772 if(arguments.size()!=2)
775 error() <<
"'" << identifier <<
"' expected to have two arguments" <<
eom;
779 bool is_precondition=
781 bool is_postcondition = identifier ==
CPROVER_PREFIX "postcondition";
789 function.source_location()));
793 t->source_location.set_property_class(ID_precondition);
795 else if(is_postcondition)
797 t->source_location.set_property_class(ID_postcondition);
801 t->source_location.set(
803 !
function.source_location().is_built_in());
804 t->source_location.set_property_class(ID_assertion);
807 t->source_location.set_comment(description);
812 error() << identifier <<
" expected not to have LHS" <<
eom;
818 if(arguments.size()!=1)
821 error() <<
"'" << identifier <<
"' expected to have one argument" <<
eom;
828 error() << identifier <<
" expected not to have LHS" <<
eom;
832 codet havoc(ID_havoc_object);
840 do_printf(lhs,
function, arguments, dest);
844 do_scanf(lhs,
function, arguments, dest);
847 identifier==
"__CPROVER::input")
852 error() << identifier <<
" expected not to have LHS" <<
eom;
856 do_input(
function, arguments, dest);
859 identifier==
"__CPROVER::output")
864 error() << identifier <<
" expected not to have LHS" <<
eom;
871 identifier==
"__CPROVER::atomic_begin" ||
872 identifier==
"java::org.cprover.CProver.atomicBegin:()V" ||
873 identifier==
"__VERIFIER_atomic_begin")
878 identifier==
"__CPROVER::atomic_end" ||
879 identifier==
"java::org.cprover.CProver.atomicEnd:()V" ||
880 identifier==
"__VERIFIER_atomic_end")
903 if(lhs.
type().
id()==ID_c_bool)
906 rhs.
set(ID_C_identifier, identifier);
912 rhs.
set(ID_C_identifier, identifier);
925 if(
function.type().get_bool(ID_C_incomplete))
928 error() <<
"'" << identifier <<
"' is not declared, "
929 <<
"missing type information required to construct call to "
930 <<
"uninterpreted function" <<
eom;
936 for(
const auto ¶meter : function_call_type.
parameters())
937 domain.push_back(parameter.type());
944 assignment.add_source_location()=
function.source_location();
949 do_array_op(ID_array_equal, lhs,
function, arguments, dest);
953 do_array_op(ID_array_set, lhs,
function, arguments, dest);
957 do_array_op(ID_array_copy, lhs,
function, arguments, dest);
961 do_array_op(ID_array_replace, lhs,
function, arguments, dest);
963 else if(identifier==
"__assert_fail" ||
964 identifier==
"_assert" ||
965 identifier==
"__assert_c99" ||
966 identifier==
"_wassert")
987 if(arguments.size()!=4 &&
991 error() <<
"'" << identifier <<
"' expected to have four arguments"
1002 t->source_location.set(
"user-provided",
true);
1003 t->source_location.set_property_class(ID_assertion);
1004 t->source_location.set_comment(description);
1007 else if(identifier==
"__assert_rtn" ||
1008 identifier==
"__assert")
1019 if(arguments.size()==4)
1024 else if(arguments.size()==3)
1032 error() <<
"'" << identifier <<
"' expected to have four arguments"
1040 t->source_location.set(
"user-provided",
true);
1041 t->source_location.set_property_class(ID_assertion);
1042 t->source_location.set_comment(description);
1045 else if(identifier==
"__assert_func")
1050 if(arguments.size()!=4)
1053 error() <<
"'" << identifier <<
"' expected to have four arguments"
1068 description=
"assertion";
1074 t->source_location.set(
"user-provided",
true);
1075 t->source_location.set_property_class(ID_assertion);
1076 t->source_location.set_comment(description);
1081 if(arguments.empty())
1084 error() <<
"'" << identifier <<
"' expected to have at least one argument"
1089 codet fence(ID_fence);
1091 for(
const auto &argument : arguments)
1096 else if(identifier==
"__builtin_prefetch")
1100 else if(identifier==
"__builtin_unreachable")
1104 else if(identifier==ID_gcc_builtin_va_arg)
1112 if(arguments.size()!=1)
1115 error() <<
"'" << identifier <<
"' expected to have one argument" <<
eom;
1123 exprt list_arg_cast = list_arg;
1125 list_arg.
type().
id() == ID_pointer &&
1143 ID_C_va_arg_type,
to_code_type(
function.type()).return_type());
1145 std::move(assign),
function.source_location()));
1147 else if(identifier==
"__builtin_va_copy")
1149 if(arguments.size()!=2)
1152 error() <<
"'" << identifier <<
"' expected to have two arguments" <<
eom;
1162 error() <<
"va_copy argument expected to be lvalue" <<
eom;
1167 dest_expr, src_expr,
function.source_location()));
1169 else if(identifier ==
"__builtin_va_start" || identifier ==
"__va_start")
1173 if(arguments.size()!=2)
1176 error() <<
"'" << identifier <<
"' expected to have two arguments" <<
eom;
1185 error() <<
"va_start argument expected to be lvalue" <<
eom;
1190 dest_expr.
type().
id() == ID_pointer &&
1199 rhs.add_to_operands(
1203 std::move(dest_expr), std::move(rhs),
function.source_location()));
1205 else if(identifier==
"__builtin_va_end")
1208 if(arguments.size()!=1)
1211 error() <<
"'" << identifier <<
"' expected to have one argument" <<
eom;
1220 error() <<
"va_end argument expected to be lvalue" <<
eom;
1225 if(dest_expr.
type().
id() == ID_pointer)
1231 dest_expr, *zero,
function.source_location()));
1235 identifier ==
"__builtin_isgreater" ||
1236 identifier ==
"__builtin_isgreaterequal" ||
1237 identifier ==
"__builtin_isless" || identifier ==
"__builtin_islessequal" ||
1238 identifier ==
"__builtin_islessgreater" ||
1239 identifier ==
"__builtin_isunordered")
1243 if(arguments.size()!=2 ||
1250 error() <<
"'" << identifier
1251 <<
"' expected to have two float/double arguments" <<
eom;
1257 bool use_double=arguments[0].type()==
double_type();
1258 if(arguments[0].type()!=arguments[1].type())
1275 const typet &a_t=new_arguments[0].type();
1282 name+=use_double?
'd':
'f';
1286 new_function.
type()=f_type;
1295 new_symbol.
name=name;
1296 new_symbol.
type=f_type;
1297 new_symbol.
location=
function.source_location();
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
#define UNREACHABLE
This should be used to mark dead code.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
static exprt conditional_cast(const exprt &expr, const typet &type)
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
virtual void do_cpp_new(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
const typet & subtype() const
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
void do_output(const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
static void replace_new_object(const exprt &object, exprt &dest)
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
#define CHECK_RETURN(CONDITION)
The type of an expression, extends irept.
std::vector< parametert > parameterst
void clean_expr(exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
exprt get_array_argument(const exprt &src)
void cpp_new_initializer(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
builds a goto program for object initialization after new
typet type
Type of symbol.
Operator to dereference a pointer.
void do_atomic_end(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
std::vector< c_enum_membert > memberst
const irept & find(const irep_namet &name) const
targett add(instructiont &&instruction)
Adds a given instruction at the end.
The plus expression Associativity is not specified.
Base class for all expressions.
const exprt & op1() const =delete
irep_idt base_name
Base (non-scoped) name.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Expression to hold a symbol (variable)
bitvector_typet index_type()
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)
const codet & to_code(const exprt &expr)
const exprt & size() const
A codet representing the declaration that an output of a particular description has a value which cor...
void do_enum_is_in_range(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
Converts calls to the built in enum_is_in_range function to a test that the given enum value is in th...
typet & type()
Return the type of the expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
bool get_bool(const irep_namet &name) const
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Expression Initialization.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
signedbv_typet signed_int_type()
bool has_prefix(const std::string &s, const std::string &prefix)
void do_scanf(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
const std::string & id2string(const irep_idt &d)
source_locationt source_location
irep_idt get_string_constant(const exprt &expr)
#define PRECONDITION(CONDITION)
const source_locationt & source_location() const
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
const irep_idt & get_identifier() const
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
floatbv_typet float_type()
API to expression classes for Pointers.
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
Application of (mathematical) function.
std::vector< typet > domaint
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
pointer_typet pointer_type(const typet &subtype)
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
exprt object_size(const exprt &pointer)
const irep_idt & id() const
std::vector< exprt > operandst
The Boolean constant false.
const parameterst & parameters() const
source_locationt & add_source_location()
floatbv_typet double_type()
const irep_idt & get_statement() const
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
A side_effect_exprt that returns a non-deterministically chosen value.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Deprecated expression utility functions.
exprt value
Initial value of symbol.
void do_input(const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void do_printf(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
void do_atomic_begin(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
const irep_idt & get(const irep_namet &name) const
source_locationt location
Source code location of definition of symbol.
void set(const irep_namet &name, const irep_idt &value)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
A generic container class for the GOTO intermediate representation of one function.
void do_array_op(const irep_idt &id, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
symbol_table_baset & symbol_table
bool is_one() const
Return whether the expression is a constant representing 1.
const typet & return_type() const
void set_statement(const irep_idt &statement)
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Operator to return the address of an object.
source_locationt & add_source_location()
Semantic type conversion.
signedbv_typet pointer_diff_type()
unsignedbv_typet size_type()
A codet representing an assignment in the program.
A constant literal expression.
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
const irep_idt & get_value() const
const source_locationt & source_location() const
exprt make_va_list(const exprt &expr)
A type for mathematical functions (do not confuse with functions/methods in code)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
void set_identifier(const irep_idt &identifier)
irep_idt name
The unique identifier.
instructionst::iterator targett
An expression containing a side effect.
void do_prob_uniform(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
const memberst & members() const
void do_prob_coin(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
bool is_lvalue(const exprt &expr)
Returns true iff the argument is (syntactically) an lvalue.
API to expression classes for 'mathematical' expressions.
Data structure for representing an arbitrary statement in a program.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.