CBMC: /home/runner/work/cbmc/cbmc/src/goto-programs/xml_goto_trace.cpp File Reference

CBMC

Loading...

Searching...

No Matches

xml_goto_trace.cpp File Reference

Traces of GOTO Programs. More...

#include "xml_goto_trace.h"
#include <util/arith_tools.h>
#include <util/bitvector_types.h>
#include <util/namespace.h>
#include <util/string_constant.h>
#include <util/symbol.h>
#include <util/xml_irep.h>
#include <ansi-c/printf_formatter.h>
#include <langapi/language_util.h>
#include "goto_trace.h"
#include "structured_trace_util.h"
#include "xml_expr.h"

+ Include dependency graph for xml_goto_trace.cpp:

Go to the source code of this file.

Functions

static void replace_string_constants_rec (exprt &expr)

Rewrite all string constants to their array counterparts.

static std::string get_printable_xml (const namespacet &ns, const irep_idt &id, const exprt &expr)

Given an expression expr, produce a string representation that is printable in XML 1.0.

xmlt full_lhs_value (const goto_trace_stept &step, const namespacet &ns)

void convert (const namespacet &ns, const goto_tracet &goto_trace, xmlt &dest)

Detailed Description

Traces of GOTO Programs.

Definition in file xml_goto_trace.cpp.

Function Documentation

◆ convert()

void convert ( const namespacet & ns,

const goto_tracet & goto_trace,

xmlt & dest

)

Definition at line 92 of file xml_goto_trace.cpp.

◆ full_lhs_value()

xmlt full_lhs_value ( const goto_trace_stept & step,

const namespacet & ns

)

Definition at line 62 of file xml_goto_trace.cpp.

◆ get_printable_xml()

static std::string get_printable_xml ( const namespacet & ns,

const irep_idt & id,

const exprt & expr

)

static

Given an expression expr, produce a string representation that is printable in XML 1.0.

Produces an empty string if no valid XML 1.0 string representing expr can be generated.

Definition at line 44 of file xml_goto_trace.cpp.

◆ replace_string_constants_rec()

static void replace_string_constants_rec ( exprt & expr )

static

Rewrite all string constants to their array counterparts.

Definition at line 31 of file xml_goto_trace.cpp.