Merge pull request #3470 from diffblue/irep-with-single-map

irept: use single map for all named sub-nodes

Author: tautschnig

src/ansi-c/README.md

@@ -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

src/cpp/cpp_type2name.cpp

@@ -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)

src/util/README.md

@@ -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
@@ -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
@@ -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.
 
@@ -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