CBMC
Public Types | Public Member Functions | Public Attributes | Protected Attributes | List of all members
goto_functiont Class Reference

A goto function, consisting of function body (see body) and parameter identifiers (see parameter_identifiers). More...

#include <goto_function.h>

+ Collaboration diagram for goto_functiont:

Public Types

typedef std::vector< irep_idt > parameter_identifierst
 

Public Member Functions

bool body_available () const
 
void set_parameter_identifiers (const code_typet &code_type)
 
bool is_hidden () const
 
void make_hidden ()
 
 goto_functiont ()
 
void clear ()
 
void swap (goto_functiont &other)
 
void copy_from (const goto_functiont &other)
 
 goto_functiont (const goto_functiont &)=delete
 
goto_functiont & operator= (const goto_functiont &)=delete
 
 goto_functiont (goto_functiont &&other)
 
goto_functiont & operator= (goto_functiont &&other)
 
void validate (const namespacet &ns, const validation_modet vm) const
 Check that the goto function is well-formed. More...
 

Public Attributes

goto_programt body
 
parameter_identifierst parameter_identifiers
 The identifiers of the parameters of this function. More...
 

Protected Attributes

bool function_is_hidden
 

Detailed Description

A goto function, consisting of function body (see body) and parameter identifiers (see parameter_identifiers).

Definition at line 23 of file goto_function.h.

Member Typedef Documentation

◆ parameter_identifierst

typedef std::vector<irep_idt> goto_functiont::parameter_identifierst

Definition at line 28 of file goto_function.h.

Constructor & Destructor Documentation

◆ goto_functiont() [1/3]

goto_functiont::goto_functiont ( )
inline

Definition at line 58 of file goto_function.h.

◆ goto_functiont() [2/3]

goto_functiont::goto_functiont ( const goto_functiont &  )
delete

◆ goto_functiont() [3/3]

goto_functiont::goto_functiont ( goto_functiont &&  other)
inline

Definition at line 86 of file goto_function.h.

Member Function Documentation

◆ body_available()

bool goto_functiont::body_available ( ) const
inline

Definition at line 35 of file goto_function.h.

◆ clear()

void goto_functiont::clear ( void  )
inline

Definition at line 62 of file goto_function.h.

◆ copy_from()

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

Definition at line 76 of file goto_function.h.

◆ is_hidden()

bool goto_functiont::is_hidden ( ) const
inline

Definition at line 48 of file goto_function.h.

◆ make_hidden()

void goto_functiont::make_hidden ( )
inline

Definition at line 53 of file goto_function.h.

◆ operator=() [1/2]

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

◆ operator=() [2/2]

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

Definition at line 93 of file goto_function.h.

◆ set_parameter_identifiers()

void goto_functiont::set_parameter_identifiers ( const code_typet &  code_type)
inline

Definition at line 40 of file goto_function.h.

◆ swap()

void goto_functiont::swap ( goto_functiont &  other)
inline

Definition at line 69 of file goto_function.h.

◆ validate()

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

Check that the goto function is well-formed.

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

Definition at line 39 of file goto_function.cpp.

Member Data Documentation

◆ body

goto_programt goto_functiont::body

Definition at line 26 of file goto_function.h.

◆ function_is_hidden

bool goto_functiont::function_is_hidden
protected

Definition at line 108 of file goto_function.h.

◆ parameter_identifiers

parameter_identifierst goto_functiont::parameter_identifiers

The identifiers of the parameters of this function.

Note: This is now the preferred way of getting the identifiers of the parameters. The identifiers in the type will go away.

Definition at line 33 of file goto_function.h.

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