CBMC
|
#include "show_on_source.h"
#include <util/message.h>
#include <util/unicode.h>
#include <analyses/ai.h>
#include <fstream>
Go to the source code of this file.
Functions | |
static std::optional< std::string > | show_location (const ai_baset &ai, ai_baset::locationt loc) |
get the name of the file referred to at a location loc, if any More... | |
static std::set< std::string > | get_source_files (const goto_modelt &goto_model, const ai_baset &ai) |
get the source files with non-top abstract states More... | |
static void | print_with_indent (const std::string &src, const std::string &indent_line, std::ostream &out) |
print a string with indent to match given sample line More... | |
void | show_on_source (const std::string &source_file, const goto_modelt &goto_model, const ai_baset &ai, message_handlert &message_handler) |
output source code annotated with abstract states for given file More... | |
void | show_on_source (const goto_modelt &goto_model, const ai_baset &ai, message_handlert &message_handler) |
output source code annotated with abstract states More... | |
|
static |
get the source files with non-top abstract states
Definition at line 35 of file show_on_source.cpp.
|
static |
print a string with indent to match given sample line
Definition at line 53 of file show_on_source.cpp.
|
static |
get the name of the file referred to at a location loc, if any
Definition at line 21 of file show_on_source.cpp.
void show_on_source | ( | const goto_modelt & | goto_model, |
const ai_baset & | ai, | ||
message_handlert & | message_handler | ||
) |
output source code annotated with abstract states
Definition at line 129 of file show_on_source.cpp.
void show_on_source | ( | const std::string & | source_file, |
const goto_modelt & | goto_model, | ||
const ai_baset & | ai, | ||
message_handlert & | message_handler | ||
) |
output source code annotated with abstract states for given file
Definition at line 68 of file show_on_source.cpp.