CBMC
Public Types | Public Member Functions | Static Public Member Functions | Public Attributes | Private Attributes | List of all members
goto_functionst Class Reference

A collection of goto functions. More...

#include <goto_functions.h>

+ Collaboration diagram for goto_functionst:

Public Types

using goto_functiont = ::goto_functiont
 
typedef std::map< irep_idt, goto_functiont > function_mapt
 

Public Member Functions

 goto_functionst ()
 
 goto_functionst (const goto_functionst &)=delete
 
goto_functionst & operator= (const goto_functionst &)=delete
 
 goto_functionst (goto_functionst &&other)
 
goto_functionst & operator= (goto_functionst &&other)
 
std::size_t unload (const irep_idt &name)
 Remove the function named name from the function map, if it exists. More...
 
void clear ()
 
void compute_location_numbers ()
 
void compute_location_numbers (goto_programt &)
 
void compute_loop_numbers ()
 
void compute_target_numbers ()
 
void compute_incoming_edges ()
 
void update ()
 
void swap (goto_functionst &other)
 
void copy_from (const goto_functionst &other)
 
std::vector< function_mapt::const_iterator > sorted () const
 returns a vector of the iterators in alphabetical order More...
 
std::vector< function_mapt::iterator > sorted ()
 returns a vector of the iterators in alphabetical order More...
 
void validate (const namespacet &, validation_modet) const
 Check that the goto functions are well-formed. More...
 

Static Public Member Functions

static irep_idt entry_point ()
 Get the identifier of the entry point to a goto model. More...
 

Public Attributes

function_mapt function_map
 

Private Attributes

unsigned unused_location_number
 A location number such that numbers in the interval [unused_location_number, MAX_UINT] are all unused. More...
 

Detailed Description

A collection of goto functions.

Definition at line 24 of file goto_functions.h.

Member Typedef Documentation

◆ function_mapt

typedef std::map<irep_idt, goto_functiont> goto_functionst::function_mapt

Definition at line 28 of file goto_functions.h.

◆ goto_functiont

using goto_functionst::goto_functiont = ::goto_functiont

Definition at line 27 of file goto_functions.h.

Constructor & Destructor Documentation

◆ goto_functionst() [1/3]

goto_functionst::goto_functionst ( )
inline

Definition at line 40 of file goto_functions.h.

◆ goto_functionst() [2/3]

goto_functionst::goto_functionst ( const goto_functionst &  )
delete

◆ goto_functionst() [3/3]

goto_functionst::goto_functionst ( goto_functionst &&  other)
inline

Definition at line 56 of file goto_functions.h.

Member Function Documentation

◆ clear()

void goto_functionst::clear ( void  )
inline

Definition at line 77 of file goto_functions.h.

◆ compute_incoming_edges()

void goto_functionst::compute_incoming_edges ( )

Definition at line 39 of file goto_functions.cpp.

◆ compute_location_numbers() [1/2]

void goto_functionst::compute_location_numbers ( )

Definition at line 21 of file goto_functions.cpp.

◆ compute_location_numbers() [2/2]

void goto_functionst::compute_location_numbers ( goto_programt &  program)

Definition at line 31 of file goto_functions.cpp.

◆ compute_loop_numbers()

void goto_functionst::compute_loop_numbers ( )

Definition at line 55 of file goto_functions.cpp.

◆ compute_target_numbers()

void goto_functionst::compute_target_numbers ( )

Definition at line 47 of file goto_functions.cpp.

◆ copy_from()

void goto_functionst::copy_from ( const goto_functionst &  other)
inline

Definition at line 108 of file goto_functions.h.

◆ entry_point()

static irep_idt goto_functionst::entry_point ( )
inlinestatic

Get the identifier of the entry point to a goto model.

Definition at line 97 of file goto_functions.h.

◆ operator=() [1/2]

goto_functionst& goto_functionst::operator= ( const goto_functionst &  )
delete

◆ operator=() [2/2]

goto_functionst& goto_functionst::operator= ( goto_functionst &&  other)
inline

Definition at line 62 of file goto_functions.h.

◆ sorted() [1/2]

std::vector< goto_functionst::function_mapt::iterator > goto_functionst::sorted ( )

returns a vector of the iterators in alphabetical order

Definition at line 85 of file goto_functions.cpp.

◆ sorted() [2/2]

std::vector< goto_functionst::function_mapt::const_iterator > goto_functionst::sorted ( ) const

returns a vector of the iterators in alphabetical order

Definition at line 65 of file goto_functions.cpp.

◆ swap()

void goto_functionst::swap ( goto_functionst &  other)
inline

Definition at line 103 of file goto_functions.h.

◆ unload()

std::size_t goto_functionst::unload ( const irep_idt &  name)
inline

Remove the function named name from the function map, if it exists.

Returns
Returns 0 when name was not present, and 1 when name was removed.

Definition at line 72 of file goto_functions.h.

◆ update()

void goto_functionst::update ( )
inline

Definition at line 88 of file goto_functions.h.

◆ validate()

void goto_functionst::validate ( const namespacet &  ns,
validation_modet  vm 
) const

Check that the goto functions are well-formed.

The validation mode indicates whether well-formedness check failures are reported via DATA_INVARIANT violations or exceptions.

Definition at line 104 of file goto_functions.cpp.

Member Data Documentation

◆ function_map

function_mapt goto_functionst::function_map

Definition at line 29 of file goto_functions.h.

◆ unused_location_number

unsigned goto_functionst::unused_location_number
private

A location number such that numbers in the interval [unused_location_number, MAX_UINT] are all unused.

There might still be unused numbers below this. If numbering a new function or renumbering a function, starting from this number is safe.

Definition at line 37 of file goto_functions.h.

The documentation for this class was generated from the following files: