Skip to content

Crash when using core models and comparing two inputs #2307

Closed
@thk123

Description

@thk123

Given the following Java:

class Test2Class {
  static void test(Object a, Object b) {
    assert(a == b);
  }
}

When running jbmc with the core models: jbmc Test2Class.class --function Test2Class.test --classpath ../../../src/java_bytecode/library/core-models.jar:.

The following error is generated:

struct: component type does not match: signedbv
  * width: 32
  * #c_type: signed_int vs. 
terminate called after throwing an instance of 'int'
Aborted (core dumped)

The component that is specifically the wrong type is monitorCount from java.lang.Object model.

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions