Z3CrosscheckVisitor.cpp File Reference

#include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h"
#include "clang/StaticAnalyzer/Core/AnalyzerOptions.h"
#include "clang/StaticAnalyzer/Core/BugReporter/BugReporter.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/EntryPointStats.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
#include "llvm/Support/SMTAPI.h"
#include "llvm/Support/Timer.h"

Go to the source code of this file.

Macros
#define	DEBUG_TYPE   "Z3CrosscheckOracle"

Functions
	STAT_COUNTER (NumZ3QueriesDone, "Number of Z3 queries done")
	STAT_COUNTER (NumTimesZ3TimedOut, "Number of times Z3 query timed out")
	STAT_COUNTER (NumTimesZ3ExhaustedRLimit, "Number of times Z3 query exhausted the rlimit")
	STAT_COUNTER (NumTimesZ3SpendsTooMuchTimeOnASingleEQClass, "Number of times report equivalenece class was cut because it spent " "too much time in Z3")
	STAT_COUNTER (NumTimesZ3QueryAcceptsReport, "Number of Z3 queries accepting a report")
	STAT_COUNTER (NumTimesZ3QueryRejectReport, "Number of Z3 queries rejecting a report")
	STAT_COUNTER (NumTimesZ3QueryRejectEQClass, "Number of times rejecting an report equivalenece class")
	STAT_COUNTER (TimeSpentSolvingZ3Queries, "Total time spent solving Z3 queries excluding retries")
	STAT_MAX (MaxTimeSpentSolvingZ3Queries, "Max time spent solving a Z3 query excluding retries")

Macro Definition Documentation

DEBUG_TYPE

#define DEBUG_TYPE   "Z3CrosscheckOracle"

Definition at line 22 of file Z3CrosscheckVisitor.cpp.

Function Documentation

STAT_COUNTER() [1/8]

STAT_COUNTER	(	NumTimesZ3ExhaustedRLimit	,
		"Number of times Z3 query exhausted the rlimit"	)

STAT_COUNTER() [2/8]

STAT_COUNTER	(	NumTimesZ3QueryAcceptsReport	,
		"Number of Z3 queries accepting a report"	)

STAT_COUNTER() [3/8]

STAT_COUNTER	(	NumTimesZ3QueryRejectEQClass	,
		"Number of times rejecting an report equivalenece class"	)

STAT_COUNTER() [4/8]

STAT_COUNTER	(	NumTimesZ3QueryRejectReport	,
		"Number of Z3 queries rejecting a report"	)

STAT_COUNTER() [5/8]

STAT_COUNTER	(	NumTimesZ3SpendsTooMuchTimeOnASingleEQClass	,
		"Number of times report equivalenece class was cut because it spent " "too much time in Z3"	)

STAT_COUNTER() [6/8]

STAT_COUNTER	(	NumTimesZ3TimedOut	,
		"Number of times Z3 query timed out"	)

STAT_COUNTER() [7/8]

STAT_COUNTER	(	NumZ3QueriesDone	,
		"Number of Z3 queries done"	)

STAT_COUNTER() [8/8]

STAT_COUNTER	(	TimeSpentSolvingZ3Queries	,
		"Total time spent solving Z3 queries excluding retries"	)

STAT_MAX()

STAT_MAX	(	MaxTimeSpentSolvingZ3Queries	,
		"Max time spent solving a Z3 query excluding retries"	)