CBMC
show_on_source.cpp File Reference
#include "show_on_source.h"
#include <util/message.h>
#include <util/unicode.h>
#include <analyses/ai.h>
#include <fstream>
+ Include dependency graph for show_on_source.cpp:

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...
 

Function Documentation

◆ get_source_files()

static std::set<std::string> get_source_files ( const goto_modelt goto_model,
const ai_baset ai 
)
static

get the source files with non-top abstract states

Definition at line 35 of file show_on_source.cpp.

◆ print_with_indent()

static void print_with_indent ( const std::string &  src,
const std::string &  indent_line,
std::ostream &  out 
)
static

print a string with indent to match given sample line

Definition at line 53 of file show_on_source.cpp.

◆ show_location()

static std::optional<std::string> show_location ( const ai_baset ai,
ai_baset::locationt  loc 
)
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.

◆ show_on_source() [1/2]

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.

◆ show_on_source() [2/2]

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.