@@ -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:
141142Another 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
149146various expressions, usually the result of some early processing, e.g. the result of the
150147frontend parsing a file).
@@ -159,3 +156,13 @@ It might be possible that a specific source location might point to a CBMC instr
159156primitive (which might be reported as a ` built-in-addition ` ) or there might even be no-source
160157location (because it might be part of harnesses generated as an example, that have no presence
161158in 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