Loading...

Searching...

No Matches

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:

[フレーム]

[legend]

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.

Public Attributes

goto_programt body

parameter_identifierst parameter_identifiers

The identifiers of the parameters of this function.

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 ( )

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:

/home/runner/work/cbmc/cbmc/src/goto-programs/goto_function.h
/home/runner/work/cbmc/cbmc/src/goto-programs/goto_function.cpp