CBMC
Public Member Functions | Public Attributes | List of all members
goto_convertt::clean_expr_resultt Struct Reference

#include <goto_convert_class.h>

+ Collaboration diagram for goto_convertt::clean_expr_resultt:

Public Member Functions

 clean_expr_resultt ()=default
 
void add (clean_expr_resultt &&other)
 
void add_temporary (const irep_idt &id)
 

Public Attributes

std::list< irep_idt > temporaries
 Identifiers of temporaries introduced while cleaning an expression. More...
 
goto_programt side_effects
 Statements implementing side effects of the expression that was subject to cleaning. More...
 

Detailed Description

Definition at line 59 of file goto_convert_class.h.

Constructor & Destructor Documentation

◆ clean_expr_resultt()

goto_convertt::clean_expr_resultt::clean_expr_resultt ( )
default

Member Function Documentation

◆ add()

void goto_convertt::clean_expr_resultt::add ( clean_expr_resultt &&  other)
inline

Definition at line 73 of file goto_convert_class.h.

◆ add_temporary()

void goto_convertt::clean_expr_resultt::add_temporary ( const irep_idt &  id)
inline

Definition at line 79 of file goto_convert_class.h.

Member Data Documentation

◆ side_effects

goto_programt goto_convertt::clean_expr_resultt::side_effects

Statements implementing side effects of the expression that was subject to cleaning.

The caller needs to merge (typically via destructive_append) these statements into the destination GOTO program.

Definition at line 69 of file goto_convert_class.h.

◆ temporaries

std::list<irep_idt> goto_convertt::clean_expr_resultt::temporaries

Identifiers of temporaries introduced while cleaning an expression.

The caller needs to add destructors for these (via destruct_locals) on all control-flow paths as soon as the temporaries are no longer needed.

Definition at line 64 of file goto_convert_class.h.

The documentation for this struct was generated from the following file: