Wrong verdicts in CWE369*bad_version2

[peterschrammel]

These three benchmarks seem to have verdict TRUE instead FALSE.

I've tried with a cut down version, which captures the core logic:

public class Cwe {
  public static void foo(float data, float offset) {
    if (offset < 1.0f)
      return;
    data = data - offset;
    int result = (int) (100.0 / data);
    if (1 < data || data <= 0) {
      assert result < 100;
    }
  }
}

The assertion is unreachable according to JBMC.

It's also unreachable in CBMC using the corresponding C version:

#include <assert.h>

void foo(float data, float offset)
{
  if (offset < 1.0f)
    return;
  data = data - offset;
  int result = (int) (100.0 / data);
  if (1 < data || data <= 0) {
    assert(result < 100);
  }
}

Does anyone have a counterexample for these benchmarks?

@mmuesly

• [ ] programs added to new and appropriately named directory

• [ ] license present and acceptable (in machine-readable comment at beginning of program as specified by the REUSE project)

• [ ] contributed-by present (either in README file or as comment at beginning of program)

• [ ] programs added to a .set file of an existing category, or new sub-category established (if justified)

• [ ] intended property matches the corresponding .prp file

• [ ] programs and expected answer added to a .yml file according to task definitions

• [ ] data model present in task-definition file
• [ ] original (ideally not preprocessed) sources present
• [ ] preprocessed files present
• [ ] preprocessed files generated with correct architecture
• [ ] Makefile added with correct content and without overly broad suppression of warnings

[mmuesly]

public class Cwe {
  public static void foo(float data, float offset) {
    if (offset < 1.0f)
      return;
    data = data - offset;
    int result = (int) (100.0 / data);
    if (1 < data || data <= 0) {
      assert result < 100;
    }
  }

  public static void main (String[] args){
    foo(123, 123);
  }

}

running with java -ea Cwe leads to:

maltemues in /tmp > java -ea Cwe 
Exception in thread "main" java.lang.AssertionError
    at Cwe.foo(Cwe.java:8)
    at Cwe.main(Cwe.java:13)

See float division rules in Java and "Narrowing Primitive Conversion" for more context in the JVM leading to this AssertionError.

I reject the PR.

[peterschrammel]

Thanks, @mmuesly. This proves that the problem is clearly in our tool.