klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
main.cpp File Reference
#include "../lib/Core/Common.h"
#include "klee/ExecutionState.h"
#include "klee/Expr.h"
#include "klee/Interpreter.h"
#include "klee/Statistics.h"
#include "klee/Config/Version.h"
#include "klee/Internal/ADT/KTest.h"
#include "klee/Internal/ADT/TreeStream.h"
#include "klee/Internal/Support/ModuleUtil.h"
#include "klee/Internal/System/Time.h"
#include "llvm/Constants.h"
#include "llvm/Module.h"
#include "llvm/Type.h"
#include "llvm/InstrTypes.h"
#include "llvm/Instruction.h"
#include "llvm/Instructions.h"
#include "llvm/LLVMContext.h"
#include "llvm/Support/FileSystem.h"
#include "llvm/Bitcode/ReaderWriter.h"
#include "llvm/Support/CommandLine.h"
#include "llvm/Support/Debug.h"
#include "llvm/Support/ManagedStatic.h"
#include "llvm/Support/MemoryBuffer.h"
#include "llvm/Support/raw_ostream.h"
#include "llvm/Support/TargetSelect.h"
#include "llvm/Support/Signals.h"
#include "llvm/Support/system_error.h"
#include <dirent.h>
#include <signal.h>
#include <unistd.h>
#include <sys/stat.h>
#include <sys/wait.h>
#include <cerrno>
#include <fstream>
#include <iomanip>
#include <iterator>
#include <sstream>
Include dependency graph for main.cpp:

Go to the source code of this file.

Classes

class  KleeHandler
 

Macros

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

Enumerations

enum  LibcType
 

Functions

static std::string strip (std::string &in)
 
static void readArgumentsFromFile (char *file, std::vector< std::string > &results)
 
static void parseArguments (int argc, char **argv)
 
static int initEnv (Module *mainModule)
 
void externalsAndGlobalsCheck (const 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 char * format_tdiff (char *buf, long seconds)
 
static llvm::Module * linkWithUclibc (llvm::Module *mainModule, StringRef libDir)
 
int main (int argc, char **argv, char **envp)
 

Variables

cl::opt< double > MaxTime
 
static const char * modelledExternals []
 
static const char * dontCareExternals []
 
static const char * dontCareKlee []
 
static const char * dontCareUclibc []
 
static const char * unsafeExternals []
 
static InterpretertheInterpreter = 0
 
static bool interrupted = false
 

Macro Definition Documentation

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

Definition at line 863 of file main.cpp.

Referenced by externalsAndGlobalsCheck().

Enumeration Type Documentation

enum LibcType

Definition at line 127 of file main.cpp.

Function Documentation

void externalsAndGlobalsCheck ( const Module *  m)

Definition at line 864 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:

static char* format_tdiff ( char *  buf,
long  seconds 
)
static

Definition at line 998 of file main.cpp.

Referenced by main().

Here is the caller graph for this function:

void halt_execution ( )

Definition at line 956 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:

static void halt_via_gdb ( int  pid)
static

Definition at line 986 of file main.cpp.

Referenced by main().

Here is the caller graph for this function:

static int initEnv ( Module *  mainModule)
static

Definition at line 663 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:

static void interrupt_handle ( )
static

Definition at line 965 of file main.cpp.

References halt_execution(), interrupted, and theInterpreter.

Referenced by main().

Here is the call graph for this function:

Here is the caller graph for this function:

static void interrupt_handle_watchdog ( )
static

Definition at line 977 of file main.cpp.

Referenced by main().

Here is the caller graph for this function:

static llvm::Module* linkWithUclibc ( llvm::Module *  mainModule,
StringRef  libDir 
)
static

Definition at line 1013 of file main.cpp.

Referenced by main().

Here is the caller graph for this function:

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

Definition at line 634 of file main.cpp.

References readArgumentsFromFile().

Referenced by main().

Here is the call graph for this function:

Here is the caller graph for this function:

static void readArgumentsFromFile ( char *  file,
std::vector< std::string > &  results 
)
static

Definition at line 621 of file main.cpp.

References line, and strip().

Referenced by parseArguments().

Here is the call graph for this function:

Here is the caller graph for this function:

void stop_forking ( )

Definition at line 961 of file main.cpp.

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

Here is the call graph for this function:

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

Definition at line 611 of file main.cpp.

Referenced by main(), and readArgumentsFromFile().

Here is the caller graph for this function:

Variable Documentation

const char* dontCareExternals[]
static

Definition at line 788 of file main.cpp.

Referenced by externalsAndGlobalsCheck().

const char* dontCareKlee[]
static
Initial value:
= {
"__ctype_b_loc",
"__ctype_get_mb_cur_max",
"open",
"write",
"read",
"close",
}

Definition at line 836 of file main.cpp.

Referenced by externalsAndGlobalsCheck().

const char* dontCareUclibc[]
static
Initial value:
= {
"__dso_handle",
"printf",
"vprintf"
}

Definition at line 847 of file main.cpp.

Referenced by externalsAndGlobalsCheck().

bool interrupted = false
static

Definition at line 952 of file main.cpp.

Referenced by interrupt_handle(), and main().

cl::opt<double> MaxTime

Referenced by main().

const char* modelledExternals[]
static

Definition at line 732 of file main.cpp.

Referenced by externalsAndGlobalsCheck().

Interpreter* theInterpreter = 0
static

Definition at line 950 of file main.cpp.

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

const char* unsafeExternals[]
static
Initial value:
= {
"fork",
"exec",
"error",
"raise",
"kill",
}

Definition at line 856 of file main.cpp.

Referenced by externalsAndGlobalsCheck().