From 52c6fcb4ee638b3b33b9e00086bdda0af93a1564 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Franti=C5=A1ek=20Ne=C4=8Das?= Date: Wed, 16 Nov 2022 15:12:29 +0100 Subject: [PATCH] Only add assumption scope if not empty MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The GOTO trace may contain instructions from the global scope (e.g. assigning a value to a global variable). In such case, the scope should be global, i.e. no assumption.scope as per the witness specification. Signed-off-by: František Nečas --- src/goto-programs/graphml_witness.cpp | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index b83e192ef0c..3a24bc63507 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -476,15 +476,18 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) code_assignt assign{it->full_lhs, it->full_lhs_value}; val.data = convert_assign_rec(lhs_id, assign); - xmlt &val_s = edge.new_element("data"); - val_s.set_attribute("key", "assumption.scope"); - irep_idt function_id = it->function_id; - const symbolt *symbol_ptr = nullptr; - if(!ns.lookup(lhs_id, symbol_ptr) && symbol_ptr->is_parameter) + if(!it->function_id.empty()) { - function_id = lhs_id.substr(0, lhs_id.find("::")); + xmlt &val_s = edge.new_element("data"); + val_s.set_attribute("key", "assumption.scope"); + irep_idt function_id = it->function_id; + const symbolt *symbol_ptr = nullptr; + if(!ns.lookup(lhs_id, symbol_ptr) && symbol_ptr->is_parameter) + { + function_id = lhs_id.substr(0, lhs_id.find("::")); + } + val_s.data = id2string(function_id); } - val_s.data = id2string(function_id); if(has_prefix(val.data, "\\result =")) {