--vsd-union top-bottom

Author: jezhiggins

src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp

@@ -52,6 +52,13 @@ vsd_configt vsd_configt::from_options(const optionst &options)
     ARRAY_INSENSITIVE
   );
 
+  config.union_abstract_type = option_to_abstract_type(
+    options,
+    "unions",
+    union_option_mappings,
+    UNION_INSENSITIVE
+  );
+
   // This should always be on (for efficeny with 3-way merge)
   // Does not work with value set
   config.context_tracking.last_write_context =
@@ -119,6 +126,10 @@ const vsd_configt::option_mappingt vsd_configt::array_option_mappings = {
   { "every-element", ARRAY_SENSITIVE }
 };
 
+const vsd_configt::option_mappingt vsd_configt::union_option_mappings = {
+  { "top-bottom", UNION_INSENSITIVE }
+};
+
 invalid_command_line_argument_exceptiont vsd_configt::invalid_argument(
   const std::string& option_name,
   const std::string& bad_argument,
@@ -262,7 +273,7 @@ variable_sensitivity_object_factoryt::get_abstract_object_type(const typet& type
   }
   else if(type.id() == ID_union)
   {
-    abstract_object_type = UNION_INSENSITIVE;
+    return configuration.union_abstract_type;
   }
 
   return abstract_object_type;

src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h

@@ -53,6 +53,7 @@ struct vsd_configt
   ABSTRACT_OBJECT_TYPET pointer_abstract_type;
   ABSTRACT_OBJECT_TYPET struct_abstract_type;
   ABSTRACT_OBJECT_TYPET array_abstract_type;
+  ABSTRACT_OBJECT_TYPET union_abstract_type;
 
   struct
   {
@@ -91,6 +92,7 @@ struct vsd_configt
   static const option_mappingt pointer_option_mappings;
   static const option_mappingt struct_option_mappings;
   static const option_mappingt array_option_mappings;
+  static const option_mappingt union_option_mappings;
 };
 
 class variable_sensitivity_object_factoryt;

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -372,6 +372,7 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
       options.set_option("pointers", cmdline.get_value("vsd-pointers"));
       options.set_option("arrays", cmdline.get_value("vsd-arrays"));
       options.set_option("structs", cmdline.get_value("vsd-structs"));
+      options.set_option("unions", cmdline.get_value("vsd-unions"));
       options.set_option(
         "data-dependencies", cmdline.isset("vsd-data-dependencies"));
     }
@@ -385,6 +386,7 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
       options.set_option("pointers", cmdline.get_value("vsd-pointers"));
       options.set_option("arrays", cmdline.get_value("vsd-arrays"));
       options.set_option("structs", cmdline.get_value("vsd-structs"));
+      options.set_option("unions", cmdline.get_value("vsd-unions"));
       options.set_option("data-dependencies", true);
     }
 
@@ -995,6 +997,7 @@ void goto_analyzer_parse_optionst::help()
     " --vsd-structs                struct field sensitive analysis - top-bottom|every-field\n"
     " --vsd-arrays                 array entry sensitive analysis - top-bottom|every-element\n"
     " --vsd-pointers               pointer sensitive analysis - top-bottom|constants|value-set\n"
+    " --vsd-unions                 union sensitive analysis - top-bottom\n"
     " --vsd-data-dependencies      track data dependencies\n"
     "\n"
     "Storage options:\n"

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -139,6 +139,7 @@ class optionst;
   "(vsd-structs):" \
   "(vsd-arrays):" \
   "(vsd-pointers):" \
+  "(vsd-unions):" \
   "(vsd-data-dependencies)"
 
 #define GOTO_ANALYSER_OPTIONS_STORAGE \