add invariant on parent-child class relationship

Daniel Kroening · Daniel Kroening · commit 147f05d25d85 · 2018-08-12T16:19:42.000+01:00
diff --git a/src/goto-programs/class_hierarchy.cpp b/src/goto-programs/class_hierarchy.cpp
@@ -50,6 +50,8 @@ void class_hierarchy_grapht::populate(const symbol_tablet &symbol_table)
         const irep_idt &parent = to_symbol_type(base.type()).get_identifier();
         if(!parent.empty())
         {
+          DATA_INVARIANT(nodes_by_name.find(parent)!=nodes_by_name.end(),
+                         "parent class not in symbol table");
           add_edge(
             nodes_by_name.at(parent), nodes_by_name.at(symbol_pair.first));
         }

Original file line number	Diff line number	Diff line change
`@@ -50,6 +50,8 @@ void class_hierarchy_grapht::populate(const symbol_tablet &symbol_table)`
`50`	`50`	`const irep_idt &parent = to_symbol_type(base.type()).get_identifier();`
`51`	`51`	`if(!parent.empty())`
`52`	`52`	`{`
	`53`	`+ DATA_INVARIANT(nodes_by_name.find(parent)!=nodes_by_name.end(),`
	`54`	`+ "parent class not in symbol table");`
`53`	`55`	`add_edge(`
`54`	`56`	`nodes_by_name.at(parent), nodes_by_name.at(symbol_pair.first));`
`55`	`57`	`}`