本文整理汇总了C++中codet类的典型用法代码示例。如果您正苦于以下问题:C++ codet类的具体用法?C++ codet怎么用?C++ codet使用的例子?那么恭喜您, 这里精选的类代码示例或许可以为您提供帮助。
在下文中一共展示了codet类的20个代码示例,这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞,您的评价将有助于我们的系统推荐出更棒的C++代码示例。
示例1: convert_CPROVER_try_catch
void goto_convertt::convert_CPROVER_try_catch(
const codet &code,
goto_programt &dest)
{
if(code.operands().size()!=2)
{
err_location(code);
throw "CPROVER_try_catch expects two arguments";
}
// this is where we go after 'throw'
goto_programt tmp;
tmp.add_instruction(SKIP)->source_location=code.source_location();
// set 'throw' target
throw_targett throw_target(targets);
targets.set_throw(tmp.instructions.begin());
// now put 'catch' code onto destructor stack
code_ifthenelset catch_code;
catch_code.cond()=exception_flag();
catch_code.add_source_location()=code.source_location();
catch_code.then_case()=to_code(code.op1());
targets.destructor_stack.push_back(catch_code);
// now convert 'try' code
convert(to_code(code.op0()), dest);
// pop 'catch' code off stack
targets.destructor_stack.pop_back();
// add 'throw' target
dest.destructive_append(tmp);
}
开发者ID:Dthird,项目名称:CBMC,代码行数:35,代码来源:goto_convert_exceptions.cpp
示例2: error
void goto_convertt::convert_msc_leave(
const codet &code,
goto_programt &dest)
{
if(!targets.leave_set)
{
error().source_location=code.find_source_location();
error() << "leave without target" << eom;
throw 0;
}
// need to process destructor stack
for(unsigned d=targets.destructor_stack.size();
d!=targets.leave_stack_size;
d--)
{
codet d_code=targets.destructor_stack[d-1];
d_code.add_source_location()=code.source_location();
convert(d_code, dest);
}
goto_programt::targett t=dest.add_instruction();
t->make_goto(targets.leave_target);
t->source_location=code.source_location();
}
开发者ID:,项目名称:,代码行数:25,代码来源:
示例3: convert_CPROVER_throw
void goto_convertt::convert_CPROVER_throw(
const codet &code,
goto_programt &dest)
{
// set the 'exception' flag
{
goto_programt::targett t_set_exception=
dest.add_instruction(ASSIGN);
t_set_exception->source_location=code.source_location();
t_set_exception->code=code_assignt(exception_flag(), true_exprt());
}
// do we catch locally?
if(targets.throw_set)
{
// need to process destructor stack
unwind_destructor_stack(code.source_location(), targets.throw_stack_size, dest);
// add goto
goto_programt::targett t=dest.add_instruction();
t->make_goto(targets.throw_target);
t->source_location=code.source_location();
}
else // otherwise, we do a return
{
// need to process destructor stack
unwind_destructor_stack(code.source_location(), 0, dest);
// add goto
goto_programt::targett t=dest.add_instruction();
t->make_goto(targets.return_target);
t->source_location=code.source_location();
}
}
开发者ID:Dthird,项目名称:CBMC,代码行数:35,代码来源:goto_convert_exceptions.cpp
示例4: typecheck_code
void java_bytecode_typecheckt::typecheck_code(codet &code)
{
const irep_idt &statement=code.get_statement();
if(statement==ID_assign)
{
code_assignt &code_assign=to_code_assign(code);
typecheck_expr(code_assign.lhs());
typecheck_expr(code_assign.rhs());
if(code_assign.lhs().type()!=code_assign.rhs().type())
code_assign.rhs().make_typecast(code_assign.lhs().type());
}
else if(statement==ID_block)
{
Forall_operands(it, code)
typecheck_code(to_code(*it));
}
else if(statement==ID_label)
{
code_labelt &code_label=to_code_label(code);
typecheck_code(code_label.code());
}
else if(statement==ID_goto)
{
}
else if(statement==ID_ifthenelse)
{
code_ifthenelset &code_ifthenelse=to_code_ifthenelse(code);
typecheck_expr(code_ifthenelse.cond());
typecheck_code(code_ifthenelse.then_case());
if(code_ifthenelse.else_case().is_not_nil())
typecheck_code(code_ifthenelse.else_case());
}
else if(statement==ID_switch)
{
code_switcht &code_switch = to_code_switch(code);
typecheck_expr(code_switch.value());
}
else if(statement==ID_return)
{
if(code.operands().size()==1)
typecheck_expr(code.op0());
}
else if(statement==ID_function_call)
{
code_function_callt &code_function_call=to_code_function_call(code);
typecheck_expr(code_function_call.lhs());
typecheck_expr(code_function_call.function());
for(code_function_callt::argumentst::iterator
a_it=code_function_call.arguments().begin();
a_it!=code_function_call.arguments().end();
a_it++)
typecheck_expr(*a_it);
}
}
开发者ID:dcattaruzza,项目名称:cbmc,代码行数:57,代码来源:java_bytecode_typecheck_code.cpp
示例5: compute
void rw_sett::compute(const codet &code)
{
const irep_idt &statement=code.get_statement();
if(statement==ID_assign)
{
assert(code.operands().size()==2);
assign(code.op0(), code.op1());
}
}
开发者ID:smaorus,项目名称:rvt,代码行数:10,代码来源:rw_set.cpp
示例6: typecheck_start_thread
void c_typecheck_baset::typecheck_start_thread(codet &code)
{
if(code.operands().size()!=1)
{
err_location(code);
error() << "start_thread expected to have one operand" << eom;
throw 0;
}
typecheck_code(to_code(code.op0()));
}
开发者ID:diffblue,项目名称:cbmc,代码行数:11,代码来源:c_typecheck_code.cpp
示例7: assert
void goto_convertt::convert_try_catch(
const codet &code,
goto_programt &dest)
{
assert(code.operands().size()>=2);
// add the CATCH-push instruction to 'dest'
goto_programt::targett catch_push_instruction=dest.add_instruction();
catch_push_instruction->make_catch();
catch_push_instruction->code.set_statement(ID_catch);
catch_push_instruction->source_location=code.source_location();
// the CATCH-push instruction is annotated with a list of IDs,
// one per target
irept::subt &exception_list=
catch_push_instruction->code.add(ID_exception_list).get_sub();
// add a SKIP target for the end of everything
goto_programt end;
goto_programt::targett end_target=end.add_instruction();
end_target->make_skip();
// the first operand is the 'try' block
convert(to_code(code.op0()), dest);
// add the CATCH-pop to the end of the 'try' block
goto_programt::targett catch_pop_instruction=dest.add_instruction();
catch_pop_instruction->make_catch();
catch_pop_instruction->code.set_statement(ID_catch);
// add a goto to the end of the 'try' block
dest.add_instruction()->make_goto(end_target);
for(unsigned i=1; i<code.operands().size(); i++)
{
const codet &block=to_code(code.operands()[i]);
// grab the ID and add to CATCH instruction
exception_list.push_back(irept(block.get(ID_exception_id)));
goto_programt tmp;
convert(block, tmp);
catch_push_instruction->targets.push_back(tmp.instructions.begin());
dest.destructive_append(tmp);
// add a goto to the end of the 'catch' block
dest.add_instruction()->make_goto(end_target);
}
// add the end-target
dest.destructive_append(end);
}
开发者ID:,项目名称:,代码行数:52,代码来源:
示例8: typecheck_spec_expr
void c_typecheck_baset::typecheck_spec_expr(
codet &code,
const irep_idt &spec)
{
if(code.find(spec).is_not_nil())
{
exprt &constraint=
static_cast<exprt&>(code.add(spec));
typecheck_expr(constraint);
implicit_typecast_bool(constraint);
}
}
开发者ID:diffblue,项目名称:cbmc,代码行数:13,代码来源:c_typecheck_code.cpp
示例9: typecheck_expression
void c_typecheck_baset::typecheck_expression(codet &code)
{
if(code.operands().size()!=1)
{
err_location(code);
error() << "expression statement expected to have one operand"
<< eom;
throw 0;
}
exprt &op=code.op0();
typecheck_expr(op);
}
开发者ID:diffblue,项目名称:cbmc,代码行数:13,代码来源:c_typecheck_code.cpp
示例10: convert_msc_try_except
void goto_convertt::convert_msc_try_except(
const codet &code,
goto_programt &dest)
{
if(code.operands().size()!=3)
{
err_location(code);
throw "msc_try_except expects three arguments";
}
convert(to_code(code.op0()), dest);
// todo: generate exception tracking
}
开发者ID:Dthird,项目名称:CBMC,代码行数:14,代码来源:goto_convert_exceptions.cpp
示例11: convert_java_try_catch
void goto_convertt::convert_java_try_catch(
const codet &code,
goto_programt &dest)
{
assert(!code.operands().empty());
// add the CATCH instruction to 'dest'
goto_programt::targett catch_instruction=dest.add_instruction();
catch_instruction->make_catch();
catch_instruction->code.set_statement(ID_catch);
catch_instruction->source_location=code.source_location();
catch_instruction->function=code.source_location().get_function();
// the CATCH instruction is annotated with a list of exception IDs
const irept exceptions=code.op0().find(ID_exception_list);
if(exceptions.is_not_nil())
{
irept::subt exceptions_sub=exceptions.get_sub();
irept::subt &exception_list=
catch_instruction->code.add(ID_exception_list).get_sub();
exception_list.resize(exceptions_sub.size());
for(size_t i=0; i<exceptions_sub.size(); ++i)
exception_list[i].id(exceptions_sub[i].id());
}
// the CATCH instruction is also annotated with a list of handle labels
const irept handlers=code.op0().find(ID_label);
if(handlers.is_not_nil())
{
irept::subt handlers_sub=handlers.get_sub();
irept::subt &handlers_list=
catch_instruction->code.add(ID_label).get_sub();
handlers_list.resize(handlers_sub.size());
for(size_t i=0; i<handlers_sub.size(); ++i)
handlers_list[i].id(handlers_sub[i].id());
}
// the CATCH instruction may also signal a handler
if(code.op0().has_operands())
{
catch_instruction->code.get_sub().resize(1);
catch_instruction->code.get_sub()[0]=code.op0().op0();
}
// add a SKIP target for the end of everything
goto_programt end;
goto_programt::targett end_target=end.add_instruction();
end_target->make_skip();
end_target->source_location=code.source_location();
end_target->function=code.source_location().get_function();
// add the end-target
dest.destructive_append(end);
}
开发者ID:DanielNeville,项目名称:cbmc,代码行数:54,代码来源:goto_convert_exceptions.cpp
示例12: typecheck_assign
void c_typecheck_baset::typecheck_assign(codet &code)
{
if(code.operands().size()!=2)
{
err_location(code);
error() << "assignment statement expected to have two operands"
<< eom;
throw 0;
}
typecheck_expr(code.op0());
typecheck_expr(code.op1());
implicit_typecast(code.op1(), code.op0().type());
}
开发者ID:diffblue,项目名称:cbmc,代码行数:15,代码来源:c_typecheck_code.cpp
示例13: convert_msc_try_except
void goto_convertt::convert_msc_try_except(
const codet &code,
goto_programt &dest)
{
if(code.operands().size()!=3)
{
error().source_location=code.find_source_location();
error() << "msc_try_except expects three arguments" << eom;
throw 0;
}
convert(to_code(code.op0()), dest);
// todo: generate exception tracking
}
开发者ID:,项目名称:,代码行数:15,代码来源:
示例14: static_lifetime_init
void static_lifetime_init(
const contextt &context,
codet &dest)
{
dest=code_blockt();
// Do assignments based on "value".
context.foreach_operand_in_order(
[&dest] (const symbolt& s)
{
if(s.static_lifetime)
init_variable(dest, s);
}
);
// call designated "initialization" functions
context.foreach_operand_in_order(
[&dest] (const symbolt& s)
{
if(s.type.initialization() && s.type.is_code())
{
code_function_callt function_call;
function_call.function() = symbol_expr(s);
dest.move_to_operands(function_call);
}
}
);
}
开发者ID:ericksonalves,项目名称:esbmc,代码行数:28,代码来源:c_main.cpp
示例15: typecheck_code
void jsil_typecheckt::typecheck_code(codet &code)
{
const irep_idt &statement=code.get_statement();
if(statement==ID_function_call)
typecheck_function_call(to_code_function_call(code));
else if(statement==ID_return)
typecheck_return(to_code_return(code));
else if(statement==ID_expression)
{
if(code.operands().size()!=1)
throw "expression statement expected to have one operand";
typecheck_expr(code.op0());
}
else if(statement==ID_label)
{
typecheck_code(to_code_label(code).code());
// TODO: produce defined label set
}
else if(statement==ID_block)
typecheck_block(code);
else if(statement==ID_ifthenelse)
typecheck_ifthenelse(to_code_ifthenelse(code));
else if(statement==ID_goto)
{
// TODO: produce used label set
}
else if(statement==ID_assign)
typecheck_assign(to_code_assign(code));
else if(statement==ID_try_catch)
typecheck_try_catch(to_code_try_catch(code));
else if(statement==ID_skip)
{
}
else
{
err_location(code);
error() << "unexpected statement: " << statement << eom;
throw 0;
}
}
开发者ID:diffblue,项目名称:cbmc,代码行数:42,代码来源:jsil_typecheck.cpp
示例16: typecheck_return
void c_typecheck_baset::typecheck_return(codet &code)
{
if(code.operands().empty())
{
if(follow(return_type).id()!=ID_empty)
{
// gcc doesn't actually complain, it just warns!
// We'll put a zero here, which is dubious.
exprt zero=zero_initializer(return_type, code.source_location(), *this, get_message_handler());
code.copy_to_operands(zero);
}
}
else if(code.operands().size()==1)
{
typecheck_expr(code.op0());
if(follow(return_type).id()==ID_empty)
{
// gcc doesn't actually complain, it just warns!
if(follow(code.op0().type()).id()!=ID_empty)
{
warning().source_location=code.source_location();
warning() << "function has return void ";
warning() << "but a return statement returning ";
warning() << to_string(follow(code.op0().type()));
warning() << eom;
code.op0().make_typecast(return_type);
}
}
else
implicit_typecast(code.op0(), return_type);
}
else
{
err_location(code);
error() << "return expected to have 0 or 1 operands" << eom;
throw 0;
}
}
开发者ID:diffblue,项目名称:cbmc,代码行数:41,代码来源:c_typecheck_code.cpp
示例17: convert_java_new
std::string expr2javat::convert_code(
const codet &src,
unsigned indent)
{
const irep_idt &statement=src.get(ID_statement);
if(statement==ID_java_new ||
statement==ID_java_new_array)
return convert_java_new(src,indent);
return expr2ct::convert_code(src, indent);
}
开发者ID:Dthird,项目名称:CBMC,代码行数:12,代码来源:expr2java.cpp
示例18: typecheck_asm
void c_typecheck_baset::typecheck_asm(codet &code)
{
const irep_idt flavor=to_code_asm(code).get_flavor();
if(flavor==ID_gcc)
{
// These have 5 operands.
// The first parameter is a string.
// Parameters 1, 2, 3, 4 are lists of expressions.
// Parameter 1: OutputOperands
// Parameter 2: InputOperands
// Parameter 3: Clobbers
// Parameter 4: GotoLabels
assert(code.operands().size()==5);
typecheck_expr(code.op0());
for(unsigned i=1; i<code.operands().size(); i++)
{
exprt &list=code.operands()[i];
Forall_operands(it, list)
typecheck_expr(*it);
}
}
else if(flavor==ID_msc)
{
assert(code.operands().size()==1);
typecheck_expr(code.op0());
}
}
开发者ID:diffblue,项目名称:cbmc,代码行数:32,代码来源:c_typecheck_code.cpp
示例19: convert_CPROVER_try_finally
void goto_convertt::convert_CPROVER_try_finally(
const codet &code,
goto_programt &dest)
{
if(code.operands().size()!=2)
{
err_location(code);
throw "CPROVER_try_finally expects two arguments";
}
// first put 'finally' code onto destructor stack
targets.destructor_stack.push_back(to_code(code.op1()));
// do 'try' code
convert(to_code(code.op0()), dest);
// pop 'finally' from destructor stack
targets.destructor_stack.pop_back();
// now add 'finally' code
convert(to_code(code.op1()), dest);
}
开发者ID:Dthird,项目名称:CBMC,代码行数:22,代码来源:goto_convert_exceptions.cpp
示例20: Forall_operands
void c_typecheck_baset::typecheck_block(codet &code)
{
Forall_operands(it, code)
typecheck_code(to_code(*it));
// do decl-blocks
exprt new_ops;
new_ops.operands().reserve(code.operands().size());
Forall_operands(it1, code)
{
if(it1->is_nil()) continue;
codet &code_op=to_code(*it1);
if(code_op.get_statement()==ID_label)
{
// these may be nested
codet *code_ptr=&code_op;
while(code_ptr->get_statement()==ID_label)
{
assert(code_ptr->operands().size()==1);
code_ptr=&to_code(code_ptr->op0());
}
//codet &label_op=*code_ptr;
new_ops.move_to_operands(code_op);
}
else
new_ops.move_to_operands(code_op);
}
code.operands().swap(new_ops.operands());
}
开发者ID:diffblue,项目名称:cbmc,代码行数:37,代码来源:c_typecheck_code.cpp
注:本文中的codet类示例由纯净天空整理自Github/MSDocs等源码及文档管理平台,相关代码片段筛选自各路编程大神贡献的开源项目,源码版权归原作者所有,传播和使用请参考对应项目的License;未经允许,请勿转载。 |
请发表评论