Skip to content

Commit 5f15042

Browse files
committed
Separate the documentation of the irept class
Because `irept` itself should be considered to live at a separate level of abstraction from the other classes.
1 parent 3d096c0 commit 5f15042

File tree

1 file changed

+12
-5
lines changed

1 file changed

+12
-5
lines changed

doc/architectural/central-data-structures.md

Lines changed: 12 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -131,7 +131,8 @@ detail to illuminate some details at the code level:
131131
* The `instruction` is a statement represented by a `goto_instruction_codet`.
132132
* A `goto_instruction_codet` is an alias of `codet` (a data structure broadly representing
133133
a statement inside CBMC) that contains the actual code to be executed.
134-
* You can distinguish different statements by inspecting the `irep` element `ID_statement`.
134+
* You can distinguish different statements by using the result of the
135+
`get_statement` member function of the `codet` class.
135136
* The `guard` is an `exprt` (a data structure broadly representing an expression inside CBMC)
136137
that is expected to have type `bool`.
137138
* This is optional - not every instruction is expected to have a `guard` associated with it.
@@ -141,10 +142,6 @@ detail to illuminate some details at the code level:
141142
Another important data structure that needs to be discussed at this point is
142143
`source_locationt`.
143144

144-
This is an `irept`. `irep`s are the central data structure that model most entities inside
145-
CBMC and the assorted tools - effectively a node/map like data structure that forms a hierachical
146-
tree that ends up modeling graphs like ASTs, CFGs, etc.
147-
148145
`source_locationt` are attached into various `exprt`s (the data structure representing
149146
various expressions, usually the result of some early processing, e.g. the result of the
150147
frontend parsing a file).
@@ -159,3 +156,13 @@ It might be possible that a specific source location might point to a CBMC instr
159156
primitive (which might be reported as a `built-in-addition`) or there might even be no-source
160157
location (because it might be part of harnesses generated as an example, that have no presence
161158
in the user code).
159+
160+
## irept
161+
162+
`irep`s are the underlying data structure used to implement many of the data
163+
structures in CBMC and the assorted tools. These include the `exprt`, `typet`,
164+
`codet` and `source_locationt` classes. This is a tree data structure where
165+
each node is expected to contain a string/ID and may have child nodes stored in
166+
both a sequence of child nodes and a map of strings/IDs to child nodes. This
167+
enables the singular `irept` data structure to be used to model graphs such as
168+
ASTs, CFGs, etc.

0 commit comments

Comments
 (0)