Add support for function-local analysis to goto-analyser

Author: martin

src/goto-analyzer/build_analyzer.cpp

@@ -40,7 +40,8 @@ std::unique_ptr<ai_baset> 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<ai_history_factory_baset> hf = nullptr;
@@ -112,6 +113,11 @@ std::unique_ptr<ai_baset> build_analyzer(
             std::move(hf), std::move(df), std::move(st), mh);
         }
       }
+      else if(options.get_bool_option("local"))
+      {
+        return util_make_unique<ai_localt>(
+          std::move(hf), std::move(df), std::move(st), mh);
+      }
     }
   }
   else if(options.get_bool_option("legacy-ait"))

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -195,6 +195,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);
@@ -710,6 +712,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"

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -116,7 +116,8 @@ class optionst;
   "(recursive-interprocedural)" \
   "(three-way-merge)" \
   "(legacy-ait)" \
-  "(legacy-concurrent)"
+  "(legacy-concurrent)" \
+  "(local)"
 
 #define GOTO_ANALYSER_OPTIONS_HISTORY \
   "(ahistorical)" \