CBMC
Static Public Member Functions | List of all members
array_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 165 of file abstract_aggregate_object.h.

Member Function Documentation

◆ ACCESS_EXPR_ID()

static const irep_idt array_aggregate_typet::ACCESS_EXPR_ID ( )
inlinestatic

Definition at line 171 of file abstract_aggregate_object.h.

◆ get_statistics()

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

Definition at line 181 of file abstract_aggregate_object.h.

◆ read_type()

static typet array_aggregate_typet::read_type ( const typet &  ,
const typet &  object_type 
)
inlinestatic

Definition at line 175 of file abstract_aggregate_object.h.

◆ TYPE_ID()

static const irep_idt array_aggregate_typet::TYPE_ID ( )
inlinestatic

Definition at line 167 of file abstract_aggregate_object.h.

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