• 设为首页
  • 点击收藏
  • 手机版
    手机扫一扫访问
    迪恩网络手机版
  • 关注官方公众号
    微信扫一扫关注
    迪恩网络公众号

C++ executor::ExactResolutionList类代码示例

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

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



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

示例1: handleRealloc

void SpecialFunctionHandler::handleRealloc(ExecutionState &state,
		KInstruction *target, std::vector<ref<Expr> > &arguments) {
	// XXX should type check args
	assert(arguments.size() == 2 && "invalid number of arguments to realloc");
	ref<Expr> address = arguments[0];
	ref<Expr> size = arguments[1];

	Executor::StatePair zeroSize = executor.fork(state,
			Expr::createIsZero(size), true);

	if (zeroSize.first) { // size == 0
		executor.executeFree(*zeroSize.first, address, target);
	}
	if (zeroSize.second) { // size != 0
		Executor::StatePair zeroPointer = executor.fork(*zeroSize.second,
				Expr::createIsZero(address), true);

		if (zeroPointer.first) { // address == 0
			executor.executeAlloc(*zeroPointer.first, size, false, target);
		}
		if (zeroPointer.second) { // address != 0
			Executor::ExactResolutionList rl;
			executor.resolveExact(*zeroPointer.second, address, rl, "realloc");

			for (Executor::ExactResolutionList::iterator it = rl.begin(), ie =
					rl.end(); it != ie; ++it) {
				executor.executeAlloc(*it->second, size, false, target, false,
						it->first.second);
			}
		}
	}
}
开发者ID:xdzhang-xjtu,项目名称:taint-analysis,代码行数:32,代码来源:SpecialFunctionHandler.cpp


示例2: handleMakeSymbolic

void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state,
                                                KInstruction *target,
                                                std::vector<ref<Expr> > &arguments) {
  std::string name;

  // FIXME: For backwards compatibility, we should eventually enforce the
  // correct arguments.
  if (arguments.size() == 2) {
    name = "unnamed";
  } else {
    // FIXME: Should be a user.err, not an assert.
    assert(arguments.size()==3 &&
           "invalid number of arguments to klee_make_symbolic");  
    name = readStringAtAddress(state, arguments[2]);
  }

  Executor::ExactResolutionList rl;
  executor.resolveExact(state, arguments[0], rl, "make_symbolic");
  
  for (Executor::ExactResolutionList::iterator it = rl.begin(), 
         ie = rl.end(); it != ie; ++it) {
    const MemoryObject *mo = it->first.first;
    mo->setName(name);
    
    const ObjectState *old = it->first.second;
    ExecutionState *s = it->second;
    
    if (old->readOnly) {
      executor.terminateStateOnError(*s, 
                                     "cannot make readonly object symbolic", 
                                     "user.err");
      return;
    } 

    // FIXME: Type coercion should be done consistently somewhere.
    bool res;
    bool success __attribute__ ((unused)) =
      executor.solver->mustBeTrue(*s, 
                                  EqExpr::create(ZExtExpr::create(arguments[1],
                                                                  Context::get().getPointerWidth()),
                                                 mo->getSizeExpr()),
                                  res);
    assert(success && "FIXME: Unhandled solver failure");
    
    if (res) {
      executor.executeMakeSymbolic(*s, mo, name);
    } else {      
      executor.terminateStateOnError(*s, 
                                     "wrong size given to klee_make_symbolic[_name]", 
                                     "user.err");
    }
  }
}
开发者ID:Wajihulhassan,项目名称:klee,代码行数:53,代码来源:SpecialFunctionHandler.cpp


示例3: handleGetObjSize

void SpecialFunctionHandler::handleGetObjSize(ExecutionState &state,
		KInstruction *target, std::vector<ref<Expr> > &arguments) {
	// XXX should type check args
	assert(
			arguments.size() == 1
					&& "invalid number of arguments to klee_get_obj_size");
	Executor::ExactResolutionList rl;
	executor.resolveExact(state, arguments[0], rl, "klee_get_obj_size");
	for (Executor::ExactResolutionList::iterator it = rl.begin(), ie = rl.end();
			it != ie; ++it) {
		executor.bindLocal(target, it->second->currentThread,
				ConstantExpr::create(it->first.first->size, Expr::Int32));
	}
}
开发者ID:xdzhang-xjtu,项目名称:taint-analysis,代码行数:14,代码来源:SpecialFunctionHandler.cpp


示例4: handleMakeLengthSymbolic

void SpecialFunctionHandler::handleMakeLengthSymbolic(ExecutionState &state,
                                                KInstruction *target,
                                                std::vector<ref<Expr> > &arguments) {
  std::string name;
  assert(arguments.size()==3 && "invalid number of arguments to klee_make_symbolic");  
  name = readStringAtAddress(state, arguments[2]);
  
  //std::cerr << "make_length_symbolic called len_rl.size=" << len_rl.size() << " \n";
    
  Executor::ExactResolutionList rl;
  executor.resolveExact(state, arguments[0], rl, "make_symbolic");
  
  for (Executor::ExactResolutionList::iterator it = rl.begin(), 
         ie = rl.end(); it != ie; ++it) {
    
    const ObjectState *old = it->first.second;
    ExecutionState *s = it->second;
    
    //allocate space for len_mo
    MemoryObject *len_mo = executor.executeNoBindAlloc(*s, 4);  //4-byte int
    len_mo->setName(name + "_len");
    len_mo->onlyTrackLength = 0;
    len_mo->isALength = 1;  
    executor.executeMakeSymbolic(*s, len_mo);    

    MemoryObject *mo = (MemoryObject*) it->first.first;
    mo->setName(name);
    mo->onlyTrackLength = 1;
    mo->isALength = 0;
    
    mo->length = len_mo;  //important! makes len_mo track mo->length
    
    if (old->readOnly) { 
      executor.terminateStateOnError(*s, "cannot make readonly object symbolic", "user.err");
      return;
    } 

    // FIXME: Type coercion should be done consistently somewhere.
    bool res;
    bool success = executor.solver->mustBeTrue(*s,EqExpr::create(ZExtExpr::create(arguments[1], Context::get().getPointerWidth()), mo->getSizeExpr()), res);
    assert(success && "FIXME: Unhandled solver failure");
    
    if (res) {
      executor.executeMakeSymbolic(*s, mo);
    } else {      
      executor.terminateStateOnError(*s, "wrong size given to klee_make_symbolic[_name]", "user.err");
    }
  }
}
开发者ID:zodiac,项目名称:klee-nush,代码行数:49,代码来源:SpecialFunctionHandler.cpp


示例5: handleMarkGlobal

void SpecialFunctionHandler::handleMarkGlobal(ExecutionState &state,
		KInstruction *target, std::vector<ref<Expr> > &arguments) {
	assert(
			arguments.size() == 1
					&& "invalid number of arguments to klee_mark_global");

	Executor::ExactResolutionList rl;
	executor.resolveExact(state, arguments[0], rl, "mark_global");

	for (Executor::ExactResolutionList::iterator it = rl.begin(), ie = rl.end();
			it != ie; ++it) {
		const MemoryObject *mo = it->first.first;
		assert(!mo->isLocal);
		mo->isGlobal = true;
	}
}
开发者ID:xdzhang-xjtu,项目名称:taint-analysis,代码行数:16,代码来源:SpecialFunctionHandler.cpp


示例6: handlePreferCex

void SpecialFunctionHandler::handlePreferCex(ExecutionState &state,
                                             KInstruction *target,
                                             std::vector<ref<Expr> > &arguments) {
  assert(arguments.size()==2 &&
         "invalid number of arguments to klee_prefex_cex");

  ref<Expr> cond = arguments[1];
  if (cond->getWidth() != Expr::Bool)
    cond = NeExpr::create(cond, ConstantExpr::alloc(0, cond->getWidth()));

  Executor::ExactResolutionList rl;
  executor.resolveExact(state, arguments[0], rl, "prefex_cex");
  
  assert(rl.size() == 1 &&
         "prefer_cex target must resolve to precisely one object");

  rl[0].first.first->cexPreferences.push_back(cond);
}
开发者ID:Wajihulhassan,项目名称:klee,代码行数:18,代码来源:SpecialFunctionHandler.cpp



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


鲜花

握手

雷人

路过

鸡蛋
该文章已有0人参与评论

请发表评论

全部评论

专题导读
上一篇:
C++ exifdata::const_iterator类代码示例发布时间:2022-05-31
下一篇:
C++ event::List类代码示例发布时间:2022-05-31
热门推荐
阅读排行榜

扫描微信二维码

查看手机版网站

随时了解更新最新资讯

139-2527-9053

在线客服(服务时间 9:00~18:00)

在线QQ客服
地址:深圳市南山区西丽大学城创智工业园
电邮:jeky_zhao#qq.com
移动电话:139-2527-9053

Powered by 互联科技 X3.4© 2001-2213 极客世界.|Sitemap