require_goto_statements::pointer_assignment_locationt Struct Reference

#include <require_goto_statements.h>

Collaboration diagram for require_goto_statements::pointer_assignment_locationt:

Public Attributes
std::optional< code_assignt >	null_assignment
std::vector< code_assignt >	non_null_assignments

Detailed Description

Definition at line 24 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 27 of file require_goto_statements.h.

null_assignment

std::optional<code_assignt> require_goto_statements::pointer_assignment_locationt::null_assignment

Definition at line 26 of file require_goto_statements.h.

---

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

• /home/runner/work/cbmc/cbmc/jbmc/unit/java-testing-utils/require_goto_statements.h