4
4
\author Martin Brain, Peter Schrammel, Owen Jones
5
5
6
6
## Strings: dstringt, the string_container and the ID_ * ##
7
+
7
8
Within cbmc, strings are represented using ` irep_idt ` . By default this is
8
9
typedefed to \ref dstringt, which stores a string as an index into a large
9
10
static table of strings. This makes it easy to compare if two ` irep_idt ` s
@@ -22,6 +23,7 @@ first encountered, and the same index is used for all instances.
22
23
See documentation at \ref dstringt.
23
24
24
25
## irept: a 4-triple (data, named-sub, comments, sub) ##
26
+
25
27
See documentation at \ref irept.
26
28
27
29
As that documentation says, ` irept ` s are generic tree nodes. You should
@@ -41,6 +43,7 @@ To be documented.
41
43
To be documented.
42
44
43
45
## exprt ##
46
+
44
47
\ref exprt is the class to represent an expression. It inherits from \ref irept,
45
48
and the only things it adds to it are that every \ref exprt has a named sub
46
49
containing its type and everything in the sub of an \ref exprt is again an
@@ -60,6 +63,7 @@ expression then you have to check its `id()` (or use
60
63
` can_cast_expr<minus_exprt> ` ).
61
64
62
65
## codet ##
66
+
63
67
\ref exprt represents expressions and \ref codet represents statements. \ref codet
64
68
inherits from \ref exprt, so all ` codet ` s are ` exprt ` s, with ` id() ` ` ID_code ` .
65
69
Many different kinds of statements inherit from \ref codet, and they are
0 commit comments