#include "klee/Expr/ArrayExprOptimizer.h"
#include "klee/ADT/BitArray.h"
#include "klee/Config/Version.h"
#include "klee/Expr/ArrayExprRewriter.h"
#include "klee/Expr/ArrayExprVisitor.h"
#include "klee/Expr/Assignment.h"
#include "klee/Expr/AssignmentGenerator.h"
#include "klee/Expr/ExprBuilder.h"
#include "klee/Support/Casting.h"
#include "klee/Support/ErrorHandling.h"
#include "klee/Support/OptionCategories.h"
#include <llvm/ADT/APInt.h>
#include <llvm/Support/CommandLine.h>
#include <algorithm>
#include <cassert>
#include <cstddef>
#include <set>

Include dependency graph for ArrayExprOptimizer.cpp:

Namespaces
namespace	klee

Functions
llvm::cl::opt< ArrayOptimizationType >	klee::OptimizeArray ("optimize-array", llvm::cl::values(clEnumValN(ALL, "all", "Combining index and value transformations"), clEnumValN(INDEX, "index", "Index-based transformation"), clEnumValN(VALUE, "value", "Value-based transformation at branch (both " "concrete and concrete/symbolic)")), llvm::cl::init(NONE), llvm::cl::desc("Optimize accesses to either concrete or concrete/symbolic " "arrays. (default=false)"), llvm::cl::cat(klee::SolvingCat))

llvm::cl::opt< double >	klee::ArrayValueRatio ("array-value-ratio", llvm::cl::desc("Maximum ratio of unique values to array size for which the " "value-based transformations are applied."), llvm::cl::init(1.0), llvm::cl::value_desc("Unique Values / Array Size"), llvm::cl::cat(klee::SolvingCat))

llvm::cl::opt< double >	klee::ArrayValueSymbRatio ("array-value-symb-ratio", llvm::cl::desc("Maximum ratio of symbolic values to array size for which " "the mixed value-based transformations are applied."), llvm::cl::init(1.0), llvm::cl::value_desc("Symbolic Values / Array Size"), llvm::cl::cat(klee::SolvingCat))

ref< Expr >	extendRead (const UpdateList &ul, const ref< Expr > index, Expr::Width w)

Function Documentation

◆ extendRead()

ref< Expr > extendRead	(	const UpdateList &	ul,
		const ref< Expr >	index,
		Expr::Width	w
	)

Definition at line 62 of file ArrayExprOptimizer.cpp.

Referenced by klee::ExprOptimizer::buildMixedSelectExpr().

Here is the caller graph for this function:

Namespaces

Functions

Function Documentation

◆ extendRead()