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

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

    Issue actions