Skip to content

Wrong property in Java classes outside classpath #562

Closed
@mgudemann

Description

@mgudemann

the following java program

public class base1 {
  class A {
    int x=1;
  }
  class B {
    int x=2;
  }
  void f()
  {
    A a = new A();
    B b = new B();
    assert(a.x == b.x);
  }
}

correctly falsifies the property

** Results:
[java::base1.f:()V.assertion.1] assertion at file base1.java line 12 function java::base1.f:()V bytecode_index 19: FAILURE

but fails to do so when base1$A.class and base1$B.class are not available on the classpath

**** WARNING: no body for function java::java.lang.Class.desiredAssertionStatus:()Z
**** WARNING: no body for function java::base1$A.<init>:(Lbase1;)V
**** WARNING: no body for function java::base1$B.<init>:(Lbase1;)V
size of program expression: 69 steps
simple slicing removed 0 assignments
Generated 0 VCC(s), 0 remaining after simplification
VERIFICATION SUCCESSFUL

Activity

peterschrammel

peterschrammel commented on Mar 10, 2021

@peterschrammel
Member

Not reproducible

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

      Development

      No branches or pull requests

        Participants

        @mgudemann@peterschrammel

        Issue actions

          Wrong property in Java classes outside classpath · Issue #562 · diffblue/cbmc