klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
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...
 

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< ExprHandleConstraints
 
ExprHandle Query
 Query - The expression being queried. More...
 
const std::vector< ExprHandleValues
 
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

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

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:

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

Definition at line 202 of file Parser.h.

void QueryCommand::dump ( )
virtual

dump - Dump the AST node to stderr.

Implements klee::expr::Decl.

Definition at line 1583 of file Parser.cpp.

References klee::ExprPPrinter::printQuery(), and klee::Array::size.

Here is the call graph for this function:

Member Data Documentation

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.

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.

ExprHandle klee::expr::QueryCommand::Query

Query - The expression being queried.

Definition at line 175 of file Parser.h.

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.


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