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

CBMC

Loading...

Searching...

No Matches

goto_program.cpp File Reference

Program Transformation. More...

#include "goto_program.h"
#include <util/expr_iterator.h>
#include <util/find_symbols.h>
#include <util/format_expr.h>
#include <util/format_type.h>
#include <util/invariant.h>
#include <util/namespace.h>
#include <util/pointer_expr.h>
#include <util/std_code.h>
#include <util/std_expr.h>
#include <util/symbol.h>
#include <util/validate.h>
#include <langapi/language_util.h>
#include "validate_code.h"
#include <iomanip>
#include <map>

+ Include dependency graph for goto_program.cpp:

Go to the source code of this file.

Functions

void parse_lhs_read (const exprt &src, std::list< exprt > &dest)

std::list< exprt > expressions_read (const goto_programt::instructiont &instruction)

std::list< exprt > expressions_written (const goto_programt::instructiont &instruction)

void objects_read (const exprt &src, std::list< exprt > &dest)

std::list< exprt > objects_read (const goto_programt::instructiont &instruction)

void objects_written (const exprt &src, std::list< exprt > &dest)

std::list< exprt > objects_written (const goto_programt::instructiont &instruction)

std::string as_string (const class namespacet &ns, const irep_idt &function, const goto_programt::instructiont &i)

std::ostream & operator<< (std::ostream &out, goto_program_instruction_typet t)

Outputs a string representation of a goto_program_instruction_typet

Detailed Description

Program Transformation.

Definition in file goto_program.cpp.

Function Documentation

◆ as_string()

std::string as_string ( const class namespacet & ns,

const irep_idt & function,

const goto_programt::instructiont & i

)

Definition at line 515 of file goto_program.cpp.

◆ expressions_read()

std::list< exprt > expressions_read ( const goto_programt::instructiont & instruction )

Definition at line 362 of file goto_program.cpp.

◆ expressions_written()

std::list< exprt > expressions_written ( const goto_programt::instructiont & instruction )

Definition at line 411 of file goto_program.cpp.

◆ objects_read() [1/2]

void objects_read ( const exprt & src,

std::list< exprt > & dest

)

Definition at line 451 of file goto_program.cpp.

◆ objects_read() [2/2]

std::list< exprt > objects_read ( const goto_programt::instructiont & instruction )

Definition at line 475 of file goto_program.cpp.

◆ objects_written() [1/2]

void objects_written ( const exprt & src,

std::list< exprt > & dest

)

Definition at line 488 of file goto_program.cpp.

◆ objects_written() [2/2]

std::list< exprt > objects_written ( const goto_programt::instructiont & instruction )

Definition at line 502 of file goto_program.cpp.

◆ operator<<()

std::ostream & operator<< ( std::ostream & out,

goto_program_instruction_typet t

)

Outputs a string representation of a goto_program_instruction_typet

Definition at line 1172 of file goto_program.cpp.

◆ parse_lhs_read()

void parse_lhs_read ( const exprt & src,

std::list< exprt > & dest

)

Definition at line 337 of file goto_program.cpp.