Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions src/ansi-c/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -78,9 +78,9 @@ data structures. In particular, \ref exprt "expressions",
An irep is a tree of ireps. A subtlety is that an irep is actually the
root of _three_ (possibly empty) trees, i.e. it has three disjoint sets
of children: \ref irept::get_sub() returns a list of children, and
\ref irept::get_named_sub() and \ref irept::get_comments() each return an
association from names to children. **Most clients never use these
functions directly**, as subtypes of irept generally provide more
\ref irept::get_named_sub() returns an association from names to children.
**Most clients never use these functions directly**,
as subtypes of irept generally provide more
descriptive functions. For example, the operands of an
\ref exprt "expression" (\ref exprt::op0() "op0", op1 etc) are
really that expression's children; the
Expand Down
29 changes: 14 additions & 15 deletions src/cpp/cpp_type2name.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -36,30 +36,29 @@ static void irep2name(const irept &irep, std::string &result)
if(irep.id()!="")
result+=do_prefix(irep.id_string());

if(irep.get_named_sub().empty() &&
irep.get_sub().empty() &&
irep.get_comments().empty())
if(irep.get_named_sub().empty() && irep.get_sub().empty())
return;

result+='(';
bool first=true;

forall_named_irep(it, irep.get_named_sub())
{
if(first)
first=false;
else
result+=',';
if(!irept::is_comment(it->first))
{
if(first)
first = false;
else
result += ',';

result+=do_prefix(name2string(it->first));
result += do_prefix(name2string(it->first));

result+='=';
std::string tmp;
irep2name(it->second, tmp);
result+=tmp;
}
result += '=';
std::string tmp;
irep2name(it->second, tmp);
result += tmp;
}

forall_named_irep(it, irep.get_comments())
forall_named_irep(it, irep.get_named_sub())
if(it->first==ID_C_constant ||
it->first==ID_C_volatile ||
it->first==ID_C_restricted)
Expand Down
36 changes: 17 additions & 19 deletions src/util/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -14,15 +14,15 @@ CPROVER codebase.

See detailed documentation at \ref irept.

[irept](\ref irept)s are generic tree nodes. You
should think of each node as holding a single string ([data](\ref irept::data),
actually an \ref irep_idt) and lots of child nodes, some of which are numbered
([sub](\ref irept::dt::sub)) and some of which are labelled, and the label
can either start with a “\#” ([comments](\ref irept::dt::comments)) or without
one ([named_sub](\ref irept::dt::named_sub)). The meaning of the “\#” is that
this child shouldn't be counted when comparing two [irept](\ref irept)s for
equality; this is usually used when making an advisory annotation which does
not alter the semantics of the program.
[irept](\ref irept)s are generic tree nodes. You should think of each node
as holding a single string ([data](\ref irept::data), actually an \ref
irep_idt) and lots of child nodes, some of which are numbered ([sub](\ref
irept::dt::sub)) and some of which are labelled ([named_sub](\ref
irept::dt::named_sub)). The the label can either start with a “\#” or
without one. The meaning of the “\#” is that this child shouldn't be
considered when comparing two [irept](\ref irept)s for equality; this is
usually used when making an advisory annotation which does not alter the
semantics of the program.

They are used to represent many kinds of structured objects throughout the
CPROVER codebase, such as expressions, types and code. An \ref exprt represents
Expand Down Expand Up @@ -72,9 +72,8 @@ standard data structures as in irept.

\subsection irep_idt_section Strings: dstringt, the string_container and the ID_*

Within cbmc, strings are represented using \ref irep_idt, or \ref irep_namet
for keys to [named_sub](\ref irept::dt::named_sub) or
[comments](\ref irept::dt::comments). By default these are both
Within cbmc, strings are represented using \ref irep_idt or \ref irep_namet
for keys to [named_sub](\ref irept::dt::named_sub). By default these are both
typedefed to \ref dstringt. For debugging purposes you can set `USE_STD_STRING`,
in which case they are both typedefed to `std::string`. You can also easily
convert an [irep_idt](\ref irep_idt) or [irep_namet](\ref irep_namet) to a
Expand All @@ -91,11 +90,10 @@ in `irep_ids.def` is `“IREP_ID_ONE(type)”`, so the string “type” has ind
You can refer to this \ref irep_idt as `ID_type`. The other kind of line you
see is \c "IREP_ID_TWO(C_source_location, #source_location)", which means the
\ref irep_idt for the string “\#source_location” can be referred to as
`ID_C_source_location`. The “C” is for comment, meaning that it should be
stored in the [comments](\ref irept::dt::comments). Any strings that need
to be stored as [irep_idt](\ref irep_idt)s which aren't in `irep_ids.def`
are added to the end of the table when they are first encountered, and the
same index is used for all instances.
`ID_C_source_location`. The “C” is for comment, meaning that it starts with
“\#”. Any strings that need to be stored as [irep_idt](\ref irep_idt)s
which aren't in `irep_ids.def` are added to the end of the table when they
are first encountered, and the same index is used for all instances.

See documentation at \ref dstringt.

Expand Down Expand Up @@ -125,8 +123,8 @@ of size 2 (for the two arguments of minus).

Recall that every \ref irept has one piece of data of its own, i.e. its
[id()](\ref irept::id()), and all other information is in its
[named_sub](\ref irept::dt::named_sub), [comments](\ref irept::dt::comments)
or [sub](\ref irept::dt::sub). For [exprt](\ref exprt)s, the
[named_sub](\ref irept::dt::named_sub) or [sub](\ref irept::dt::sub).
For [exprt](\ref exprt)s, the
[id()](\ref irept::id()) is used to specify why kind of \ref exprt this is,
so a \ref minus_exprt has `ID_minus` as its [id()](\ref irept::id()). This
means that a \ref minus_exprt can be passed wherever an \ref exprt is
Expand Down
Loading