#include "klee/ADT/TreeStream.h"
#include "klee/Config/Version.h"
#include "klee/Core/Interpreter.h"
#include "klee/Expr/Expr.h"
#include "klee/ADT/KTest.h"
#include "klee/Support/OptionCategories.h"
#include "klee/Statistics/Statistics.h"
#include "klee/Solver/SolverCmdLine.h"
#include "klee/Support/Debug.h"
#include "klee/Support/ErrorHandling.h"
#include "klee/Support/FileHandling.h"
#include "klee/Support/ModuleUtil.h"
#include "klee/Support/PrintVersion.h"
#include "klee/System/Time.h"
#include "llvm/Bitcode/BitcodeReader.h"
#include "llvm/IR/Constants.h"
#include "llvm/IR/IRBuilder.h"
#include "llvm/IR/InstrTypes.h"
#include "llvm/IR/Instruction.h"
#include "llvm/IR/Instructions.h"
#include "llvm/IR/LLVMContext.h"
#include "llvm/IR/Type.h"
#include "llvm/Support/CommandLine.h"
#include "llvm/Support/Errno.h"
#include "llvm/Support/FileSystem.h"
#include "llvm/Support/Host.h"
#include "llvm/Support/ManagedStatic.h"
#include "llvm/Support/MemoryBuffer.h"
#include "llvm/Support/Path.h"
#include "llvm/Support/raw_ostream.h"
#include "llvm/Support/TargetSelect.h"
#include "llvm/Support/Signals.h"
#include <dirent.h>
#include <signal.h>
#include <unistd.h>
#include <sys/stat.h>
#include <sys/wait.h>
#include <cerrno>
#include <ctime>
#include <fstream>
#include <iomanip>
#include <iterator>
#include <sstream>

Include dependency graph for main.cpp:

Classes
class	KleeHandler

Namespaces
namespace	klee

Macros
#define	NELEMS(array) (sizeof(array)/sizeof(array[0]))

Functions
static std::string	strip (std::string &in)

static void	parseArguments (int argc, char **argv)

static void	preparePOSIX (std::vector< std::unique_ptr< llvm::Module > > &loadedModules, llvm::StringRef libCPrefix)

void	externalsAndGlobalsCheck (const llvm::Module *m)

void	halt_execution ()

void	stop_forking ()

static void	interrupt_handle ()

static void	interrupt_handle_watchdog ()

static void	halt_via_gdb (int pid)

static void	linkWithUclibc (StringRef libDir, std::string opt_suffix, std::vector< std::unique_ptr< llvm::Module > > &modules)

int	main (int argc, char argv, char envp)

Variables
cl::opt< std::string >	klee::MaxTime

static const char *	modelledExternals []

static const char *	dontCareExternals []

static const char *	dontCareKlee []

static const char *	dontCareUclibc []

static const char *	unsafeExternals []

static Interpreter *	theInterpreter = 0

static bool	interrupted = false

Macro Definition Documentation

◆ NELEMS

#define NELEMS ( array ) (sizeof(array)/sizeof(array[0]))

Definition at line 889 of file main.cpp.

Function Documentation

◆ externalsAndGlobalsCheck()

void externalsAndGlobalsCheck ( const llvm::Module * m )

Definition at line 890 of file main.cpp.

References dontCareExternals, dontCareKlee, dontCareUclibc, klee::floats::ext(), klee_warning(), klee_warning_once(), modelledExternals, NELEMS, and unsafeExternals.

Referenced by main().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ halt_execution()

void halt_execution ( )

Definition at line 988 of file main.cpp.

References klee::Interpreter::setHaltExecution(), and theInterpreter.

Referenced by interrupt_handle().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ halt_via_gdb()

static void halt_via_gdb ( int pid )

static

Definition at line 1018 of file main.cpp.

Referenced by main().

Here is the caller graph for this function:

◆ interrupt_handle()

static void interrupt_handle ( )

static

Definition at line 997 of file main.cpp.

References halt_execution(), interrupt_handle(), interrupted, and theInterpreter.

Referenced by interrupt_handle(), and main().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ interrupt_handle_watchdog()

static void interrupt_handle_watchdog ( )

static

Definition at line 1009 of file main.cpp.

Referenced by main().

Here is the caller graph for this function:

◆ linkWithUclibc()

static void linkWithUclibc	(	StringRef	libDir,
		std::string	opt_suffix,
		std::vector< std::unique_ptr< llvm::Module > > &	modules
	)

static

Definition at line 1031 of file main.cpp.

References klee::klee_error().

Referenced by main().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ main()

int main	(	int	argc,
		char **	argv,
		char **	envp
	)

Definition at line 1154 of file main.cpp.

References KTest::args, externalsAndGlobalsCheck(), klee::stats::forks, klee::time::getClockInfo(), KleeHandler::getInfoStream(), KleeHandler::getKTestFilesInDir(), KleeHandler::getNumPathsCompleted(), KleeHandler::getNumPathsExplored(), KleeHandler::getNumTestCases(), KleeHandler::getRunTimeLibraryPath(), klee::StatisticManager::getStatisticByName(), klee::time::getWallTime(), halt_via_gdb(), klee::stats::instructions, interrupt_handle(), interrupt_handle_watchdog(), interrupted, klee::klee_error(), klee::klee_message(), klee_warning(), kTest_free(), kTest_fromFile(), kTest_numBytes(), klee::Interpreter::ModuleOptions::LibraryDir, line, klee::linkModules(), linkWithUclibc(), klee::loadFile(), KleeHandler::loadPathFile(), klee::Interpreter::InterpreterOptions::MakeConcreteSymbolic, klee::MaxTime, KTest::numArgs, parseArguments(), preparePOSIX(), klee::stats::queries, klee::stats::queriesInvalid, klee::stats::queriesValid, klee::stats::queryConstructs, klee::stats::queryCounterexamples, klee::Interpreter::runFunctionAsMain(), klee::time::seconds(), KleeHandler::setInterpreter(), klee::Interpreter::setModule(), klee::Interpreter::setReplayKTest(), klee::Interpreter::setReplayPath(), strip(), theInterpreter, klee::theStatisticManager, klee::time::Span::toHMS(), and klee::Interpreter::useSeeds().

Here is the call graph for this function:

◆ parseArguments()

static void parseArguments	(	int	argc,
		char **	argv
	)

static

Definition at line 693 of file main.cpp.

References klee::printVersion().

Referenced by main().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ preparePOSIX()

static void preparePOSIX	(	std::vector< std::unique_ptr< llvm::Module > > &	loadedModules,
		llvm::StringRef	libCPrefix
	)

static

Definition at line 700 of file main.cpp.

References klee::klee_error().

Referenced by main().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ stop_forking()

void stop_forking ( )

Definition at line 993 of file main.cpp.

References klee::Interpreter::setInhibitForking(), and theInterpreter.

Here is the call graph for this function:

◆ strip()

static std::string strip ( std::string & in )

static

Definition at line 683 of file main.cpp.

Referenced by main().

Here is the caller graph for this function:

Variable Documentation

◆ dontCareExternals

const char* dontCareExternals[]

static

Definition at line 810 of file main.cpp.

Referenced by externalsAndGlobalsCheck().

◆ dontCareKlee

const char* dontCareKlee[]

static

Initial value:

= {
  "__ctype_b_loc",
  "__ctype_get_mb_cur_max",
 
  
  "open",
  "write",
  "read",
  "close",
}

Definition at line 859 of file main.cpp.

Referenced by externalsAndGlobalsCheck().

◆ dontCareUclibc

const char* dontCareUclibc[]

static

Initial value:

= {
  "__dso_handle",
 
  
  
  "printf",
  "vprintf"
}

Definition at line 871 of file main.cpp.

Referenced by externalsAndGlobalsCheck().

◆ interrupted

bool interrupted = false

static

Definition at line 984 of file main.cpp.

Referenced by interrupt_handle(), and main().

◆ modelledExternals

const char* modelledExternals[]

static

Definition at line 743 of file main.cpp.

Referenced by externalsAndGlobalsCheck().

◆ theInterpreter

Interpreter* theInterpreter = 0

static

Definition at line 982 of file main.cpp.

Referenced by halt_execution(), interrupt_handle(), main(), and stop_forking().

◆ unsafeExternals

const char* unsafeExternals[]

static

Initial value:

= {
  "fork", 
  "exec", 
  "error", 
  "raise", 
  "kill", 
}

Definition at line 881 of file main.cpp.

Referenced by externalsAndGlobalsCheck().

Classes

Namespaces

Macros

Functions

Variables

Macro Definition Documentation

◆ NELEMS

Function Documentation

◆ externalsAndGlobalsCheck()

◆ halt_execution()

◆ halt_via_gdb()

◆ interrupt_handle()

◆ interrupt_handle_watchdog()

◆ linkWithUclibc()

◆ main()

◆ parseArguments()

◆ preparePOSIX()

◆ stop_forking()

◆ strip()

Variable Documentation

◆ dontCareExternals

◆ dontCareKlee

◆ dontCareUclibc

◆ interrupted

◆ modelledExternals

◆ theInterpreter

◆ unsafeExternals