klee::expr::QueryCommand Class Reference

#include <Parser.h>

Inheritance diagram for klee::expr::QueryCommand:

Collaboration diagram for klee::expr::QueryCommand:

Public Member Functions
	QueryCommand (const std::vector< ExprHandle > &_Constraints, ExprHandle _Query, const std::vector< ExprHandle > &_Values, const std::vector< const Array * > &_Objects)
virtual void	dump ()
	dump - Dump the AST node to stderr. More...
Public Member Functions inherited from klee::expr::CommandDecl
	CommandDecl (DeclKind _Kind)
Public Member Functions inherited from klee::expr::Decl
	Decl (DeclKind _Kind)
virtual	~Decl ()
DeclKind	getKind () const
	getKind - Get the decl kind. More...
virtual void	dump ()=0
	dump - Dump the AST node to stderr. More...

Static Public Member Functions
static bool	classof (const Decl *D)
static bool	classof (const QueryCommand *)
Static Public Member Functions inherited from klee::expr::CommandDecl
static bool	classof (const Decl *D)
static bool	classof (const CommandDecl *)
Static Public Member Functions inherited from klee::expr::Decl
static bool	classof (const Decl *)

Public Attributes
const std::vector< ExprHandle >	Constraints
ExprHandle	Query
	Query - The expression being queried. More...
const std::vector< ExprHandle >	Values
const std::vector< const Array * >	Objects

Additional Inherited Members
Public Types inherited from klee::expr::Decl
enum	DeclKind {   ArrayDeclKind , ExprVarDeclKind , VersionVarDeclKind , QueryCommandDeclKind ,   DeclKindLast = QueryCommandDeclKind , VarDeclKindFirst = ExprVarDeclKind , VarDeclKindLast = VersionVarDeclKind , CommandDeclKindFirst = QueryCommandDeclKind ,   CommandDeclKindLast = QueryCommandDeclKind }

Detailed Description

QueryCommand - Query commands.

(query [ ... constraints ... ] expression) (query [ ... constraints ... ] expression values) (query [ ... constraints ... ] expression values objects)

Definition at line 163 of file Parser.h.

Constructor & Destructor Documentation

QueryCommand()

klee::expr::QueryCommand::QueryCommand ( const std::vector< ExprHandle > &  _Constraints, ExprHandle  _Query, const std::vector< ExprHandle > &  _Values, const std::vector< const Array * > &  _Objects  )

inline

Definition at line 186 of file Parser.h.

Member Function Documentation

classof() [1/2]

static bool klee::expr::QueryCommand::classof ( const Decl *  D )

inlinestatic

Definition at line 199 of file Parser.h.

References klee::expr::Decl::getKind(), and klee::expr::Decl::QueryCommandDeclKind.

Here is the call graph for this function:

classof() [2/2]

static bool klee::expr::QueryCommand::classof ( const QueryCommand *  )

inlinestatic

Definition at line 202 of file Parser.h.

dump()

void QueryCommand::dump ( )

virtual

dump - Dump the AST node to stderr.

Implements klee::expr::Decl.

Definition at line 1624 of file Parser.cpp.

References Constraints, Objects, klee::ExprPPrinter::printQuery(), and Values.

Here is the call graph for this function:

Member Data Documentation

Constraints

const std::vector<ExprHandle> klee::expr::QueryCommand::Constraints

Constraints - The list of constraints to assume for this expression.

Definition at line 172 of file Parser.h.

Referenced by dump().

Objects

const std::vector<const Array*> klee::expr::QueryCommand::Objects

Objects - Symbolic arrays whose initial contents should be given if the query is invalid.

Definition at line 183 of file Parser.h.

Referenced by dump().

Query

ExprHandle klee::expr::QueryCommand::Query

Query - The expression being queried.

Definition at line 175 of file Parser.h.

Values

const std::vector<ExprHandle> klee::expr::QueryCommand::Values

Values - The expressions for which counterexamples should be given if the query is invalid.

Definition at line 179 of file Parser.h.

Referenced by dump().

---

The documentation for this class was generated from the following files:

• /Users/cristic/klee/include/klee/Expr/Parser/Parser.h
• /Users/cristic/klee/lib/Expr/Parser.cpp