Merge pull request #1586 from polgreen/get_source_location_for_property

Find source location from a property irep_idt

Author: tautschnig

src/goto-programs/show_properties.cpp

@@ -23,6 +23,30 @@ Author: Daniel Kroening, [email protected]
 #include "goto_functions.h"
 #include "goto_model.h"
 
+
+optionalt<source_locationt> find_property(
+    const irep_idt &property,
+    const goto_functionst & goto_functions)
+{
+  for(const auto &fct : goto_functions.function_map)
+  {
+    const goto_programt &goto_program = fct.second.body;
+
+    for(const auto &ins : goto_program.instructions)
+    {
+      if(ins.is_assert())
+      {
+        if(ins.source_location.get_property_id() == property)
+        {
+          return ins.source_location;
+        }
+      }
+    }
+  }
+  return { };
+}
+
+
 void show_properties(
   const namespacet &ns,
   const irep_idt &identifier,

src/goto-programs/show_properties.h

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_GOTO_PROGRAMS_SHOW_PROPERTIES_H
 
 #include <util/ui_message.h>
+#include <util/optional.h>
 
 class namespacet;
 class goto_modelt;
@@ -28,4 +29,15 @@ void show_properties(
   ui_message_handlert::uit ui,
   const goto_functionst &goto_functions);
 
+/// \brief Returns a source_locationt that corresponds
+/// to the property given by an irep_idt.
+/// \param property irep_idt that identifies property
+/// \param goto_functions  program in which to search for
+///   the property
+/// \return optional<source_locationt> the location of the
+/// property, if found.
+optionalt<source_locationt> find_property(
+    const irep_idt &property,
+    const goto_functionst &goto_functions);
+
 #endif // CPROVER_GOTO_PROGRAMS_SHOW_PROPERTIES_H