Skip to content

Commit 589a584

Browse files
Merge pull request #2779 from antlechner/antonia/doc-util-readme
Document dstringt to string conversions
2 parents c679e55 + 3f2537d commit 589a584

File tree

1 file changed

+6
-2
lines changed

1 file changed

+6
-2
lines changed

src/util/README.md

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -76,7 +76,11 @@ Within cbmc, strings are represented using \ref irep_idt, or \ref irep_namet
7676
for keys to [named_sub](\ref irept::dt::named_sub) or
7777
[comments](\ref irept::dt::comments). By default these are both
7878
typedefed to \ref dstringt. For debugging purposes you can set `USE_STD_STRING`,
79-
in which case they are both typedefed to `std::string`.
79+
in which case they are both typedefed to `std::string`. You can also easily
80+
convert an [irep_idt](\ref irep_idt) or [irep_namet](\ref irep_namet) to a
81+
`std::string` using the [id2string](\ref id2string) or
82+
[name2string](\ref name2string) function, respectively, or either of them to a
83+
`char*` using the [c_str()](\ref dstringt::c_str) member function.
8084

8185
\ref dstringt stores a string as an index into a large
8286
static table of strings. This makes it easy to compare if two
@@ -88,7 +92,7 @@ You can refer to this \ref irep_idt as `ID_type`. The other kind of line you
8892
see is `“IREP_ID_TWO(C_source_location, #source_location)”`, which means the
8993
\ref irep_idt for the string “#source_location” can be referred to as
9094
`ID_C_source_location`. The “C” is for comment, meaning that it should be
91-
stored in the ([comments](\ref irept::dt::comments). Any strings that need
95+
stored in the [comments](\ref irept::dt::comments). Any strings that need
9296
to be stored as [irep_idt](\ref irep_idt)s which aren't in `irep_ids.def`
9397
are added to the end of the table when they are first encountered, and the
9498
same index is used for all instances.

0 commit comments

Comments
 (0)