goto_programt::instructiont::loop_contract_datat Struct Reference

#include <goto_program.h>

Public Attributes
std::list< expr2tc >	invariants
std::list< expr2tc >	assigns_targets

Detailed Description

Loop-contract payload (invariants + assigns-clause targets). Only loop_invariant instructions ever carry it, so it lives in a lazily allocated side struct rather than costing 48 bytes (two empty std::lists) on every instruction in the program.

Member Data Documentation

assigns_targets

std::list<expr2tc> goto_programt::instructiont::loop_contract_datat::assigns_targets

invariants

std::list<expr2tc> goto_programt::instructiont::loop_contract_datat::invariants

---

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

• src/goto-programs/goto_program.h