diff --git a/src/goto-programs/show_properties.cpp b/src/goto-programs/show_properties.cpp index 7f0be70cc64..3393923ca75 100644 --- a/src/goto-programs/show_properties.cpp +++ b/src/goto-programs/show_properties.cpp @@ -23,6 +23,30 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_functions.h" #include "goto_model.h" + +optionalt 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, diff --git a/src/goto-programs/show_properties.h b/src/goto-programs/show_properties.h index 0cb0d1c641f..145a195fa8d 100644 --- a/src/goto-programs/show_properties.h +++ b/src/goto-programs/show_properties.h @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_GOTO_PROGRAMS_SHOW_PROPERTIES_H #include +#include 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 the location of the +/// property, if found. +optionalt find_property( + const irep_idt &property, + const goto_functionst &goto_functions); + #endif // CPROVER_GOTO_PROGRAMS_SHOW_PROPERTIES_H