本文整理汇总了C++中exprt类的典型用法代码示例。如果您正苦于以下问题:C++ exprt类的具体用法?C++ exprt怎么用?C++ exprt使用的例子?那么恭喜您, 这里精选的类代码示例或许可以为您提供帮助。
在下文中一共展示了exprt类的20个代码示例,这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞,您的评价将有助于我们的系统推荐出更棒的C++代码示例。
示例1: new_object
void cpp_typecheckt::new_temporary(
const source_locationt &source_location,
const typet &type,
const exprt::operandst &ops,
exprt &temporary)
{
// create temporary object
exprt tmp_object_expr=exprt(ID_side_effect, type);
tmp_object_expr.set(ID_statement, ID_temporary_object);
tmp_object_expr.add_source_location()= source_location;
exprt new_object(ID_new_object);
new_object.add_source_location()=tmp_object_expr.source_location();
new_object.set(ID_C_lvalue, true);
new_object.type()=tmp_object_expr.type();
already_typechecked(new_object);
codet new_code =
cpp_constructor(source_location, new_object, ops);
if(new_code.is_not_nil())
{
if(new_code.get(ID_statement)==ID_assign)
tmp_object_expr.move_to_operands(new_code.op1());
else
tmp_object_expr.add(ID_initializer)=new_code;
}
temporary.swap(tmp_object_expr);
}
开发者ID:dcattaruzza,项目名称:cbmc,代码行数:31,代码来源:cpp_constructor.cpp
示例2: add
void guardt::add(const exprt &expr)
{
if(expr.id()==ID_and && expr.type().id()==ID_bool)
{
forall_operands(it, expr)
add(*it);
return;
}
if(expr.is_true())
{
}
else
guard_list.push_back(expr);
}
开发者ID:ashokkelur,项目名称:CBMC-With-DSP-C,代码行数:16,代码来源:guard.cpp
示例3: simplify_isinf
bool simplify_exprt::simplify_isinf(exprt &expr)
{
if(expr.operands().size()!=1) return true;
if(ns.follow(expr.op0().type()).id()!=ID_floatbv)
return true;
if(expr.op0().is_constant())
{
ieee_floatt value(to_constant_expr(expr.op0()));
expr.make_bool(value.is_infinity());
return false;
}
return true;
}
开发者ID:Dthird,项目名称:CBMC,代码行数:16,代码来源:simplify_expr_floatbv.cpp
示例4: base_type
void base_type(exprt &expr, const namespacet &ns)
{
base_type(expr.type(), ns);
Forall_operands(it, expr)
base_type(*it, ns);
}
开发者ID:lihaol,项目名称:cbmc,代码行数:7,代码来源:base_type.cpp
示例5: convert_index
void boolbvt::convert_index(
const exprt &array,
const mp_integer &index,
bvt &bv)
{
const array_typet &array_type=
to_array_type(ns.follow(array.type()));
unsigned width=boolbv_width(array_type.subtype());
if(width==0)
return conversion_failed(array, bv);
bv.resize(width);
const bvt &tmp=convert_bv(array); // recursive call
mp_integer offset=index*width;
if(offset>=0 &&
offset+width<=mp_integer(tmp.size()))
{
// in bounds
for(unsigned i=0; i<width; i++)
bv[i]=tmp[integer2long(offset+i)];
}
else
{
// out of bounds
for(unsigned i=0; i<width; i++)
bv[i]=prop.new_variable();
}
}
开发者ID:ashokkelur,项目名称:CBMC-With-DSP-C,代码行数:33,代码来源:boolbv_index.cpp
示例6: assert
bool clang_c_convertert::convert_integer_literal(
const clang::IntegerLiteral &integer_literal,
exprt &dest)
{
typet type;
if(get_type(integer_literal.getType(), type))
return true;
assert(type.is_unsignedbv() || type.is_signedbv());
llvm::APInt val = integer_literal.getValue();
exprt the_val;
if (type.is_unsignedbv())
{
the_val =
constant_exprt(
integer2binary(val.getZExtValue(), bv_width(type)),
integer2string(val.getZExtValue()),
type);
}
else
{
the_val =
constant_exprt(
integer2binary(val.getSExtValue(), bv_width(type)),
integer2string(val.getSExtValue()),
type);
}
dest.swap(the_val);
return false;
}
开发者ID:ericksonalves,项目名称:esbmc,代码行数:33,代码来源:clang_c_convert_literals.cpp
示例7: convert_with_bv
void boolbvt::convert_with_bv(
const typet &type,
const exprt &op1,
const exprt &op2,
const bvt &prev_bv,
bvt &next_bv)
{
literalt l=convert(op2);
mp_integer op1_value;
if(!to_integer(op1, op1_value))
{
next_bv=prev_bv;
if(op1_value<next_bv.size())
next_bv[integer2size_t(op1_value)]=l;
return;
}
typet counter_type=op1.type();
for(std::size_t i=0; i<prev_bv.size(); i++)
{
exprt counter=from_integer(i, counter_type);
literalt eq_lit=convert(equal_exprt(op1, counter));
next_bv[i]=prop.lselect(eq_lit, l, prev_bv[i]);
}
}
开发者ID:lihaol,项目名称:cbmc,代码行数:31,代码来源:boolbv_with.cpp
示例8: has_failed_symbol
bool symex_dereference_statet::has_failed_symbol(
const exprt &expr,
const symbolt *&symbol)
{
renaming_nst renaming_ns(goto_symex.ns, state);
if(expr.id()==ID_symbol)
{
const symbolt &ptr_symbol=
renaming_ns.lookup(to_symbol_expr(expr).get_identifier());
const irep_idt &failed_symbol=
ptr_symbol.type.get("#failed_symbol");
if(failed_symbol!="" &&
!renaming_ns.lookup(failed_symbol, symbol))
{
symbolt sym=*symbol;
symbolt *sym_ptr=0;
sym.name=state.rename(sym.name, renaming_ns, goto_symex_statet::L1);
goto_symex.new_symbol_table.move(sym, sym_ptr);
symbol=sym_ptr;
return true;
}
}
return false;
}
开发者ID:,项目名称:,代码行数:28,代码来源:
示例9: gather_rvalues
void cone_of_influencet::gather_rvalues(const exprt &expr, expr_sett &rvals)
{
if(expr.id() == ID_symbol ||
expr.id() == ID_index ||
expr.id() == ID_member ||
expr.id() == ID_dereference)
{
rvals.insert(expr);
}
else
{
forall_operands(it, expr)
{
gather_rvalues(*it, rvals);
}
}
开发者ID:,项目名称:,代码行数:16,代码来源:
示例10: dereference_rec
exprt dereferencet::dereference_typecast(
const typecast_exprt &expr,
const exprt &offset,
const typet &type)
{
const exprt &op=expr.op();
const typet &op_type=ns.follow(op.type());
// pointer type cast?
if(op_type.id()==ID_pointer)
return dereference_rec(op, offset, type); // just pass down
else if(op_type.id()==ID_signedbv || op_type.id()==ID_unsignedbv)
{
// We got an integer-typed address A. We turn this back (!)
// into *(type *)(A+offset), and then let some other layer
// worry about it.
exprt integer=
plus_exprt(offset, typecast_exprt(op, offset.type()));
exprt new_typecast=
typecast_exprt(integer, pointer_typet(type));
return dereference_exprt(new_typecast, type);
}
else
throw "dereferencet: unexpected cast";
}
开发者ID:rbavishi,项目名称:iCBMC,代码行数:28,代码来源:dereference.cpp
示例11: convert_with_union
void boolbvt::convert_with_union(
const union_typet &type,
const exprt &op1,
const exprt &op2,
const bvt &prev_bv,
bvt &next_bv)
{
next_bv=prev_bv;
const bvt &op2_bv=convert_bv(op2);
if(next_bv.size()<op2_bv.size())
{
error().source_location=type.source_location();
error() << "convert_with_union: unexpected operand op2 width" << eom;
throw 0;
}
if(config.ansi_c.endianness==configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN)
{
for(std::size_t i=0; i<op2_bv.size(); i++)
next_bv[i]=op2_bv[i];
}
else
{
assert(config.ansi_c.endianness==configt::ansi_ct::endiannesst::IS_BIG_ENDIAN);
endianness_mapt map_u(type, false, ns);
endianness_mapt map_op2(op2.type(), false, ns);
for(std::size_t i=0; i<op2_bv.size(); i++)
next_bv[map_u.map_bit(i)]=op2_bv[map_op2.map_bit(i)];
}
}
开发者ID:diffblue,项目名称:cbmc,代码行数:34,代码来源:boolbv_with.cpp
示例12: convert_mult
bvt bv_refinementt::convert_mult(const exprt &expr)
{
if(!do_arithmetic_refinement || expr.type().id()==ID_fixedbv)
return SUB::convert_mult(expr);
// we catch any multiplication
// unless it involves a constant
const exprt::operandst &operands=expr.operands();
const typet &type=ns.follow(expr.type());
assert(operands.size()>=2);
if(operands.size()>2)
return convert_mult(make_binary(expr)); // make binary
// we keep multiplication by a constant for integers
if(type.id()!=ID_floatbv)
if(operands[0].is_constant() || operands[1].is_constant())
return SUB::convert_mult(expr);
bvt bv;
approximationt &a=add_approximation(expr, bv);
// initially, we have a partial interpretation for integers
if(type.id()==ID_signedbv ||
type.id()==ID_unsignedbv)
{
// x*0==0 and 0*x==0
literalt op0_zero=bv_utils.is_zero(a.op0_bv);
literalt op1_zero=bv_utils.is_zero(a.op1_bv);
literalt res_zero=bv_utils.is_zero(a.result_bv);
prop.l_set_to_true(
prop.limplies(prop.lor(op0_zero, op1_zero), res_zero));
// x*1==x and 1*x==x
literalt op0_one=bv_utils.is_one(a.op0_bv);
literalt op1_one=bv_utils.is_one(a.op1_bv);
literalt res_op0=bv_utils.equal(a.op0_bv, a.result_bv);
literalt res_op1=bv_utils.equal(a.op1_bv, a.result_bv);
prop.l_set_to_true(prop.limplies(op0_one, res_op1));
prop.l_set_to_true(prop.limplies(op1_one, res_op0));
}
return bv;
}
开发者ID:diffblue,项目名称:cbmc,代码行数:47,代码来源:refine_arithmetic.cpp
示例13: from_expr
bool languaget::from_expr(
const exprt &expr,
std::string &code,
const namespacet &ns)
{
code=expr.pretty();
return false;
}
开发者ID:hc825b,项目名称:static_analysis,代码行数:8,代码来源:language.cpp
示例14: needs_cleaning
bool goto_convertt::needs_cleaning(const exprt &expr)
{
if(expr.id()==ID_index ||
expr.id()==ID_dereference ||
expr.id()==ID_sideeffect ||
expr.id()==ID_struct ||
expr.id()==ID_array ||
expr.id()==ID_union ||
expr.id()==ID_comma)
return true;
forall_operands(it, expr)
if(needs_cleaning(*it))
return true;
return false;
}
开发者ID:ashokkelur,项目名称:CBMC-With-DSP-C,代码行数:17,代码来源:goto_clean_expr.cpp
示例15: replace_nondet_sideeffects
void termination_baset::replace_nondet_sideeffects(exprt &expr)
{
if(expr.id()=="sideeffect" &&
expr.get("statement")=="nondet")
{
symbolt symbol;
symbol.name=std::string("termination::nondet")+i2string(++nondet_counter);
symbol.base_name=std::string("nondet")+i2string(nondet_counter);
symbol.type=expr.type();
expr=symbol_expr(symbol);
shadow_context.move(symbol);
}
else
Forall_operands(it, expr)
replace_nondet_sideeffects(*it);
}
开发者ID:olivo,项目名称:BP,代码行数:17,代码来源:termination_base.cpp
示例16: gen_comp_var
void component_exprt::gen_comp_var(
exprt &comp_var,
const exprt &expr,
std::string suffix)
{
std::string base;
if (expr.id()==ID_symbol)
base="."+id2string(to_symbol_expr(expr).get_identifier());
else if (expr.id()==ID_constant)
base=".const";
else if(id_maps.find(expr.id())!=id_maps.end())
base=".OPERATOR."+id_maps[expr.id()];
else
base=".OPERATOR."+id2string(expr.id());
std::string final_name="C."+id2string(source_location.get_line())+"."+i2string(instruction_number)+"_"+i2string(component_cnt)+"_"+i2string(unique_identifier)+base+suffix;
to_symbol_expr(comp_var).set_identifier(final_name);
}
开发者ID:rbavishi,项目名称:iCBMC,代码行数:17,代码来源:component_e.cpp
示例17: get
exprt boolbvt::get(const exprt &expr) const
{
if(expr.id()==ID_symbol ||
expr.id()==ID_nondet_symbol)
{
const irep_idt &identifier=expr.get(ID_identifier);
boolbv_mapt::mappingt::const_iterator it=
map.mapping.find(identifier);
if(it!=map.mapping.end())
{
const boolbv_mapt::map_entryt &map_entry=it->second;
if(is_unbounded_array(map_entry.type))
return bv_get_unbounded_array(expr);
std::vector<bool> unknown;
bvt bv;
std::size_t width=map_entry.width;
bv.resize(width);
unknown.resize(width);
for(std::size_t bit_nr=0; bit_nr<width; bit_nr++)
{
assert(bit_nr<map_entry.literal_map.size());
if(map_entry.literal_map[bit_nr].is_set)
{
unknown[bit_nr]=false;
bv[bit_nr]=map_entry.literal_map[bit_nr].l;
}
else
{
unknown[bit_nr]=true;
bv[bit_nr].clear();
}
}
return bv_get_rec(bv, unknown, 0, map_entry.type);
}
}
return SUB::get(expr);
}
开发者ID:diffblue,项目名称:cbmc,代码行数:46,代码来源:boolbv_get.cpp
示例18: make_temp_symbol
void goto_convertt::make_temp_symbol(
exprt &expr,
goto_programt &dest)
{
const locationt location=expr.find_location();
symbolt &new_symbol=new_tmp_symbol(expr.type());
code_assignt assignment;
assignment.lhs()=symbol_expr(new_symbol);
assignment.rhs()=expr;
assignment.location()=location;
convert(assignment, dest);
expr=symbol_expr(new_symbol);
}
开发者ID:huangshiyou,项目名称:esbmc,代码行数:17,代码来源:goto_sideeffects.cpp
示例19: simplify_sign
bool simplify_exprt::simplify_sign(exprt &expr)
{
if(expr.operands().size()!=1) return true;
if(expr.op0().is_constant())
{
const typet &type=ns.follow(expr.op0().type());
if(type.id()==ID_floatbv)
{
ieee_floatt value(to_constant_expr(expr.op0()));
expr.make_bool(value.get_sign());
return false;
}
else if(type.id()==ID_signedbv ||
type.id()==ID_unsignedbv)
{
mp_integer value;
if(!to_integer(expr.op0(), value))
{
expr.make_bool(value>=0);
return false;
}
}
}
return true;
}
开发者ID:diffblue,项目名称:cbmc,代码行数:28,代码来源:simplify_expr_floatbv.cpp
示例20: check_termination_argument
/// checks whether a termination argument implies termination
threevalt summarizer_fw_termt::check_termination_argument(exprt expr)
{
if(expr.is_false())
return YES;
// should be of the form /\_i g_i=> R_i
if(expr.id()==ID_and)
{
threevalt result=YES;
for(exprt::operandst::iterator it=expr.operands().begin();
it!=expr.operands().end(); it++)
{
if(it->is_true())
result=UNKNOWN;
if(it->id()==ID_implies)
{
if(it->op1().is_true())
result=UNKNOWN;
}
}
return result;
}
else
{
if(expr.id()==ID_implies)
{
if(expr.op1().is_true())
return UNKNOWN;
}
else
return !expr.is_true() ? YES : UNKNOWN;
}
return YES;
}
开发者ID:diffblue,项目名称:2ls,代码行数:35,代码来源:summarizer_fw_term.cpp
注:本文中的exprt类示例由纯净天空整理自Github/MSDocs等源码及文档管理平台,相关代码片段筛选自各路编程大神贡献的开源项目,源码版权归原作者所有,传播和使用请参考对应项目的License;未经允许,请勿转载。 |
请发表评论