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/SMTConv.h"
#include "llvm/ADT/Statistic.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
	STATISTIC (NumZ3QueriesDone, "Number of Z3 queries done")
	STATISTIC (NumTimesZ3TimedOut, "Number of times Z3 query timed out")
	STATISTIC (NumTimesZ3ExhaustedRLimit, "Number of times Z3 query exhausted the rlimit")
	STATISTIC (NumTimesZ3SpendsTooMuchTimeOnASingleEQClass, "Number of times report equivalenece class was cut because it spent " "too much time in Z3")
	STATISTIC (NumTimesZ3QueryAcceptsReport, "Number of Z3 queries accepting a report")
	STATISTIC (NumTimesZ3QueryRejectReport, "Number of Z3 queries rejecting a report")
	STATISTIC (NumTimesZ3QueryRejectEQClass, "Number of times rejecting an report equivalenece class")

Macro Definition Documentation

DEBUG_TYPE

#define DEBUG_TYPE   "Z3CrosscheckOracle"

Definition at line 22 of file Z3CrosscheckVisitor.cpp.

Function Documentation

STATISTIC() [1/7]

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

STATISTIC() [2/7]

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

STATISTIC() [3/7]

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

STATISTIC() [4/7]

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

STATISTIC() [5/7]

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

STATISTIC() [6/7]

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

STATISTIC() [7/7]

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