[SV-COMP'18 12/19] SV-COMP graphml fixes [blocks: #3486]

regression/cbmc/graphml_witness1/test.desc

@@ -7,34 +7,21 @@ main.c
 <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"/>
@@ -45,7 +32,6 @@ main.c
   <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="[0-9\.]*">
       <data key="entry">true</data>
     </node>
@@ -57,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\.]*">
@@ -68,10 +54,6 @@ main.c
     <node id="[0-9\.]*">
       <data key="violation">true</data>
     </node>
-    <edge source="[0-9\.]*" target="sink">
-      <data key="originfile">main.c</data>
-      <data key="startline">31</data>
-    </edge>
   </graph>
 </graphml>
 --

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/ansi-c/expr2c.cpp

@@ -42,7 +42,8 @@ expr2c_configurationt expr2c_configurationt::default_configuration
   true,
   true,
   "TRUE",
-  "FALSE"
+  "FALSE",
+  true
 };
 
 expr2c_configurationt expr2c_configurationt::clean_configuration
@@ -51,7 +52,8 @@ expr2c_configurationt expr2c_configurationt::clean_configuration
   false,
   false,
   "1",
-  "0"
+  "0",
+  false
 };
 
 // clang-format on
@@ -1857,14 +1859,39 @@ std::string expr2ct::convert_constant(
     else if(dest.size()==4 &&
             (dest[0]=='+' || dest[0]=='-'))
     {
-      if(dest=="+inf")
-        dest="+INFINITY";
-      else if(dest=="-inf")
-        dest="-INFINITY";
-      else if(dest=="+NaN")
-        dest="+NAN";
-      else if(dest=="-NaN")
-        dest="-NAN";
+      if(configuration.use_library_macros)
+      {
+        if(dest == "+inf")
+          dest = "+INFINITY";
+        else if(dest == "-inf")
+          dest = "-INFINITY";
+        else if(dest == "+NaN")
+          dest = "+NAN";
+        else if(dest == "-NaN")
+          dest = "-NAN";
+      }
+      else
+      {
+        // ANSI-C: double is default; float/long-double require annotation
+        std::string suffix = "";
+        if(src.type() == float_type())
+          suffix = "f";
+        else if(
+          src.type() == long_double_type() &&
+          double_type() != long_double_type())
+        {
+          suffix = "l";
+        }
+
+        if(dest == "+inf")
+          dest = "(1.0" + suffix + "/0.0" + suffix + ")";
+        else if(dest == "-inf")
+          dest = "(-1.0" + suffix + "/0.0" + suffix + ")";
+        else if(dest == "+NaN")
+          dest = "(0.0" + suffix + "/0.0" + suffix + ")";
+        else if(dest == "-NaN")
+          dest = "(-0.0" + suffix + "/0.0" + suffix + ")";
+      }
     }
   }
   else if(type.id()==ID_fixedbv)
@@ -1885,16 +1912,14 @@ std::string expr2ct::convert_constant(
   }
   else if(type.id()==ID_pointer)
   {
-    if(value==ID_NULL)
-    {
-      dest="NULL";
-      if(type.subtype().id()!=ID_empty)
-        dest="(("+convert(type)+")"+dest+")";
-    }
-    else if(value==std::string(value.size(), '0') &&
-            config.ansi_c.NULL_is_zero)
+    if(
+      value == ID_NULL ||
+      (value == std::string(value.size(), '0') && config.ansi_c.NULL_is_zero))
     {
-      dest="NULL";
+      if(configuration.use_library_macros)
+        dest = "NULL";
+      else
+        dest = "0";
       if(type.subtype().id()!=ID_empty)
         dest="(("+convert(type)+")"+dest+")";
     }

src/ansi-c/expr2c.h

@@ -36,17 +36,22 @@ struct expr2c_configurationt final
   /// This is the string that will be printed for the false boolean expression
   std::string false_string;
 
+  /// This is the string that will be printed for null pointers
+  bool use_library_macros;
+
   expr2c_configurationt(
     const bool include_struct_padding_components,
     const bool print_struct_body_in_type,
     const bool include_array_size,
     const std::string &true_string,
-    const std::string &false_string)
+    const std::string &false_string,
+    const bool use_library_macros)
     : include_struct_padding_components(include_struct_padding_components),
       print_struct_body_in_type(print_struct_body_in_type),
       include_array_size(include_array_size),
       true_string(true_string),
-      false_string(false_string)
+      false_string(false_string),
+      use_library_macros(use_library_macros)
   {
   }