Home Original page

CBMC: goto_functiont Class Reference

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

#include <goto_function.h>

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.
 

Public Attributes

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

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

Definition at line 23 of file goto_function.h.

◆ parameter_identifierst

goto_functiont::goto_functiont ( )
inline

◆ goto_functiont() [2/3]

◆ goto_functiont() [3/3]

◆ body_available()

bool goto_functiont::body_available ( ) const
inline

◆ clear()

void goto_functiont::clear ( )
inline

◆ copy_from()

◆ is_hidden()

bool goto_functiont::is_hidden ( ) const
inline

◆ make_hidden()

void goto_functiont::make_hidden ( )
inline

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ set_parameter_identifiers()

◆ swap()

◆ validate()

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.

◆ body

◆ function_is_hidden

bool goto_functiont::function_is_hidden

 protected

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