CBMC
Public Attributes | List of all members
require_goto_statements::pointer_assignment_locationt Struct Reference

#include <require_goto_statements.h>

+ Collaboration diagram for require_goto_statements::pointer_assignment_locationt:

Public Attributes

optionalt< code_assignt > null_assignment
 
std::vector< code_assignt > non_null_assignments
 

Detailed Description

Definition at line 26 of file require_goto_statements.h.

Member Data Documentation

◆ non_null_assignments

std::vector<code_assignt> require_goto_statements::pointer_assignment_locationt::non_null_assignments

Definition at line 29 of file require_goto_statements.h.

◆ null_assignment

optionalt<code_assignt> require_goto_statements::pointer_assignment_locationt::null_assignment

Definition at line 28 of file require_goto_statements.h.

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