855{
856 int arg_num = 0;
857 int extraArgc = 3;
858 char **arg_value = new char *[argc + extraArgc];
859 for (; arg_num < argc; ++arg_num)
860 {
861 arg_value[arg_num] = argv[arg_num];
862 }
863
864 arg_value[arg_num++] = (char*) "-model-consts=true";
865 arg_value[arg_num++] = (char*) "-model-arrays=true";
866 arg_value[arg_num++] = (char*) "-pre-field-sensitive=false";
867 assert(arg_num == (argc + extraArgc) && "more extra arguments? Change the value of extraArgc");
868
869 std::vector<std::string> moduleNameVec;
871 arg_num, arg_value, "Static Symbolic Execution", "[options] <input-bitcode...>"
872 );
873 delete[] arg_value;
875 {
878 return 0;
879 }
880
882 {
886 return 0;
887 }
888
892
893
898 ae.
addDetector(std::make_unique<BufOverflowDetector>());
900 ae.
addDetector(std::make_unique<NullptrDerefDetector>());
902
905
906 return 0;
907}
static Option< bool > SYMABS("symabs", "symbolic abstraction test", false)
static Option< bool > AETEST("aetest", "abstract execution basic function test", false)
static std::vector< std::string > parseOptions(int argc, char *argv[], std::string description, std::string callFormat)
virtual void runOnModule()
void addDetector(std::unique_ptr< AEDetector > detector)
static AbstractInterpretation & getAEInstance()
static AndersenWaveDiff * createAndersenWaveDiff(SVFIR *_pag)
Create an singleton instance directly instead of invoking llvm pass manager.
static void releaseAndersenWaveDiff()
static LLVMModuleSet * getLLVMModuleSet()
static void releaseLLVMModuleSet()
static void buildSVFModule(Module &mod)
static const Option< bool > NullDerefCheck
nullptr dereference checker, Default: false
static const Option< bool > BufferOverflowCheck
buffer overflow checker, Default: false
CallGraph * getCallGraph() const
Return call graph.
void updateCallGraph(CallGraph *callgraph)
connect PAG edges based on callgraph
virtual SVFIR * build()
Start building SVFIR here.