Skip to content

Wrong label in Java benchmark float-nonlinear-calculation/coral79

coral79, one of the newly added benchmarks from float-nonlinear-calculation is labeled: expected_verdict: true, but the following violation witness produces an assertion violation:

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<graphml xmlns="http://graphml.graphdrawing.org/xmlns" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
  <key attr.name="originFileName" attr.type="string" for="edge" id="originfile">
    <default>&lt;command-line&gt;</default>
  </key>
  <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="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="cyclehead" attr.type="boolean" for="edge" id="cyclehead">
    <default>false</default>
  </key>
  <key attr.name="threadId" attr.type="int" for="edge" id="threadId">
    <default>0</default>
  </key>
  <key attr.name="createThread" attr.type="int" for="edge" id="createThread">
    <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="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="witness-type">violation_witness</data>
      <data key="producer">SWAT</data>
      <!-- data key="specification">na</data>
      <data key="programfile">na</data>
      <data key="programhash">na</data>
      <data key="architecture">64bit</data>
      <data key="sourcecodelang">Java</data -->
    <node id="sink"/>

       <node id="n0">
             <data key="entry">true</data> 
       </node>
       <node id="n1">
       </node>
       <node id="n2">
       </node>
       <node id="n3">
       </node>
       <node id="n4">
       </node>
       <node id="n5">
             <data key="violation">true</data> 
       </node>


       <edge source="n0" target="n1">
         <data key="originfile">Main.java</data>
         <data key="startline">12</data>
         <data key="threadId">0</data>
         <data key="assumption">d1 = 2.225073858507202E-308</data>
         <data key="assumption.scope">java::LMain;.main([Ljava/lang/String;)V</data>
       </edge> <edge source="n1" target="n2">
         <data key="originfile">Main.java</data>
         <data key="startline">13</data>
         <data key="threadId">0</data>
         <data key="assumption">d2 = 2.225073858507202E-308</data>
         <data key="assumption.scope">java::LMain;.main([Ljava/lang/String;)V</data>
       </edge> <edge source="n2" target="n3">
         <data key="originfile">Main.java</data>
         <data key="startline">14</data>
         <data key="threadId">0</data>
         <data key="assumption">d3 = 2.225073858507202E-308</data>
         <data key="assumption.scope">java::LMain;.main([Ljava/lang/String;)V</data>
       </edge> <edge source="n3" target="n4">
         <data key="originfile">Main.java</data>
         <data key="startline">15</data>
         <data key="threadId">0</data>
         <data key="assumption">d4 = 2.225073858507202E-308</data>
         <data key="assumption.scope">java::LMain;.main([Ljava/lang/String;)V</data>
       </edge> <edge source="n4" target="n5">
         <data key="originfile">Main.java</data>
         <data key="startline">16</data>
         <data key="threadId">0</data>
         <data key="assumption">i = 1</data>
         <data key="assumption.scope">java::LMain;.main([Ljava/lang/String;)V</data>
       </edge> 

  </graph>
</graphml>

When checked against wit4java produces:

bin/wit4java --packages ../../SWAT-Research/targets/sv-comp/sv-benchmarks/java/common/ ../../SWAT-Research/targets/sv-comp/sv-benchmarks/java/float-nonlinear-calculation/common --witness ../SWAT/WitnessCreator/witness.graphml ../../SWAT-Research/targets/sv-comp/sv-benchmarks/java/float-nonlinear-calculation/coral79
wit4java version: 3.0
witness:  ../SWAT/WitnessCreator/witness.graphml
wit4java: Witness Correct

So instantiating all four double values to Double.MIN_NORMAL and the one int to 1 causes the assertion violation.

@MLB-SE did I miss something that makes this witness invalid?

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information