#include <iostream>
#include <fstream>
#include <string>
#include <err.h>
#include <SgGraphTemplate.h>
#include <graphProcessing.h>
#include <staticCFG.h>
#include <yices_c.h>

Include dependency graph for yicesParserLib.h:

Classes
class	visitorTraversalFunc

struct	Vertex2

struct	Edge2

class	visitorTraversal

class	visitorTraversal2

Typedefs
typedef myGraph	CFGforT

typedef boost::adjacency_list < boost::vecS, boost::vecS, boost::bidirectionalS, Vertex2, Edge2 >	newGraph

typedef newGraph::vertex_descriptor	VertexID2

typedef newGraph::edge_descriptor	EdgeID2

typedef boost::graph_traits < newGraph >::vertex_iterator	vertex_iterator

typedef boost::graph_traits < newGraph > ::out_edge_iterator	out_edge_iterator

typedef boost::graph_traits < newGraph >::in_edge_iterator	in_edge_iterator

typedef boost::graph_traits < newGraph >::edge_iterator	edge_iterator

Functions
yices_expr	mainParse (vector< SgGraphNode * > expr, yices_context &ctx)

string	getGraphNodeType (SgGraphNode *sn)

void	propagateFunctionCall (std::vector< SgGraphNode * > path, int i, int pathnum)
	These should be unsatisfiable under integer logic int main (argc, argv) { int x = argc[0]; int y = argc[1]; if (x > 0 && y < 0) {. More...

long	getIndex (SgGraphNode *n)

int	getSource (int &edge, newGraph *&g)

int	getTarget (int &edge, newGraph *&g)

void	printCFGNode2 (int &cf, VertexID2 v, newGraph *&g, std::ofstream &o)

void	printCFGEdge2 (int &cf, newGraph *&cfg, std::ofstream &o)

void	printHotness2 (newGraph *&g)

string	getType (SgNode *n)

yices_expr	evalFunction (std::vector< SgGraphNode * > path, yices_context &ctx, bool mainFlag)

std::vector< int >	breakTriple (std::vector< SgGraphNode * > expr)

string	isAtom (SgNode *)

bool	isLogicalSplit (SgNode *)

string	getLogicalSplit (SgNode *)

string	getBinaryLogicOp (SgNode *)

bool	isBinaryLogicOp (SgNode *)

bool	isBinaryOp (SgNode *)

string	getBinaryOp (SgNode *)

std::vector< SgGraphNode * >	getSlice (std::vector< SgGraphNode * > vv, int i)

int	yicesCheck (int argc, char **argv)

Variables
int	FORLOOPS

bool	inconsistent

int	qst

bool	unknown_flag

std::map< SgInitializedName *, yices_var_decl >	unknowns

std::map< yices_var_decl, SgInitializedName * >	IName

std::vector< yices_var_decl >	unknownvdeclis

bool	usingNots

std::map< SgInitializedName *, std::vector< int > >	notMap

std::map< std::vector < SgGraphNode * >, std::set < int > >	calledMap

std::set< SgNode * >	unknownFunctions

std::map< SgNode , std::vector< std::vector < SgGraphNode > > >	FuncPathMap

bool	forFlag

int	nvars

std::map< SgName, string >	nameOf

bool	noAssert

std::map< SgNode *, int >	forsts

std::map< int, std::vector < SgGraphNode * > >	intvecmap

std::map< std::vector < SgGraphNode * >, int >	vecintmap

std::vector< std::vector < SgGraphNode * > >	paths

std::map< SgName, yices_expr >	getExpr

newGraph *	nGraph

SgIncidenceDirectedGraph *	openg

myGraph *	openorig

StaticCFG::CFG *	opencfg

int	rounds

int	pathnum

std::set< std::pair< VertexID2, VertexID2 > >	knownEdges

std::map< SgGraphNode *, VertexID2 >	graphVertex

std::map< int, EdgeID2 >	intedgemap

std::map< EdgeID2, int >	edgeintmap

std::map< VertexID2, int >	intmap

std::vector< VertexID >	exprs

int	ipaths

std::set< std::vector < SgGraphNode * > >	globalPaths

StaticCFG::CFG *	cfg

Typedef Documentation

typedef myGraph CFGforT

Definition at line 19 of file yicesParserLib.h.

typedef boost::adjacency_list< boost::vecS, boost::vecS, boost::bidirectionalS, Vertex2, Edge2> newGraph

Definition at line 101 of file yicesParserLib.h.

typedef newGraph::vertex_descriptor VertexID2

Definition at line 103 of file yicesParserLib.h.

typedef newGraph::edge_descriptor EdgeID2

Definition at line 104 of file yicesParserLib.h.

typedef boost::graph_traits<newGraph>::vertex_iterator vertex_iterator

Definition at line 106 of file yicesParserLib.h.

typedef boost::graph_traits<newGraph>::out_edge_iterator out_edge_iterator

Definition at line 107 of file yicesParserLib.h.

typedef boost::graph_traits<newGraph>::in_edge_iterator in_edge_iterator

Definition at line 108 of file yicesParserLib.h.

typedef boost::graph_traits<newGraph>::edge_iterator edge_iterator

Definition at line 109 of file yicesParserLib.h.

Function Documentation

yices_expr mainParse	(	vector< SgGraphNode * >	expr,
		yices_context &	ctx
	)

Definition at line 1507 of file yicesParserLib.h.

References breakTriple(), evalFunction(), SgFunctionParameterList::get_args(), SgFunctionDeclaration::get_args(), SgVariableSymbol::get_declaration(), SgFunctionDeclaration::get_orig_return_type(), SgFunctionDeclaration::get_parameterList(), SgInitializedName::get_qualified_name(), SgFunctionDeclaration::get_qualified_name(), SgGraphNode::get_SgNode(), SgVarRefExp::get_symbol(), SgInitializedName::get_type(), SgVarRefExp::get_type(), SgBoolValExp::get_value(), SgShortVal::get_value(), SgIntVal::get_value(), SgLongIntVal::get_value(), SgLongLongIntVal::get_value(), SgFloatVal::get_value(), SgDoubleVal::get_value(), SgLongDoubleVal::get_value(), SgFunctionCallExp::getAssociatedFunctionDeclaration(), getBinaryLogicOp(), getBinaryOp(), getExpr, getGraphNodeType(), getLogicalSplit(), SgName::getString(), getType(), IName, isAtom(), isBinaryLogicOp(), isBinaryOp(), isLogicalSplit(), isSgAssignOp(), isSgBoolValExp(), isSgDoubleVal(), isSgExprListExp(), isSgExprStatement(), isSgFloatVal(), isSgFunctionCallExp(), isSgInitializedName(), isSgIntVal(), isSgLongDoubleVal(), isSgLongIntVal(), isSgLongLongIntVal(), isSgNotOp(), isSgPlusPlusOp(), isSgReturnStmt(), isSgShortVal(), isSgVariableDeclaration(), isSgVarRefExp(), nameOf, notMap, nvars, rounds, unknown_flag, unknownFunctions, unknowns, unknownvdeclis, and usingNots.

Referenced by evalFunction().

string getGraphNodeType ( SgGraphNode * sn)

Definition at line 1499 of file yicesParserLib.h.

References opencfg, StaticCFG::CFG::toCFGNode(), and VirtualCFG::CFGNode::toString().

Referenced by visitorTraversal::analyzePath(), and mainParse().

void propagateFunctionCall	(	std::vector< SgGraphNode * >	path,
		int	i,
		int	pathnum
	)

These should be unsatisfiable under integer logic int main (argc, argv) { int x = argc[0]; int y = argc[1]; if (x > 0 && y < 0) {.

if (x == y) { } else if (y > x) { } else if (x*y > 0) { } else { } } else { } return 0;

Therefore there should only be 2 satisfiable paths, the primary if statement being false or the primary if statement being true and everything else false

This should translate to

(set-logic QF_LIA) (declare-fun x () Int) (declare-fun y () Int) (assert (> (x 0))) (assert (< (y 0))) (assert (= (x y))) (check-sat) (pop 1) (push 1) (assert (> (y x))) (check-sat) (pop 1) (push 1) (assert (> (* (x y) ) 0)) (check-sat) (pop 1) (check-sat) (pop 2) (check-sat)

Definition at line 167 of file yicesParserLib.h.

References calledMap, FuncPathMap, SgFunctionDeclaration::get_definition(), SgFunctionDeclaration::get_qualified_name(), SgFunctionCallExp::getAssociatedFunctionDeclaration(), isSgFunctionCallExp(), pathnum, and paths.

Referenced by visitorTraversal::analyzePath().

long getIndex ( SgGraphNode * n)

Definition at line 290 of file yicesParserLib.h.

References SgGraphNode::get_index().