GraphML witnesses: correctly set the scope of parameters

We would previously use the name of the calling function. Instead,
parameter assignments require a special case. Regression test kindly
provided by @JanSvejda.

Fixes: #4418

Author: tautschnig

regression/cbmc/graphml_witness1/test.desc

@@ -43,7 +43,7 @@ main.c
     <edge source="[0-9\.]*" target="[0-9\.]*">
       <data key="originfile">main.c</data>
       <data key="startline">29</data>
-      <data key="assumption.scope">main</data>
+      <data key="assumption.scope">remove_one</data>
     </edge>
     <node id="[0-9\.]*"/>
     <edge source="[0-9\.]*" target="[0-9\.]*">

regression/cbmc/graphml_witness2/main.c

@@ -0,0 +1,31 @@
+extern void __VERIFIER_error();
+
+static float one(float *foo)
+{
+  return *foo;
+}
+
+static float two(float *foo)
+{
+  return *foo;
+}
+
+float x = 0;
+
+void step()
+{
+  x = one(0);
+}
+
+int main(void)
+{
+  while(1)
+  {
+    step();
+    if(x == 0)
+    {
+      __VERIFIER_error();
+    }
+  }
+  return 0;
+}

regression/cbmc/graphml_witness2/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--graphml-witness - --unwindset main.0:1 --unwinding-assertions
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+<data key="assumption">foo = \(\(float \*\)0\);</data>
+<data key="assumption.scope">one</data>
+--
+^warning: ignoring

src/goto-programs/graphml_witness.cpp

@@ -492,7 +492,13 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
 
           xmlt &val_s = edge.new_element("data");
           val_s.set_attribute("key", "assumption.scope");
-          val_s.data = id2string(it->function_id);
+          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);
 
           if(has_prefix(val.data, "\\result ="))
           {