CBMC
union_aggregate_typet Struct Reference

#include <abstract_aggregate_object.h>

Static Public Member Functions

static const irep_idt TYPE_ID ()
 
static const irep_idt ACCESS_EXPR_ID ()
 
static typet read_type (const typet &, const typet &object_type)
 
static void get_statistics (abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns)
 

Detailed Description

Definition at line 216 of file abstract_aggregate_object.h.

Member Function Documentation

◆ ACCESS_EXPR_ID()

static const irep_idt union_aggregate_typet::ACCESS_EXPR_ID ( )
inlinestatic

Definition at line 222 of file abstract_aggregate_object.h.

◆ get_statistics()

static void union_aggregate_typet::get_statistics ( abstract_object_statisticst statistics,
abstract_object_visitedt visited,
const abstract_environmentt env,
const namespacet ns 
)
inlinestatic

Definition at line 231 of file abstract_aggregate_object.h.

◆ read_type()

static typet union_aggregate_typet::read_type ( const typet ,
const typet object_type 
)
inlinestatic

Definition at line 226 of file abstract_aggregate_object.h.

◆ TYPE_ID()

static const irep_idt union_aggregate_typet::TYPE_ID ( )
inlinestatic

Definition at line 218 of file abstract_aggregate_object.h.


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