CBMC
Loading...
Searching...
No Matches
Public Member Functions | List of all members
codet Class Reference

Data structure for representing an arbitrary statement in a program. More...

#include <std_code_base.h>

+ Inheritance diagram for codet:
[フレーム]
[legend]
+ Collaboration diagram for codet:
[フレーム]
[legend]

Public Member Functions

  codet (const irep_idt &statement)
 
  codet (const irep_idt &statement, source_locationt loc)
 
  codet (const irep_idt &statement, operandst _op)
 
  codet (const irep_idt &statement, operandst op, source_locationt loc)
 
void  set_statement (const irep_idt &statement)
 
const irep_idt &  get_statement () const
 
codet &  first_statement ()
  In the case of a codet type that represents multiple statements, return the first of them.
 
const codet &  first_statement () const
  In the case of a codet type that represents multiple statements, return the first of them.
 
codet &  last_statement ()
  In the case of a codet type that represents multiple statements, return the last of them.
 
const codet &  last_statement () const
  In the case of a codet type that represents multiple statements, return the last of them.
 
exprt &  op0 ()
 
const exprt &  op0 () const
 
exprt &  op1 ()
 
const exprt &  op1 () const
 
exprt &  op2 ()
 
const exprt &  op2 () const
 
exprt &  op3 ()
 
const exprt &  op3 () const
 
- Public Member Functions inherited from exprt
  exprt ()
 
  exprt (const irep_idt &_id)
 
  exprt (irep_idt _id, typet _type)
 
  exprt (irep_idt _id, typet _type, operandst &&_operands)
 
  exprt (const irep_idt &id, typet type, source_locationt loc)
 
typet &  type ()
  Return the type of the expression.
 
const typet &  type () const
 
bool  has_operands () const
  Return true if there is at least one operand.
 
operandst &  operands ()
 
const operandst &  operands () const
 
exprt &  with_source_location (source_locationt location) &
  Add the source location from location, if it is non-nil.
 
exprt &&  with_source_location (source_locationt location) &&
  Add the source location from location, if it is non-nil.
 
exprt &  with_source_location (const exprt &other) &
  Add the source location from other, if it has any.
 
exprt &&  with_source_location (const exprt &other) &&
  Add the source location from other, if it has any.
 
void  reserve_operands (operandst::size_type n)
 
void  copy_to_operands (const exprt &expr)
  Copy the given argument to the end of exprt's operands.
 
void  add_to_operands (const exprt &expr)
  Add the given argument to the end of exprt's operands.
 
void  add_to_operands (exprt &&expr)
  Add the given argument to the end of exprt's operands.
 
void  add_to_operands (exprt &&e1, exprt &&e2)
  Add the given arguments to the end of exprt's operands.
 
void  add_to_operands (exprt &&e1, exprt &&e2, exprt &&e3)
  Add the given arguments to the end of exprt's operands.
 
bool  is_constant () const
  Return whether the expression is a constant.
 
bool  is_true () const
  Return whether the expression is a constant representing true.
 
bool  is_false () const
  Return whether the expression is a constant representing false.
 
bool  is_zero () const
  Return whether the expression is a constant representing 0.
 
bool  is_one () const
  Return whether the expression is a constant representing 1.
 
bool  is_boolean () const
  Return whether the expression represents a Boolean.
 
const source_locationt &  find_source_location () const
  Get a source_locationt from the expression or from its operands (non-recursively).
 
const source_locationt &  source_location () const
 
source_locationt &  add_source_location ()
 
void  drop_source_location ()
 
void  visit (class expr_visitort &visitor)
  These are pre-order traversal visitors, i.e., the visitor is executed on a node before its children have been visited.
 
void  visit (class const_expr_visitort &visitor) const
 
void  visit_pre (std::function< void(exprt &)>)
 
void  visit_pre (std::function< void(const exprt &)>) const
 
void  visit_post (std::function< void(exprt &)>)
  These are post-order traversal visitors, i.e., the visitor is executed on a node after its children have been visited.
 
void  visit_post (std::function< void(const exprt &)>) const
 
depth_iteratort  depth_begin ()
 
depth_iteratort  depth_end ()
 
const_depth_iteratort  depth_begin () const
 
const_depth_iteratort  depth_end () const
 
const_depth_iteratort  depth_cbegin () const
 
const_depth_iteratort  depth_cend () const
 
depth_iteratort  depth_begin (std::function< exprt &()> mutate_root) const
 
const_unique_depth_iteratort  unique_depth_begin () const
 
const_unique_depth_iteratort  unique_depth_end () const
 
const_unique_depth_iteratort  unique_depth_cbegin () const
 
const_unique_depth_iteratort  unique_depth_cend () const
 
- Public Member Functions inherited from irept
bool  is_nil () const
 
bool  is_not_nil () const
 
  irept (const irep_idt &_id)
 
  irept (const irep_idt &_id, const named_subt &_named_sub, const subt &_sub)
 
  irept ()=default
 
const irep_idt &  id () const
 
const std::string &  id_string () const
 
void  id (const irep_idt &_data)
 
const irept &  find (const irep_idt &name) const
 
irept &  add (const irep_idt &name)
 
irept &  add (const irep_idt &name, irept irep)
 
const std::string &  get_string (const irep_idt &name) const
 
const irep_idt &  get (const irep_idt &name) const
 
bool  get_bool (const irep_idt &name) const
 
signed int  get_int (const irep_idt &name) const
 
std::size_t  get_size_t (const irep_idt &name) const
 
long long  get_long_long (const irep_idt &name) const
 
void  set (const irep_idt &name, const irep_idt &value)
 
void  set (const irep_idt &name, irept irep)
 
void  set (const irep_idt &name, const long long value)
 
void  set_size_t (const irep_idt &name, const std::size_t value)
 
void  remove (const irep_idt &name)
 
void  move_to_sub (irept &irep)
 
void  move_to_named_sub (const irep_idt &name, irept &irep)
 
bool  operator== (const irept &other) const
 
bool  operator!= (const irept &other) const
 
void  swap (irept &irep)
 
bool  operator< (const irept &other) const
  defines ordering on the internal representation
 
bool  ordering (const irept &other) const
  defines ordering on the internal representation
 
int  compare (const irept &i) const
  defines ordering on the internal representation comments are ignored
 
void  clear ()
 
void  make_nil ()
 
subt &  get_sub ()
 
const subt &  get_sub () const
 
named_subt &  get_named_sub ()
 
const named_subt &  get_named_sub () const
 
std::size_t  hash () const
 
std::size_t  full_hash () const
 
bool  full_eq (const irept &other) const
 
std::string  pretty (unsigned indent=0, unsigned max_indent=0) const
 
- Public Member Functions inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >
  sharing_treet (irep_idt _id)
 
  sharing_treet (irep_idt _id, named_subt _named_sub, subt _sub)
 
  sharing_treet ()
 
  sharing_treet (const sharing_treet &irep)
 
  sharing_treet (sharing_treet &&irep)
 
sharing_treet &  operator= (const sharing_treet &irep)
 
sharing_treet &  operator= (sharing_treet &&irep)
 
  ~sharing_treet ()
 
const dt &  read () const
 
dt &  write ()
 

Additional Inherited Members

- Public Types inherited from exprt
typedef std::vector< exprt >  operandst
 
- Public Types inherited from irept
using  baset = tree_implementationt
 
- Public Types inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >
using  dt = tree_nodet< irept, forward_list_as_mapt< irep_idt, irept >, true >
 
using  subt = typename dt::subt
 
using  named_subt = typename dt::named_subt
 
using  tree_implementationt = sharing_treet
  Used to refer to this class from derived classes.
 
- Static Public Member Functions inherited from exprt
static void  check (const exprt &, const validation_modet=validation_modet::INVARIANT)
  Check that the expression is well-formed (shallow checks only, i.e., subexpressions and its type are not checked).
 
static void  validate (const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
  Check that the expression is well-formed, assuming that its subexpressions and type have all ready been checked for well-formedness.
 
static void  validate_full (const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
  Check that the expression is well-formed (full check, including checks of all subexpressions and the type)
 
- Static Public Member Functions inherited from irept
static bool  is_comment (const irep_idt &name)
 
static std::size_t  number_of_non_comments (const named_subt &)
  count the number of named_sub elements that are not comments
 
- Protected Member Functions inherited from exprt
exprt &  op0 ()
 
exprt &  op1 ()
 
exprt &  op2 ()
 
exprt &  op3 ()
 
const exprt &  op0 () const
 
const exprt &  op1 () const
 
const exprt &  op2 () const
 
const exprt &  op3 () const
 
exprt &  add_expr (const irep_idt &name)
 
const exprt &  find_expr (const irep_idt &name) const
 
- Protected Member Functions inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >
void  detach ()
 
- Static Protected Member Functions inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >
static void  remove_ref (dt *old_data)
 
static void  nonrecursive_destructor (dt *old_data)
  Does the same as remove_ref, but using an explicit stack instead of recursion.
 
- Protected Attributes inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >
dt *  data
 
- Static Protected Attributes inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >
static dt  empty_d
 

Detailed Description

Data structure for representing an arbitrary statement in a program.

Every specific type of statement (e.g. block of statements, assignment, if-then-else statement...) is represented by a subtype of codet. codets are represented to be subtypes of exprt since statements can occur in an expression context in C: for example, the assignment x = y; is an expression with return value y. For other types of statements in an expression context, see e.g. https://gcc.gnu.org/onlinedocs/gcc/Statement-Exprs.html. To distinguish a codet from other exprts, we set its id() to ID_code. To distinguish different types of codet, we use a named sub ID_statement.

Definition at line 28 of file std_code_base.h.

Constructor & Destructor Documentation

◆  codet() [1/4]

codet::codet ( const irep_idt &  statement )
inlineexplicit
Parameters
statement Specifies the type of the codet to be constructed, e.g. ID_block for a code_blockt or ID_assign for a code_frontend_assignt.

Definition at line 34 of file std_code_base.h.

◆  codet() [2/4]

codet::codet ( const irep_idt &  statement,
source_locationt  loc 
)
inline

Definition at line 39 of file std_code_base.h.

◆  codet() [3/4]

codet::codet ( const irep_idt &  statement,
operandst  _op 
)
inlineexplicit
Parameters
statement Specifies the type of the codet to be constructed, e.g. ID_block for a code_blockt or ID_assign for a code_frontend_assignt.
_op any operands to be added

Definition at line 49 of file std_code_base.h.

◆  codet() [4/4]

codet::codet ( const irep_idt &  statement,
operandst  op,
source_locationt  loc 
)
inline

Definition at line 54 of file std_code_base.h.

Member Function Documentation

◆  first_statement() [1/2]

codet & codet::first_statement ( )

In the case of a codet type that represents multiple statements, return the first of them.

Otherwise return the codet itself.

Definition at line 18 of file std_code.cpp.

◆  first_statement() [2/2]

const codet & codet::first_statement ( ) const

In the case of a codet type that represents multiple statements, return the first of them.

Otherwise return the codet itself.

Definition at line 35 of file std_code.cpp.

◆  get_statement()

const irep_idt & codet::get_statement ( ) const
inline

Definition at line 65 of file std_code_base.h.

◆  last_statement() [1/2]

codet & codet::last_statement ( )

In the case of a codet type that represents multiple statements, return the last of them.

Otherwise return the codet itself.

Definition at line 52 of file std_code.cpp.

◆  last_statement() [2/2]

const codet & codet::last_statement ( ) const

In the case of a codet type that represents multiple statements, return the last of them.

Otherwise return the codet itself.

Definition at line 69 of file std_code.cpp.

◆  op0() [1/2]

exprt & exprt::op0 ( )
inline

Definition at line 134 of file expr.h.

◆  op0() [2/2]

const exprt & exprt::op0 ( ) const
inline

Definition at line 146 of file expr.h.

◆  op1() [1/2]

exprt & exprt::op1 ( )
inline

Definition at line 137 of file expr.h.

◆  op1() [2/2]

const exprt & exprt::op1 ( ) const
inline

Definition at line 149 of file expr.h.

◆  op2() [1/2]

exprt & exprt::op2 ( )
inline

Definition at line 140 of file expr.h.

◆  op2() [2/2]

const exprt & exprt::op2 ( ) const
inline

Definition at line 152 of file expr.h.

◆  op3() [1/2]

exprt & exprt::op3 ( )
inline

Definition at line 143 of file expr.h.

◆  op3() [2/2]

const exprt & exprt::op3 ( ) const
inline

Definition at line 155 of file expr.h.

◆  set_statement()

void codet::set_statement ( const irep_idt &  statement )
inline

Definition at line 60 of file std_code_base.h.

The documentation for this class was generated from the following files:

AltStyle によって変換されたページ (->オリジナル) /