Expose conversion of properties of a goto-program into a JSON array

so that it can be reused to goto-diff

Author: peterschrammel

src/goto-programs/show_properties.cpp

@@ -108,8 +108,7 @@ void show_properties(
   }
 }
 
-
-void show_properties_json(
+void convert_properties_json(
   json_arrayt &json_properties,
   const namespacet &ns,
   const irep_idt &identifier,
@@ -155,11 +154,7 @@ void show_properties_json(
 
   for(const auto &fct : goto_functions.function_map)
     if(!fct.second.is_inlined())
-      show_properties_json(
-        json_properties,
-        ns,
-        fct.first,
-        fct.second.body);
+      convert_properties_json(json_properties, ns, fct.first, fct.second.body);
 
   json_objectt json_result;
   json_result["properties"] = json_properties;

src/goto-programs/show_properties.h

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 class namespacet;
 class goto_modelt;
 class symbol_tablet;
+class goto_programt;
 class goto_functionst;
 class message_handlert;
 
@@ -43,4 +44,15 @@ optionalt<source_locationt> find_property(
     const irep_idt &property,
     const goto_functionst &goto_functions);
 
+/// \brief Collects the properties in the goto program into a `json_arrayt`
+/// \param json_properties: JSON array to hold the properties
+/// \param ns: namespace
+/// \param identifier: function id of the goto program
+/// \param goto_program: the goto program
+void convert_properties_json(
+  json_arrayt &json_properties,
+  const namespacet &ns,
+  const irep_idt &identifier,
+  const goto_programt &goto_program);
+
 #endif // CPROVER_GOTO_PROGRAMS_SHOW_PROPERTIES_H