Added a test case requiring GraphML witnesses

The test data includes almost all GraphML output - lines that may be
interpreted as regular expressions are omitted.

Author: tautschnig

regression/cbmc/graphml_witness1/main.c

@@ -0,0 +1,34 @@
+extern int __VERIFIER_nondet_int(void);
+
+typedef enum {
+  LIST_BEG,
+  LIST_END
+} end_point_t;
+
+typedef enum {
+  ITEM_PREV,
+  ITEM_NEXT
+} direction_t;
+
+void remove_one(end_point_t from)
+{
+  const direction_t next_field = (LIST_BEG == from) ? ITEM_NEXT : ITEM_PREV;
+}
+
+end_point_t rand_end_point(void)
+{
+  _Bool choice;
+  if (choice)
+    return LIST_BEG;
+  else
+    return LIST_END;
+}
+
+int main()
+{
+  remove_one(rand_end_point());
+
+  __CPROVER_assert(0, "");
+
+  return 0;
+}

regression/cbmc/graphml_witness1/test.desc

@@ -0,0 +1,78 @@
+CORE
+main.c
+--graphml-witness -
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+<graphml xmlns="http://graphml.graphdrawing.org/xmlns" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
+  <key attr.name="invariant" attr.type="string" for="node" id="invariant"/>
+  <key attr.name="invariant.scope" attr.type="string" for="node" id="invariant.scope"/>
+  <key attr.name="nodeType" attr.type="string" for="node" id="nodetype">
+    <default>path</default>
+  </key>
+  <key attr.name="isFrontierNode" attr.type="boolean" for="node" id="frontier">
+    <default>false</default>
+  </key>
+  <key attr.name="isViolationNode" attr.type="boolean" for="node" id="violation">
+    <default>false</default>
+  </key>
+  <key attr.name="isEntryNode" attr.type="boolean" for="node" id="entry">
+    <default>false</default>
+  </key>
+  <key attr.name="isSinkNode" attr.type="boolean" for="node" id="sink">
+    <default>false</default>
+  </key>
+  <key attr.name="enterLoopHead" attr.type="boolean" for="edge" id="enterLoopHead">
+    <default>false</default>
+  </key>
+  <key attr.name="threadNumber" attr.type="int" for="node" id="thread">
+    <default>0</default>
+  </key>
+  <key attr.name="sourcecodeLanguage" attr.type="string" for="graph" id="sourcecodelang"/>
+  <key attr.name="programFile" attr.type="string" for="graph" id="programfile"/>
+  <key attr.name="programHash" attr.type="string" for="graph" id="programhash"/>
+  <key attr.name="specification" attr.type="string" for="graph" id="specification"/>
+  <key attr.name="architecture" attr.type="string" for="graph" id="architecture"/>
+  <key attr.name="producer" attr.type="string" for="graph" id="producer"/>
+  <key attr.name="sourcecode" attr.type="string" for="edge" id="sourcecode"/>
+  <key attr.name="startline" attr.type="int" for="edge" id="startline"/>
+  <key attr.name="control" attr.type="string" for="edge" id="control"/>
+  <key attr.name="assumption" attr.type="string" for="edge" id="assumption"/>
+  <key attr.name="assumption.resultfunction" attr.type="string" for="edge" id="assumption.resultfunction"/>
+  <key attr.name="assumption.scope" attr.type="string" for="edge" id="assumption.scope"/>
+  <key attr.name="enterFunction" attr.type="string" for="edge" id="enterFunction"/>
+  <key attr.name="returnFromFunction" attr.type="string" for="edge" id="returnFrom"/>
+  <key attr.name="witness-type" attr.type="string" for="graph" id="witness-type"/>
+  <graph edgedefault="directed">
+    <data key="sourcecodelang">C</data>
+    <node id="sink"/>
+    <node id="33.22">
+      <data key="entry">true</data>
+    </node>
+    <edge source="33.22" target="4.29">
+      <data key="originfile">main.c</data>
+      <data key="startline">21</data>
+    </edge>
+    <node id="4.29"/>
+    <edge source="4.29" target="29.31">
+      <data key="originfile">main.c</data>
+      <data key="startline">29</data>
+      <data key="assumption.scope">main</data>
+    </edge>
+    <node id="29.31"/>
+    <edge source="29.31" target="5.33">
+      <data key="originfile">main.c</data>
+      <data key="startline">15</data>
+      <data key="assumption.scope">remove_one</data>
+    </edge>
+    <node id="5.33">
+      <data key="violation">true</data>
+    </node>
+    <edge source="5.33" target="sink">
+      <data key="originfile">main.c</data>
+      <data key="startline">31</data>
+    </edge>
+  </graph>
+</graphml>
+--
+^warning: ignoring