cprover
show_goto_functions_jsont Class Reference

#include <show_goto_functions_json.h>

Collaboration diagram for show_goto_functions_jsont:
[legend]

Public Member Functions

 show_goto_functions_jsont (const namespacet &ns)
 For outputting the GOTO program in a readable JSON format. More...
 
json_objectt convert (const goto_functionst &goto_functions)
 Walks through all of the functions in the program and returns a JSON object representing all their functions. More...
 
void operator() (const goto_functionst &goto_functions, std::ostream &out, bool append=true)
 Print the json object generated by show_goto_functions_jsont::show_goto_functions to the provided stream (e.g. More...
 

Private Attributes

const namespacetns
 

Detailed Description

Definition at line 20 of file show_goto_functions_json.h.

Constructor & Destructor Documentation

◆ show_goto_functions_jsont()

show_goto_functions_jsont::show_goto_functions_jsont ( const namespacet ns)
explicit

For outputting the GOTO program in a readable JSON format.

Parameters
nsthe namespace to use to resolve names with

Definition at line 29 of file show_goto_functions_json.cpp.

Member Function Documentation

◆ convert()

json_objectt show_goto_functions_jsont::convert ( const goto_functionst goto_functions)

Walks through all of the functions in the program and returns a JSON object representing all their functions.

Parameters
goto_functionsthe goto functions that make up the program

Definition at line 36 of file show_goto_functions_json.cpp.

References json_irept::convert_from_irep(), CPROVER_PREFIX, goto_functions_templatet< bodyT >::entry_point(), goto_functions_templatet< bodyT >::function_map, goto_modelt::goto_functions, has_prefix(), id2string(), json(), jsont::json_boolean(), jsont::make_object(), ns, exprt::operands(), and json_arrayt::push_back().

Referenced by operator()().

◆ operator()()

void show_goto_functions_jsont::operator() ( const goto_functionst goto_functions,
std::ostream &  out,
bool  append = true 
)

Print the json object generated by show_goto_functions_jsont::show_goto_functions to the provided stream (e.g.

std::cout)

Parameters
goto_functionsthe goto functions that make up the program
outthe stream to write the object to
appendshould a command and newline be appended to the stream before writing the JSON object. Defaults to true

Definition at line 121 of file show_goto_functions_json.cpp.

References convert(), and goto_modelt::goto_functions.

Member Data Documentation

◆ ns

const namespacet& show_goto_functions_jsont::ns
private

Definition at line 30 of file show_goto_functions_json.h.

Referenced by convert().


The documentation for this class was generated from the following files: