Loading...

Searching...

No Matches

Classes | Macros | Enumerations | Functions

goto_program.h File Reference

Concrete Goto Program. More...

#include <util/invariant.h>
#include <util/source_location.h>
#include "goto_instruction_code.h"
#include <limits>
#include <list>
#include <set>
#include <string>

+ Include dependency graph for goto_program.h:

[フレーム]

Go to the source code of this file.

Classes

class goto_programt

A generic container class for the GOTO intermediate representation of one function. More...

class goto_programt::instructiont

This class represents an instruction in the GOTO intermediate representation. More...

struct goto_programt::instructiont::target_less_than

A total order over targett and const_targett. More...

struct const_target_hash

struct pointee_address_equalt

Functor to check whether iterators from different collections point at the same object. More...

Macros

#define forall_goto_program_instructions(it, program)

#define Forall_goto_program_instructions(it, program)

Enumerations

enum goto_program_instruction_typet {
  NO_INSTRUCTION_TYPE = 0 , GOTO = 1 , ASSUME = 2 , ASSERT = 3 ,
  OTHER = 4 , SKIP = 5 , START_THREAD = 6 , END_THREAD = 7 ,
  LOCATION = 8 , END_FUNCTION = 9 , ATOMIC_BEGIN = 10 , ATOMIC_END = 11 ,
  SET_RETURN_VALUE = 12 , ASSIGN = 13 , DECL = 14 , DEAD = 15 ,
  FUNCTION_CALL = 16 , THROW = 17 , CATCH = 18 , INCOMPLETE_GOTO = 19
}

The type of an instruction in a GOTO program. More...

Functions

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

Outputs a string representation of a goto_program_instruction_typet

template<typename GotoFunctionT , typename PredicateT , typename HandlerT >

void for_each_instruction_if (GotoFunctionT &&goto_function, PredicateT predicate, HandlerT handler)

template<typename GotoFunctionT , typename HandlerT >

void for_each_instruction (GotoFunctionT &&goto_function, HandlerT handler)

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

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

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

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

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

Detailed Description

Concrete Goto Program.

Definition in file goto_program.h.

Macro Definition Documentation

◆ forall_goto_program_instructions

#define forall_goto_program_instructions ( it,

program

)

Value:

for(goto_programt::instructionst::const_iterator \

it=(program).instructions.begin(); \

it!=(program).instructions.end(); it++)

Definition at line 1228 of file goto_program.h.

◆ Forall_goto_program_instructions

#define Forall_goto_program_instructions ( it,

program

)

Value:

for(goto_programt::instructionst::iterator \

it=(program).instructions.begin(); \

it!=(program).instructions.end(); it++)

Definition at line 1233 of file goto_program.h.

Enumeration Type Documentation

◆ goto_program_instruction_typet

enum goto_program_instruction_typet

The type of an instruction in a GOTO program.

Enumerator
NO_INSTRUCTION_TYPE
GOTO
ASSUME
ASSERT
OTHER
SKIP
START_THREAD
END_THREAD
LOCATION
END_FUNCTION
ATOMIC_BEGIN
ATOMIC_END
SET_RETURN_VALUE
ASSIGN
DECL
DEAD
FUNCTION_CALL
THROW
CATCH
INCOMPLETE_GOTO

Definition at line 30 of file goto_program.h.

Function Documentation

◆ as_string()

std::string as_string ( const namespacet & ns,

const irep_idt & function,

const goto_programt::instructiont &

)

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

◆ for_each_instruction()

template<typename GotoFunctionT , typename HandlerT >

void for_each_instruction ( GotoFunctionT && goto_function,

HandlerT handler

)

Definition at line 1221 of file goto_program.h.

◆ for_each_instruction_if()

template<typename GotoFunctionT , typename PredicateT , typename HandlerT >

void for_each_instruction_if ( GotoFunctionT && goto_function,

PredicateT predicate,

HandlerT handler

)

Definition at line 1205 of file goto_program.h.

◆ objects_read()

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

Definition at line 475 of file goto_program.cpp.

◆ objects_written()

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.