CBMC
pointer_offset_size.h File Reference

Pointer Logic. More...

#include "irep.h"
#include "mp_arith.h"
#include <optional>
+ Include dependency graph for pointer_offset_size.h:

Go to the source code of this file.

Functions

std::optional< mp_integermember_offset (const struct_typet &type, const irep_idt &member, const namespacet &ns)
 
std::optional< mp_integermember_offset_bits (const struct_typet &type, const irep_idt &member, const namespacet &ns)
 
std::optional< mp_integerpointer_offset_size (const typet &type, const namespacet &ns)
 Compute the size of a type in bytes, rounding up to full bytes. More...
 
std::optional< mp_integerpointer_offset_bits (const typet &type, const namespacet &ns)
 
std::optional< mp_integercompute_pointer_offset (const exprt &expr, const namespacet &ns)
 
std::optional< exprtmember_offset_expr (const member_exprt &, const namespacet &ns)
 
std::optional< exprtmember_offset_expr (const struct_typet &type, const irep_idt &member, const namespacet &ns)
 
std::optional< exprtsize_of_expr (const typet &type, const namespacet &ns)
 
std::optional< exprtget_subexpression_at_offset (const exprt &expr, const mp_integer &offset, const typet &target_type, const namespacet &ns)
 
std::optional< exprtget_subexpression_at_offset (const exprt &expr, const exprt &offset, const typet &target_type, const namespacet &ns)
 

Detailed Description

Pointer Logic.

Definition in file pointer_offset_size.h.

Function Documentation

◆ compute_pointer_offset()

std::optional<mp_integer> compute_pointer_offset ( const exprt expr,
const namespacet ns 
)

Definition at line 508 of file pointer_offset_size.cpp.

◆ get_subexpression_at_offset() [1/2]

std::optional<exprt> get_subexpression_at_offset ( const exprt expr,
const exprt offset,
const typet target_type,
const namespacet ns 
)

Definition at line 692 of file pointer_offset_size.cpp.

◆ get_subexpression_at_offset() [2/2]

std::optional<exprt> get_subexpression_at_offset ( const exprt expr,
const mp_integer offset,
const typet target_type,
const namespacet ns 
)

Definition at line 569 of file pointer_offset_size.cpp.

◆ member_offset()

std::optional<mp_integer> member_offset ( const struct_typet type,
const irep_idt member,
const namespacet ns 
)

Definition at line 25 of file pointer_offset_size.cpp.

◆ member_offset_bits()

std::optional<mp_integer> member_offset_bits ( const struct_typet type,
const irep_idt member,
const namespacet ns 
)

Definition at line 66 of file pointer_offset_size.cpp.

◆ member_offset_expr() [1/2]

std::optional<exprt> member_offset_expr ( const member_exprt member_expr,
const namespacet ns 
)

Definition at line 222 of file pointer_offset_size.cpp.

◆ member_offset_expr() [2/2]

std::optional<exprt> member_offset_expr ( const struct_typet type,
const irep_idt member,
const namespacet ns 
)

Definition at line 235 of file pointer_offset_size.cpp.

◆ pointer_offset_bits()

std::optional<mp_integer> pointer_offset_bits ( const typet type,
const namespacet ns 
)

Definition at line 102 of file pointer_offset_size.cpp.

◆ pointer_offset_size()

std::optional<mp_integer> pointer_offset_size ( const typet type,
const namespacet ns 
)

Compute the size of a type in bytes, rounding up to full bytes.

Definition at line 91 of file pointer_offset_size.cpp.

◆ size_of_expr()

std::optional<exprt> size_of_expr ( const typet type,
const namespacet ns 
)

Definition at line 281 of file pointer_offset_size.cpp.