From cd97e2169f2da84d02e9ca40c3010422c8d51563 Mon Sep 17 00:00:00 2001
From: Martin Brain <martin.brain@city.ac.uk>
Date: Fri, 18 Nov 2022 18:37:18 +0000
Subject: [PATCH] Add support for function-local analysis to goto-analyser

---
 src/goto-analyzer/build_analyzer.cpp              | 8 +++++++-
 src/goto-analyzer/goto_analyzer_parse_options.cpp | 3 +++
 src/goto-analyzer/goto_analyzer_parse_options.h   | 3 ++-
 3 files changed, 12 insertions(+), 2 deletions(-)

diff --git a/src/goto-analyzer/build_analyzer.cpp b/src/goto-analyzer/build_analyzer.cpp
index 9d9e44e318a6..f22c97834a43 100644
--- a/src/goto-analyzer/build_analyzer.cpp
+++ b/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"))
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index 840621d0baf0..60611377dc32 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);
@@ -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"
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)" \