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><command-line></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?