本文整理汇总了C++中exprt::operandst类的典型用法代码示例。如果您正苦于以下问题:C++ operandst类的具体用法?C++ operandst怎么用?C++ operandst使用的例子?那么恭喜您, 这里精选的类代码示例或许可以为您提供帮助。
在下文中一共展示了operandst类的17个代码示例,这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞,您的评价将有助于我们的系统推荐出更棒的C++代码示例。
示例1: collect_postconditions
void summarizer_bwt::collect_postconditions(
const function_namet &function_name,
const local_SSAt &SSA,
const summaryt &summary,
exprt::operandst &postconditions,
bool sufficient)
{
for(local_SSAt::nodest::const_iterator n_it = SSA.nodes.begin();
n_it != SSA.nodes.end(); n_it++)
{
for(local_SSAt::nodet::assertionst::const_iterator
a_it = n_it->assertions.begin();
a_it != n_it->assertions.end(); a_it++)
{
postconditions.push_back(*a_it);
}
}
/* if(termination)
{
if(!summary.termination_argument.is_nil())
postconditions.push_back(summary.termination_argument);
}*/
exprt guard = SSA.guard_symbol(--SSA.goto_function.body.instructions.end());
if(!sufficient)
postconditions.push_back(and_exprt(guard,summary.bw_postcondition));
else
postconditions.push_back(implies_exprt(guard,summary.bw_postcondition));
}
开发者ID:AnnaTrost,项目名称:2ls,代码行数:29,代码来源:summarizer_bw.cpp
示例2: assert
exprt functionst::arguments_equal(const exprt::operandst &o1,
const exprt::operandst &o2)
{
assert(o1.size()==o2.size());
if(o1.empty())
return true_exprt();
and_exprt and_expr;
and_exprt::operandst &conjuncts=and_expr.operands();
conjuncts.resize(o1.size());
for(std::size_t i=0; i<o1.size(); i++)
{
exprt lhs=o1[i];
exprt rhs=o2[i];
if(lhs.type()!=rhs.type())
rhs.make_typecast(lhs.type());
conjuncts[i]=equal_exprt(lhs, rhs);
}
return and_expr;
}
开发者ID:dcattaruzza,项目名称:cbmc,代码行数:25,代码来源:functions.cpp
示例3: conjunction
exprt conjunction(const exprt::operandst &op)
{
if(op.empty())
return true_exprt();
else if(op.size()==1)
return op.front();
else
{
and_exprt result;
result.operands()=op;
return result;
}
}
开发者ID:dcattaruzza,项目名称:cbmc,代码行数:13,代码来源:std_expr.cpp
示例4: disjunction
exprt disjunction(const exprt::operandst &op)
{
if(op.empty())
return false_exprt();
else if(op.size()==1)
return op.front();
else
{
or_exprt result;
result.operands()=op;
return result;
}
}
开发者ID:dcattaruzza,项目名称:cbmc,代码行数:13,代码来源:std_expr.cpp
示例5: make_not_post_constraints
void equality_domaint::make_not_post_constraints(
valuet &_value,
exprt::operandst &cond_exprs)
{
assert(*e_it<templ.size());
cond_exprs.resize(1);
if(check_dis)
{
cond_exprs[0]=get_post_not_disequ_constraint(*e_it);
return;
}
const template_rowt &templ_row=templ[*e_it];
if(templ_row.kind==IN)
{
cond_exprs[0]=true_exprt();
return;
}
const var_pairt &vv=templ_row.var_pair;
exprt c=
and_exprt(
templ_row.aux_expr,
not_exprt(
implies_exprt(
templ_row.post_guard,
equal_exprt(vv.first, vv.second))));
rename(c);
cond_exprs[0]=c;
}
开发者ID:diffblue,项目名称:2ls,代码行数:29,代码来源:equality_domain.cpp
示例6: assert
void predabs_domaint::make_not_post_constraints(
const templ_valuet &value,
exprt::operandst &cond_exprs)
{
assert(value.size()==templ.size());
cond_exprs.resize(templ.size());
exprt::operandst c;
for(std::size_t row=0; row<templ.size(); row++)
{
cond_exprs[row]=and_exprt(
templ[row].aux_expr,
not_exprt(get_row_post_constraint(row, value)));
}
}
开发者ID:viktormalik,项目名称:2ls,代码行数:15,代码来源:predabs_domain.cpp
示例7: do_array_copy
void goto_convertt::do_array_copy(
const exprt &lhs,
const exprt &function,
const exprt::operandst &arguments,
goto_programt &dest)
{
if(arguments.size()!=2)
{
err_location(function);
throw "array_copy expects two arguments";
}
codet array_set_statement;
array_set_statement.set_statement(ID_array_copy);
array_set_statement.operands()=arguments;
copy(array_set_statement, OTHER, dest);
}
开发者ID:romainbrenguier,项目名称:cbmc,代码行数:18,代码来源:builtin_functions.cpp
示例8: do_output
void goto_convertt::do_output(
const exprt &lhs,
const exprt &function,
const exprt::operandst &arguments,
goto_programt &dest)
{
codet output_code;
output_code.set_statement(ID_output);
output_code.operands()=arguments;
output_code.add_source_location()=function.source_location();
if(arguments.size()<2)
{
err_location(function);
throw "output takes at least two arguments";
}
copy(output_code, OTHER, dest);
}
开发者ID:romainbrenguier,项目名称:cbmc,代码行数:19,代码来源:builtin_functions.cpp
示例9: do_atomic_end
void goto_convertt::do_atomic_end(
const exprt &lhs,
const exprt &function,
const exprt::operandst &arguments,
goto_programt &dest)
{
if(lhs.is_not_nil())
{
err_location(lhs);
throw "atomic_end does not expect an LHS";
}
if(!arguments.empty())
{
err_location(function);
throw "atomic_end takes no arguments";
}
goto_programt::targett t=dest.add_instruction(ATOMIC_END);
t->source_location=function.source_location();
}
开发者ID:romainbrenguier,项目名称:cbmc,代码行数:21,代码来源:builtin_functions.cpp
示例10: do_array_equal
void goto_convertt::do_array_equal(
const exprt &lhs,
const exprt &function,
const exprt::operandst &arguments,
goto_programt &dest)
{
if(arguments.size()!=2)
{
err_location(function);
throw "array_equal expects two arguments";
}
const typet &arg0_type=ns.follow(arguments[0].type());
const typet &arg1_type=ns.follow(arguments[1].type());
if(arg0_type.id()!=ID_pointer ||
arg1_type.id()!=ID_pointer)
{
err_location(function);
throw "array_equal expects pointer arguments";
}
if(lhs.is_not_nil())
{
code_assignt assignment;
// add dereferencing here
dereference_exprt lhs_array, rhs_array;
lhs_array.op0()=arguments[0];
rhs_array.op0()=arguments[1];
lhs_array.type()=arg0_type.subtype();
rhs_array.type()=arg1_type.subtype();
assignment.lhs()=lhs;
assignment.rhs()=binary_exprt(
lhs_array, ID_array_equal, rhs_array, lhs.type());
convert(assignment, dest);
}
}
开发者ID:romainbrenguier,项目名称:cbmc,代码行数:40,代码来源:builtin_functions.cpp
示例11: do_prob_uniform
void goto_convertt::do_prob_uniform(
const exprt &lhs,
const exprt &function,
const exprt::operandst &arguments,
goto_programt &dest)
{
const irep_idt &identifier=function.get(ID_identifier);
// make it a side effect if there is an LHS
if(arguments.size()!=2)
{
err_location(function);
throw "`"+id2string(identifier)+"' expected to have two arguments";
}
if(lhs.is_nil())
{
err_location(function);
throw "`"+id2string(identifier)+"' expected to have LHS";
}
exprt rhs=side_effect_exprt("prob_uniform", lhs.type());
rhs.add_source_location()=function.source_location();
if(lhs.type().id()!=ID_unsignedbv &&
lhs.type().id()!=ID_signedbv)
{
err_location(function);
throw "`"+id2string(identifier)+"' expected other type";
}
if(arguments[0].type().id()!=lhs.type().id() ||
arguments[1].type().id()!=lhs.type().id())
{
err_location(function);
throw "`"+id2string(identifier)+"' expected operands to be of same type as LHS";
}
if(!arguments[0].is_constant() ||
!arguments[1].is_constant())
{
err_location(function);
throw "`"+id2string(identifier)+"' expected operands to be constant literals";
}
mp_integer lb, ub;
if(to_integer(arguments[0], lb) ||
to_integer(arguments[1], ub))
{
err_location(function);
throw "error converting operands";
}
if(lb > ub)
{
err_location(function);
throw "expected lower bound to be smaller or equal to the upper bound";
}
rhs.copy_to_operands(arguments[0], arguments[1]);
code_assignt assignment(lhs, rhs);
assignment.add_source_location()=function.source_location();
copy(assignment, ASSIGN, dest);
}
开发者ID:romainbrenguier,项目名称:cbmc,代码行数:66,代码来源:builtin_functions.cpp
示例12: do_prob_coin
void goto_convertt::do_prob_coin(
const exprt &lhs,
const exprt &function,
const exprt::operandst &arguments,
goto_programt &dest)
{
const irep_idt &identifier=function.get(ID_identifier);
// make it a side effect if there is an LHS
if(arguments.size()!=2)
{
err_location(function);
throw "`"+id2string(identifier)+"' expected to have two arguments";
}
if(lhs.is_nil())
{
err_location(function);
throw "`"+id2string(identifier)+"' expected to have LHS";
}
exprt rhs=side_effect_exprt("prob_coin", lhs.type());
rhs.add_source_location()=function.source_location();
if(lhs.type()!=bool_typet())
{
err_location(function);
throw "`"+id2string(identifier)+"' expected bool";
}
if(arguments[0].type().id()!=ID_unsignedbv ||
arguments[0].id()!=ID_constant)
{
err_location(function);
throw "`"+id2string(identifier)+"' expected first "
"operand to be a constant literal of type unsigned long";
}
mp_integer num, den;
if(to_integer(arguments[0], num) ||
to_integer(arguments[1], den))
{
err_location(function);
throw "error converting operands";
}
if(num-den > mp_integer(0))
{
err_location(function);
throw "probability has to be smaller than 1";
}
if(den == mp_integer(0))
{
err_location(function);
throw "denominator may not be zero";
}
rationalt numerator(num), denominator(den);
rationalt prob = numerator / denominator;
rhs.copy_to_operands(from_rational(prob));
code_assignt assignment(lhs, rhs);
assignment.add_source_location()=function.source_location();
copy(assignment, ASSIGN, dest);
}
开发者ID:romainbrenguier,项目名称:cbmc,代码行数:68,代码来源:builtin_functions.cpp
示例13: do_function_call_symbol
void goto_convertt::do_function_call_symbol(
const exprt &lhs,
const symbol_exprt &function,
const exprt::operandst &arguments,
goto_programt &dest)
{
if(function.get_bool("#invalid_object"))
return; // ignore
// lookup symbol
const irep_idt &identifier=function.get_identifier();
const symbolt *symbol;
if(ns.lookup(identifier, symbol))
{
err_location(function);
throw "error: function `"+id2string(identifier)+"' not found";
}
if(symbol->type.id()!=ID_code)
{
err_location(function);
throw "error: function `"+id2string(identifier)+"' type mismatch: expected code";
}
if(identifier==CPROVER_PREFIX "assume" ||
identifier=="__VERIFIER_assume")
{
if(arguments.size()!=1)
{
err_location(function);
throw "`"+id2string(identifier)+"' expected to have one argument";
}
goto_programt::targett t=dest.add_instruction(ASSUME);
t->guard=arguments.front();
t->source_location=function.source_location();
t->source_location.set("user-provided", true);
// let's double-check the type of the argument
if(t->guard.type().id()!=ID_bool)
t->guard.make_typecast(bool_typet());
if(lhs.is_not_nil())
{
err_location(function);
throw id2string(identifier)+" expected not to have LHS";
}
}
else if(identifier=="__VERIFIER_error")
{
if(!arguments.empty())
{
err_location(function);
throw "`"+id2string(identifier)+"' expected to have no arguments";
}
goto_programt::targett t=dest.add_instruction(ASSERT);
t->guard=false_exprt();
t->source_location=function.source_location();
t->source_location.set("user-provided", true);
t->source_location.set_property_class(ID_assertion);
if(lhs.is_not_nil())
{
err_location(function);
throw id2string(identifier)+" expected not to have LHS";
}
}
else if(has_prefix(id2string(identifier), "java::java.lang.AssertionError.<init>:"))
{
// insert function call anyway
code_function_callt function_call;
function_call.lhs()=lhs;
function_call.function()=function;
function_call.arguments()=arguments;
function_call.add_source_location()=function.source_location();
copy(function_call, FUNCTION_CALL, dest);
if(arguments.size()!=1 && arguments.size()!=2)
{
err_location(function);
throw "`"+id2string(identifier)+"' expected to have one or two arguments";
}
goto_programt::targett t=dest.add_instruction(ASSERT);
t->guard=false_exprt();
t->source_location=function.source_location();
t->source_location.set("user-provided", true);
t->source_location.set_property_class(ID_assertion);
t->source_location.set_comment("assertion at "+function.source_location().as_string());
}
else if(identifier=="assert" &&
!ns.lookup(identifier).location.get_function().empty())
{
if(arguments.size()!=1)
{
err_location(function);
throw "`"+id2string(identifier)+"' expected to have one argument";
//.........这里部分代码省略.........
开发者ID:romainbrenguier,项目名称:cbmc,代码行数:101,代码来源:builtin_functions.cpp
示例14: parameter_assignments
void goto_inlinet::parameter_assignments(
const locationt &location,
const code_typet &code_type,
const exprt::operandst &arguments,
goto_programt &dest)
{
// iterates over the operands
exprt::operandst::const_iterator it1=arguments.begin();
goto_programt::local_variablest local_variables;
const code_typet::argumentst &argument_types=
code_type.arguments();
// iterates over the types of the arguments
for(code_typet::argumentst::const_iterator
it2=argument_types.begin();
it2!=argument_types.end();
it2++)
{
// if you run out of actual arguments there was a mismatch
if(it1==arguments.end())
{
err_location(location);
throw "function call: not enough arguments";
}
const exprt &argument=static_cast<const exprt &>(*it2);
// this is the type the n-th argument should be
const typet &arg_type=ns.follow(argument.type());
const irep_idt &identifier=argument.cmt_identifier();
if(identifier=="")
{
err_location(location);
throw "no identifier for function argument";
}
{
const symbolt &symbol=ns.lookup(identifier);
goto_programt::targett decl=dest.add_instruction();
decl->make_other();
exprt tmp = code_declt(symbol_expr(symbol));
migrate_expr(tmp, decl->code);
decl->location=location;
decl->function=location.get_function();
decl->local_variables=local_variables;
}
local_variables.insert(identifier);
// nil means "don't assign"
if(it1->is_nil())
{
}
else
{
// this is the actual parameter
exprt actual(*it1);
// it should be the same exact type
type2tc arg_type_2, actual_type_2;
migrate_type(arg_type, arg_type_2);
migrate_type(actual.type(), actual_type_2);
if (!base_type_eq(arg_type_2, actual_type_2, ns))
{
const typet &f_argtype = ns.follow(arg_type);
const typet &f_acttype = ns.follow(actual.type());
// we are willing to do some conversion
if((f_argtype.id()=="pointer" &&
f_acttype.id()=="pointer") ||
(f_argtype.is_array() &&
f_acttype.id()=="pointer" &&
f_argtype.subtype()==f_acttype.subtype()))
{
actual.make_typecast(arg_type);
}
else if((f_argtype.id()=="signedbv" ||
f_argtype.id()=="unsignedbv" ||
f_argtype.is_bool()) &&
(f_acttype.id()=="signedbv" ||
f_acttype.id()=="unsignedbv" ||
f_acttype.is_bool()))
{
actual.make_typecast(arg_type);
}
else
{
err_location(location);
str << "function call: argument `" << identifier
<< "' type mismatch: got "
<< from_type(ns, identifier, it1->type())
<< ", expected "
<< from_type(ns, identifier, arg_type);
throw 0;
//.........这里部分代码省略.........
开发者ID:huangshiyou,项目名称:esbmc,代码行数:101,代码来源:goto_inline.cpp
示例15: do_scanf
void goto_convertt::do_scanf(
const exprt &lhs,
const exprt &function,
const exprt::operandst &arguments,
goto_programt &dest)
{
const irep_idt &f_id=function.get(ID_identifier);
if(f_id==CPROVER_PREFIX "scanf")
{
if(arguments.size()<1)
{
err_location(function);
error() << "scanf takes at least one argument" << eom;
throw 0;
}
irep_idt format_string;
if(!get_string_constant(arguments[0], format_string))
{
// use our model
format_token_listt token_list=parse_format_string(id2string(format_string));
std::size_t argument_number=1;
for(const auto & t : token_list)
{
typet type=get_type(t);
if(type.is_not_nil())
{
if(argument_number<arguments.size())
{
exprt ptr=
typecast_exprt(arguments[argument_number], pointer_type(type));
argument_number++;
// make it nondet for now
exprt lhs=dereference_exprt(ptr, type);
exprt rhs=side_effect_expr_nondett(type);
code_assignt assign(lhs, rhs);
assign.add_source_location()=function.source_location();
copy(assign, ASSIGN, dest);
}
}
}
}
else
{
// we'll just do nothing
code_function_callt function_call;
function_call.lhs()=lhs;
function_call.function()=function;
function_call.arguments()=arguments;
function_call.add_source_location()=function.source_location();
copy(function_call, FUNCTION_CALL, dest);
}
}
else
assert(false);
}
开发者ID:romainbrenguier,项目名称:cbmc,代码行数:63,代码来源:builtin_functions.cpp
示例16: convert_update_rec
void boolbvt::convert_update_rec(
const exprt::operandst &designators,
std::size_t d,
const typet &type,
std::size_t offset,
const exprt &new_value,
bvt &bv)
{
if(type.id()==ID_symbol)
convert_update_rec(
designators, d, ns.follow(type), offset, new_value, bv);
if(d>=designators.size())
{
// done
bvt new_value_bv=convert_bv(new_value);
std::size_t new_value_width=boolbv_width(type);
if(new_value_width!=new_value_bv.size())
throw "convert_update_rec: unexpected new_value size";
// update
for(std::size_t i=0; i<new_value_width; i++)
{
assert(offset+i<bv.size());
bv[offset+i]=new_value_bv[i];
}
return;
}
const exprt &designator=designators[d];
if(designator.id()==ID_index_designator)
{
if(type.id()!=ID_array)
throw "update: index designator needs array";
if(designator.operands().size()!=1)
throw "update: index designator takes one operand";
bvt index_bv=convert_bv(designator.op0());
const array_typet &array_type=to_array_type(type);
const typet &subtype=ns.follow(array_type.subtype());
std::size_t element_size=boolbv_width(subtype);
// iterate over array
mp_integer size;
if(to_integer(array_type.size(), size))
throw "update: failed to get array size";
bvt tmp_bv=bv;
for(std::size_t i=0; i!=integer2long(size); ++i)
{
std::size_t new_offset=offset+i*element_size;
convert_update_rec(
designators, d+1, subtype, new_offset, new_value, tmp_bv);
bvt const_bv=bv_utils.build_constant(i, index_bv.size());
literalt equal=bv_utils.equal(const_bv, index_bv);
for(std::size_t j=0; j<element_size; j++)
{
std::size_t idx=new_offset+j;
assert(idx<bv.size());
bv[idx]=prop.lselect(equal, tmp_bv[idx], bv[idx]);
}
}
}
else if(designator.id()==ID_member_designator)
{
const irep_idt &component_name=designator.get(ID_component_name);
if(type.id()==ID_struct)
{
const struct_typet &struct_type=
to_struct_type(type);
std::size_t struct_offset=0;
struct_typet::componentt component;
component.make_nil();
const struct_typet::componentst &components=
struct_type.components();
for(struct_typet::componentst::const_iterator
it=components.begin();
it!=components.end();
it++)
{
const typet &subtype=it->type();
std::size_t sub_width=boolbv_width(subtype);
if(it->get_name()==component_name)
//.........这里部分代码省略.........
开发者ID:Dthird,项目名称:CBMC,代码行数:101,代码来源:boolbv_update.cpp
示例17: typecheck_expr
codet cpp_typecheckt::cpp_constructor(
const source_locationt &source_location,
const exprt &object,
const exprt::operandst &operands)
{
exprt object_tc=object;
typecheck_expr(object_tc);
elaborate_class_template(object_tc.type());
typet tmp_type(object_tc.type());
follow_symbol(tmp_type);
assert(!is_reference(tmp_type));
if(tmp_type.id()==ID_array)
{
// We allow only one operand and it must be tagged with '#array_ini'.
// Note that the operand is an array that is used for copy-initialization.
// In the general case, a program is not allow to use this form of
// construct. This way of initializing an array is used internaly only.
// The purpose of the tag #arra_ini is to rule out ill-formed
// programs.
if(!operands.empty() && !operands.front().get_bool("#array_ini"))
{
error().source_location=source_location;
error() << "bad array initializer" << eom;
throw 0;
}
assert(operands.empty() || operands.size()==1);
if(operands.empty() && cpp_is_pod(tmp_type))
{
codet nil;
nil.make_nil();
return nil;
}
const exprt &size_expr=
to_array_type(tmp_type).size();
if(size_expr.id()=="infinity")
{
// don't initialize
codet nil;
nil.make_nil();
return nil;
}
exprt tmp_size=size_expr;
make_constant_index(tmp_size);
mp_integer s;
if(to_integer(tmp_size, s))
{
error().source_location=source_location;
error() << "array size `" << to_string(size_expr)
<< "' is not a constant" << eom;
throw 0;
}
/*if(cpp_is_pod(tmp_type))
{
code_expressiont new_code;
exprt op_tc=operands.front();
typecheck_expr(op_tc);
// Override constantness
object_tc.type().set("#constant", false);
object_tc.set("#lvalue", true);
side_effect_exprt assign("assign");
assign.add_source_location()=source_location;
assign.copy_to_operands(object_tc, op_tc);
typecheck_side_effect_assignment(assign);
new_code.expression()=assign;
return new_code;
}
else*/
{
codet new_code(ID_block);
// for each element of the array, call the default constructor
for(mp_integer i=0; i < s; ++i)
{
exprt::operandst tmp_operands;
exprt constant=from_integer(i, index_type());
constant.add_source_location()=source_location;
exprt index(ID_index);
index.copy_to_operands(object);
index.copy_to_operands(constant);
index.add_source_location()=source_location;
if(!operands.empty())
{
exprt operand(ID_index);
operand.copy_to_operands(operands.front());
//.........这里部分代码省略.........
开发者ID:dcattaruzza,项目名称:cbmc,代码行数:101,代码来源:cpp_constructor.cpp
注:本文中的exprt::operandst类示例由纯净天空整理自Github/MSDocs等源码及文档管理平台,相关代码片段筛选自各路编程大神贡献的开源项目,源码版权归原作者所有,传播和使用请参考对应项目的License;未经允许,请勿转载。 |
请发表评论