Skip to content

Error on switch on variable in base class #154

Closed
@mgudemann

Description

@mgudemann

This program

public class Inheritance2
{
  int x;
  public class A extends Inheritance2
  {
    void m1(int i)
    {
      if (x == 1)
        assert(true);
      else
        assert(false);
    }
    void m2(int i)
    {
      switch(x)
        {
        case 1:
          assert(true);
          break;
        default:
          assert(false);
          break;
        }
    }

    void test1(int i)
    {
      m1(i);
    }
    void test2(int i)
    {
      m2(i);
    }
  }
}

correctly reports on cbmc --function "Inheritance2\$A.test1" Inheritance2.class

** Results:
[assertion.1] assertion at file Inheritance2.java line 11: FAILURE
[assertion.2] assertion at file Inheritance2.java line 21: SUCCESS

but fails on cbmc --function "Inheritance2\$A.test2" Inheritance2.class with

size of program expression: 57 steps
simple slicing removed 8 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to propositional reduction
converting SSA
component x not found in structure

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