CBMC
object_numbering.h File Reference

Object Numbering. More...

#include <util/expr.h>
#include <util/numbering.h>
+ Include dependency graph for object_numbering.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Typedefs

typedef numberingt< exprt, irep_hashobject_numberingt
 

Detailed Description

Object Numbering.

This is used to abbreviate identical expressions by number: for example, an object_numberingt instance might maintain the map:

1 -> constant_exprt("Hello", string_typet())
2 -> constant_exprt("World", string_typet())
A constant literal expression.
Definition: std_expr.h:2987
String type.
Definition: std_types.h:957

Then any users that agree to use the same object_numberingt instance as a common reference source can use '1' and '2' as shorthands for "Hello" and "World" respectively.

Definition in file object_numbering.h.

Typedef Documentation

◆ object_numberingt

Definition at line 28 of file object_numbering.h.