C++ guardt类代码示例

OStack程序员社区-中国程序员成长平台 › 门户 › 编程› C++›C++教程

原作者: [db:作者] 来自: [db:来源] 收藏邀请

本文整理汇总了C++中guardt类的典型用法代码示例。如果您正苦于以下问题：C++ guardt类的具体用法？C++ guardt怎么用？C++ guardt使用的例子？那么恭喜您, 这里精选的类代码示例或许可以为您提供帮助。

在下文中一共展示了guardt类的9个代码示例，这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞，您的评价将有助于我们的系统推荐出更棒的C++代码示例。

示例1: dereference_failure

void goto_program_dereferencet::dereference_failure(
  const std::string &property,
  const std::string &msg,
  const guardt &guard)
{
  exprt guard_expr=guard.as_expr();

  if(assertions.insert(guard_expr).second)
  {
    guard_expr.make_not();

    // first try simplifier on it
    if(options.get_bool_option("simplify"))
      simplify(guard_expr, ns);

    if(!guard_expr.is_true())
    {
      goto_program_instruction_typet type=
        options.get_bool_option("assert-to-assume")?ASSUME:ASSERT;

      goto_programt::targett t=new_code.add_instruction(type);
      t->guard.swap(guard_expr);
      t->source_location=dereference_location;
      t->source_location.set_property_class(property);
      t->source_location.set_comment("dereference failure: "+msg);
    }
  }
}

开发者ID:DanielNeville，项目名称:cbmc，代码行数:28，代码来源:goto_program_dereference.cpp

示例2: function_return

void symex_target_equationt::function_return(
  const guardt &guard,
  const sourcet &source)
{
  SSA_steps.push_back(SSA_stept());
  SSA_stept &SSA_step=SSA_steps.back();
  
  SSA_step.guard_expr=guard.as_expr();
  SSA_step.type=goto_trace_stept::FUNCTION_RETURN;
  SSA_step.source=source;
}

开发者ID:ashokkelur，项目名称:CBMC-With-DSP-C，代码行数:11，代码来源:symex_target_equation.cpp

示例3: add_guarded_claim

void goto_checkt::add_guarded_claim(
  const exprt &_expr,
  const std::string &comment,
  const std::string &property_class,
  const source_locationt &source_location,
  const exprt &src_expr,
  const guardt &guard)
{
  exprt expr(_expr);

  // first try simplifier on it
  if(enable_simplify)
    simplify(expr, ns);

  // throw away trivial properties?
  if(!retain_trivial && expr.is_true())
    return;

  // add the guard
  exprt guard_expr=guard.as_expr();

  exprt new_expr;

  if(guard_expr.is_true())
    new_expr.swap(expr);
  else
  {
    new_expr=exprt(ID_implies, bool_typet());
    new_expr.move_to_operands(guard_expr, expr);
  }

  if(assertions.insert(new_expr).second)
  {
    goto_program_instruction_typet type=
      enable_assert_to_assume?ASSUME:ASSERT;

    goto_programt::targett t=new_code.add_instruction(type);

    std::string source_expr_string=from_expr(ns, "", src_expr);

    t->guard.swap(new_expr);
    t->source_location=source_location;
    t->source_location.set_comment(comment+" in "+source_expr_string);
    t->source_location.set_property_class(property_class);
  }
}

开发者ID:diffblue，项目名称:cbmc，代码行数:46，代码来源:goto_check.cpp

示例4: add_guarded_claim

void goto_checkt::add_guarded_claim(const exprt &_expr,
    const std::string &comment, const std::string &property,
    const locationt &location, const guardt &guard)
{
  bool all_claims = options.get_bool_option("all-claims");
  exprt expr(_expr);

  // first try simplifier on it
  if (!options.get_bool_option("no-simplify"))
  {
    expr2tc tmpexpr;
    migrate_expr(expr, tmpexpr);
    base_type(tmpexpr, ns);
    expr = migrate_expr_back(tmpexpr);
    simplify(expr);
  }

  if (!all_claims && expr.is_true())
    return;

  // add the guard
  exprt guard_expr = migrate_expr_back(guard.as_expr());

  exprt new_expr;

  if (guard_expr.is_true())
    new_expr.swap(expr);
  else
  {
    new_expr = exprt("=>", bool_typet());
    new_expr.move_to_operands(guard_expr, expr);
  }

  if (assertions.insert(new_expr).second)
  {
    goto_programt::targett t = new_code.add_instruction(ASSERT);
    migrate_expr(new_expr, t->guard);

    t->location = location;
    t->location.comment(comment);
    t->location.property(property);
  }
}

开发者ID:ericksonalves，项目名称:esbmc，代码行数:43，代码来源:goto_check.cpp

示例5: read_write_rec

void rw_sett::read_write_rec(
  const exprt &expr,
  bool r, bool w,
  const std::string &suffix,
  const guardt &guard)
{
  if(expr.id()==ID_symbol)
  {
    const symbol_exprt &symbol_expr=to_symbol_expr(expr);

    const symbolt *symbol;
    if(!ns.lookup(symbol_expr.get_identifier(), symbol))
    {
      if(!symbol->static_lifetime)
        return; // ignore for now
        
      if(symbol->thread_local)
        return; // must ignore
        
      if(symbol->name=="c::__CPROVER_alloc" ||
         symbol->name=="c::__CPROVER_alloc_size" ||
         symbol->name=="c::stdin" ||
         symbol->name=="c::stdout" ||
         symbol->name=="c::stderr" ||
         symbol->name=="c::sys_nerr")
        return; // ignore for now
    }
    
    irep_idt object=id2string(symbol_expr.get_identifier())+suffix;
    
    entryt &entry=entries[object];
    entry.object=object;
    entry.r=entry.r || r;
    entry.w=entry.w || w;
    entry.guard=guard.as_expr();
  }
  else if(expr.id()=="member")

开发者ID:smaorus，项目名称:rvt，代码行数:37，代码来源:rw_set.cpp

示例6: assert

void goto_checkt::check_rec(
  const exprt &expr,
  guardt &guard,
  bool address)
{
  // we don't look into quantifiers
  if(expr.id()==ID_exists || expr.id()==ID_forall)
    return;

  if(address)
  {
    if(expr.id()==ID_dereference)
    {
      assert(expr.operands().size()==1);
      check_rec(expr.op0(), guard, false);
    }
    else if(expr.id()==ID_index)
    {
      assert(expr.operands().size()==2);
      check_rec(expr.op0(), guard, true);
      check_rec(expr.op1(), guard, false);
    }
    else
    {
      forall_operands(it, expr)
        check_rec(*it, guard, true);
    }
    return;
  }

  if(expr.id()==ID_address_of)
  {
    assert(expr.operands().size()==1);
    check_rec(expr.op0(), guard, true);
    return;
  }
  else if(expr.id()==ID_and || expr.id()==ID_or)
  {
    if(!expr.is_boolean())
      throw "`"+expr.id_string()+"' must be Boolean, but got "+
            expr.pretty();

    guardt old_guard=guard;

    for(unsigned i=0; i<expr.operands().size(); i++)
    {
      const exprt &op=expr.operands()[i];

      if(!op.is_boolean())
        throw "`"+expr.id_string()+"' takes Boolean operands only, but got "+
              op.pretty();

      check_rec(op, guard, false);

      if(expr.id()==ID_or)
        guard.add(not_exprt(op));
      else
        guard.add(op);
    }

    guard.swap(old_guard);

    return;
  }
  else if(expr.id()==ID_if)
  {
    if(expr.operands().size()!=3)
      throw "if takes three arguments";

    if(!expr.op0().is_boolean())
    {
      std::string msg=
        "first argument of if must be boolean, but got "
        +expr.op0().pretty();
      throw msg;
    }

    check_rec(expr.op0(), guard, false);

    {
      guardt old_guard=guard;
      guard.add(expr.op0());
      check_rec(expr.op1(), guard, false);
      guard.swap(old_guard);
    }

    {
      guardt old_guard=guard;
      guard.add(not_exprt(expr.op0()));
      check_rec(expr.op2(), guard, false);
      guard.swap(old_guard);
    }

    return;
  }

  forall_operands(it, expr)
    check_rec(*it, guard, false);

  if(expr.id()==ID_index)
//.........这里部分代码省略.........

开发者ID:diffblue，项目名称:cbmc，代码行数:101，代码来源:goto_check.cpp

示例7: check_rec

void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
{

  if (address)
  {
    if (expr.id() == "dereference")
    {
      assert(expr.operands().size() == 1);
      check_rec(expr.op0(), guard, false);
    }
    else if (expr.id() == "index")
    {
      assert(expr.operands().size() == 2);
      check_rec(expr.op0(), guard, true);
      check_rec(expr.op1(), guard, false);
    }
    else
    {
      forall_operands(it, expr)
        check_rec(*it, guard, true);
    }
    return;
  }

  if (expr.is_address_of())
  {
    assert(expr.operands().size() == 1);
    check_rec(expr.op0(), guard, true);
    return;
  }
  else if (expr.is_and() || expr.id() == "or")
  {
    if (!expr.is_boolean())
      throw expr.id_string() + " must be Boolean, but got " + expr.pretty();

    unsigned old_guards = guard.size();

    for (unsigned i = 0; i < expr.operands().size(); i++)
    {
      const exprt &op = expr.operands()[i];

      if (!op.is_boolean())
        throw expr.id_string() + " takes Boolean operands only, but got "
            + op.pretty();

      check_rec(op, guard, false);

      if (expr.id() == "or")
      {
        exprt tmp(op);
        tmp.make_not();
        expr2tc tmp_expr;
        migrate_expr(tmp, tmp_expr);
        guard.move(tmp_expr);
      }
      else
      {
        expr2tc tmp;
        migrate_expr(op, tmp);
        guard.add(tmp);
      }
    }

    guard.resize(old_guards);

    return;
  }
  else if (expr.id() == "if")
  {
    if (expr.operands().size() != 3)
      throw "if takes three arguments";

    if (!expr.op0().is_boolean())
    {
      std::string msg = "first argument of if must be boolean, but got "
          + expr.op0().to_string();
      throw msg;
    }

    check_rec(expr.op0(), guard, false);

    {
      unsigned old_guard = guard.size();
      expr2tc tmp;
      migrate_expr(expr.op0(), tmp);
      guard.add(tmp);
      check_rec(expr.op1(), guard, false);
      guard.resize(old_guard);
    }

    {
      unsigned old_guard = guard.size();
      exprt tmp(expr.op0());
      tmp.make_not();
      expr2tc tmp_expr;
      migrate_expr(tmp, tmp_expr);
      guard.move(tmp_expr);
      check_rec(expr.op2(), guard, false);
      guard.resize(old_guard);
    }
//.........这里部分代码省略.........

开发者ID:ericksonalves，项目名称:esbmc，代码行数:101，代码来源:goto_check.cpp

示例8: dereference_rec

void goto_program_dereferencet::dereference_rec(
  exprt &expr,
  guardt &guard,
  const value_set_dereferencet::modet mode)
{
  if(!dereference.has_dereference(expr))
    return;

  if(expr.id()==ID_and || expr.id()==ID_or)
  {
    if(!expr.is_boolean())
      throw expr.id_string()+" must be Boolean, but got "+
            expr.pretty();

    guardt old_guard=guard;

    for(unsigned i=0; i<expr.operands().size(); i++)
    {
      exprt &op=expr.operands()[i];

      if(!op.is_boolean())
        throw expr.id_string()+" takes Boolean operands only, but got "+
              op.pretty();

      if(dereference.has_dereference(op))
        dereference_rec(op, guard, value_set_dereferencet::modet::READ);

      if(expr.id()==ID_or)
      {
        exprt tmp(op);
        tmp.make_not();
        guard.add(tmp);
      }
      else
        guard.add(op);
    }

    guard.swap(old_guard);

    return;
  }
  else if(expr.id()==ID_if)
  {
    if(expr.operands().size()!=3)
      throw "if takes three arguments";

    if(!expr.op0().is_boolean())
    {
      std::string msg=
        "first argument of if must be boolean, but got "
        +expr.op0().pretty();
      throw msg;
    }

    dereference_rec(expr.op0(), guard, value_set_dereferencet::modet::READ);

    bool o1=dereference.has_dereference(expr.op1());
    bool o2=dereference.has_dereference(expr.op2());

    if(o1)
    {
      guardt old_guard=guard;
      guard.add(expr.op0());
      dereference_rec(expr.op1(), guard, mode);
      guard.swap(old_guard);
    }

    if(o2)
    {
      guardt old_guard=guard;
      exprt tmp(expr.op0());
      tmp.make_not();
      guard.add(tmp);
      dereference_rec(expr.op2(), guard, mode);
      guard.swap(old_guard);
    }

    return;
  }

  if(expr.id()==ID_address_of ||
     expr.id()=="reference_to")
  {
    // turn &*p to p
    // this has *no* side effect!

    assert(expr.operands().size()==1);

    if(expr.op0().id()==ID_dereference)
    {
      assert(expr.op0().operands().size()==1);

      exprt tmp;
      tmp.swap(expr.op0().op0());

      if(tmp.type()!=expr.type())
        tmp.make_typecast(expr.type());

      expr.swap(tmp);
    }
//.........这里部分代码省略.........

开发者ID:DanielNeville，项目名称:cbmc，代码行数:101，代码来源:goto_program_dereference.cpp

示例9: migrate_expr_back

void rw_sett::read_write_rec(
  const exprt &expr,
  bool r, bool w,
  const std::string &suffix,
  const guardt &guard)
{
  if(expr.id()=="symbol" && !expr.has_operands())
  {
    const symbol_exprt &symbol_expr=to_symbol_expr(expr);

    const symbolt *symbol;
    if(!ns.lookup(symbol_expr.get_identifier(), symbol))
    {

      if(!symbol->static_lifetime /*&& expr.type().id()=="pointer"*/)
      {
        return; // ignore for now
      }

      if(symbol->name=="c::__ESBMC_alloc" ||
         symbol->name=="c::__ESBMC_alloc_size" ||
         symbol->name=="c::stdin" ||
         symbol->name=="c::stdout" ||
         symbol->name=="c::stderr" ||
         symbol->name=="c::sys_nerr")
      {
        return; // ignore for now
      }
    }

    irep_idt object=id2string(symbol_expr.get_identifier())+suffix;

    entryt &entry=entries[object];
    entry.object=object;
    entry.r=entry.r || r;
    entry.w=entry.w || w;
    entry.guard = migrate_expr_back(guard.as_expr());
  }
  else if(expr.id()=="member")
  {
    assert(expr.operands().size()==1);
    const std::string &component_name=expr.component_name().as_string();
    read_write_rec(expr.op0(), r, w, "."+component_name+suffix, guard);
  }
  else if(expr.id()=="index")
  {
    // we don't distinguish the array elements for now
    assert(expr.operands().size()==2);
    std::string tmp;

    tmp = integer2string(binary2integer(expr.op1().value().as_string(), true),10);

    read_write_rec(expr.op0(), r, w, "["+suffix+tmp+"]", guard);
    read(expr.op1(), guard);
  }
  else if(expr.id()=="dereference")
  {
    assert(expr.operands().size()==1);
    read(expr.op0(), guard);

    exprt tmp(expr.op0());
    expr2tc tmp_expr;
    migrate_expr(tmp, tmp_expr);
    dereference(target, tmp_expr, ns, value_sets);
    tmp = migrate_expr_back(tmp_expr);

    read_write_rec(tmp, r, w, suffix, guard);
  }
  else if(expr.is_address_of() ||
          expr.id()=="implicit_address_of")
  {
    assert(expr.operands().size()==1);

  }
  else if(expr.id()=="if")
  {
    assert(expr.operands().size()==3);
    read(expr.op0(), guard);

    guardt true_guard(guard);
    expr2tc tmp_expr;
    migrate_expr(expr.op0(), tmp_expr);
    true_guard.add(tmp_expr);
    read_write_rec(expr.op1(), r, w, suffix, true_guard);

    guardt false_guard(guard);
    migrate_expr(gen_not(expr.op0()), tmp_expr);
    false_guard.add(tmp_expr);
    read_write_rec(expr.op2(), r, w, suffix, false_guard);
  }
  else
  {
    forall_operands(it, expr)
      read_write_rec(*it, r, w, suffix, guard);
  }
}

开发者ID:ericksonalves，项目名称:esbmc，代码行数:96，代码来源:rw_set.cpp

注：本文中的guardt类示例由纯净天空整理自Github/MSDocs等源码及文档管理平台，相关代码片段筛选自各路编程大神贡献的开源项目，源码版权归原作者所有，传播和使用请参考对应项目的License；未经允许，请勿转载。