@@ -29,7 +29,11 @@ Within cbmc, strings are represented using \ref irep_idt, or \ref irep_namet
29
29
for keys to [ named_sub] (\ref irept::dt::named_sub) or
30
30
[ comments] (\ref irept::dt::comments). By default these are both
31
31
typedefed to \ref dstringt. For debugging purposes you can set ` USE_STD_STRING ` ,
32
- in which case they are both typedefed to ` std::string ` .
32
+ in which case they are both typedefed to ` std::string ` . You can also easily
33
+ convert an [ irep_idt] (\ref irep_idt) or [ irep_namet] (\ref irep_namet) to a
34
+ ` std::string ` using the [ id2string] (\ref id2string) or
35
+ [ name2string] (\ref name2string) function, respectively, or either of them to a
36
+ ` char* ` using the [ c_str()] (\ref dstringt::c_str) member function.
33
37
34
38
\ref dstringt stores a string as an index into a large
35
39
static table of strings. This makes it easy to compare if two
@@ -41,7 +45,7 @@ You can refer to this \ref irep_idt as `ID_type`. The other kind of line you
41
45
see is ` “IREP_ID_TWO(C_source_location, #source_location)” ` , which means the
42
46
\ref irep_idt for the string “#source_location” can be referred to as
43
47
` ID_C_source_location ` . The “C” is for comment, meaning that it should be
44
- stored in the ( [ comments] (\ref irept::dt::comments). Any strings that need
48
+ stored in the [ comments] (\ref irept::dt::comments). Any strings that need
45
49
to be stored as [ irep_idt] (\ref irep_idt)s which aren't in ` irep_ids.def `
46
50
are added to the end of the table when they are first encountered, and the
47
51
same index is used for all instances.
0 commit comments