Add support for function-local analysis to goto-analyser

Author: martin-cs

src/goto-analyzer/build_analyzer.cpp

@@ -39,7 +39,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;
@@ -111,6 +112,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

@@ -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);
@@ -716,6 +718,7 @@ void goto_analyzer_parse_optionst::help()
     " reasoning\n"
     " {y--three-way-merge} \t use VSD's three-way merge on return from function"
     " call\n"
+    " {y--local} \t perform function-local analysis for every function\n"
     " {y--legacy-concurrent} \t legacy-ait with an extended fixed-point for"
     " concurrency\n"
     " {y--location-sensitive} \t use location-sensitive abstract interpreter\n"

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)" \