From 5e803105b4fa904f329dbb1437e5b5e26b1c71c8 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 12 Aug 2018 16:19:20 +0100 Subject: [PATCH] add invariant on parent-child class relationship --- src/goto-programs/class_hierarchy.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/goto-programs/class_hierarchy.cpp b/src/goto-programs/class_hierarchy.cpp index cb9106c818d..db7cb2c5d90 100644 --- a/src/goto-programs/class_hierarchy.cpp +++ b/src/goto-programs/class_hierarchy.cpp @@ -50,8 +50,11 @@ void class_hierarchy_grapht::populate(const symbol_tablet &symbol_table) const irep_idt &parent = to_symbol_type(base.type()).get_identifier(); if(!parent.empty()) { - add_edge( - nodes_by_name.at(parent), nodes_by_name.at(symbol_pair.first)); + const auto parent_node_it = nodes_by_name.find(parent); + DATA_INVARIANT( + parent_node_it != nodes_by_name.end(), + "parent class not in symbol table"); + add_edge(parent_node_it->second, nodes_by_name.at(symbol_pair.first)); } } }