diff --git a/src/goto-analyzer/build_analyzer.cpp b/src/goto-analyzer/build_analyzer.cpp index 194a91eeed5e..92ea78997db3 100644 --- a/src/goto-analyzer/build_analyzer.cpp +++ b/src/goto-analyzer/build_analyzer.cpp @@ -40,7 +40,8 @@ std::unique_ptr build_analyzer( // These support all of the option categories if( options.get_bool_option("recursive-interprocedural") || - options.get_bool_option("three-way-merge")) + options.get_bool_option("three-way-merge") || + options.get_bool_option("local") ||) { // Build the history factory std::unique_ptr hf = nullptr; @@ -112,6 +113,11 @@ std::unique_ptr build_analyzer( std::move(hf), std::move(df), std::move(st), mh); } } + else if(options.get_bool_option("local")) + { + return util_make_unique( + std::move(hf), std::move(df), std::move(st), mh); + } } } else if(options.get_bool_option("legacy-ait")) diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index efeedbc66db1..d7f722b1f5f9 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -192,6 +192,8 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) options.set_option("recursive-interprocedural", true); else if(cmdline.isset("three-way-merge")) options.set_option("three-way-merge", true); + else if(cmdline.isset("local")) + options.set_option("local", true); else if(cmdline.isset("legacy-ait") || cmdline.isset("location-sensitive")) { options.set_option("legacy-ait", true); @@ -715,6 +717,8 @@ void goto_analyzer_parse_optionst::help() // NOLINTNEXTLINE(whitespace/line_length) " --three-way-merge use VSD's three-way merge on return from function call\n" // NOLINTNEXTLINE(whitespace/line_length) + " --local perform function-local analysis for every function\n" + // NOLINTNEXTLINE(whitespace/line_length) " --legacy-ait recursion for function and one domain per location\n" // NOLINTNEXTLINE(whitespace/line_length) " --legacy-concurrent legacy-ait with an extended fixed-point for concurrency\n" diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index beda0d3a2d37..8d3ca607d831 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -115,7 +115,8 @@ class optionst; "(recursive-interprocedural)" \ "(three-way-merge)" \ "(legacy-ait)" \ - "(legacy-concurrent)" + "(legacy-concurrent)" \ + "(local)" #define GOTO_ANALYSER_OPTIONS_HISTORY \ "(ahistorical)" \