Skip to content

Integer.getInteger model recurses unconditionally #9168

Open
Open
Integer.getInteger model recurses unconditionally#9168

Description

@lemmy
lemmy
opened on Sep 24, 2026

https://github.com/diffblue/java-models-library/blob/master/src/main/java/java/lang/Integer.java#L873-L875 calls itself:

  public static Integer getInteger(String nm, Integer val) {
      return getInteger(nm, null);
  }

All three overloads are affected because the others delegate to this one.

mkuppe@mkuppe01:/data/src/TLA/tlaplus$ jbmc java.lang.Integer -cp /usr/lib/core-models.jar --verbosity 4 --unwind 1 --function 'java.lang.Integer.getInteger:(Ljava/lang/String;)Ljava/lang/Integer;'

** Results:
[array-create-negative-size.1] Array size should be >= 0: SUCCESS
[array-create-negative-size.2] Array size should be >= 0: SUCCESS
[array-create-negative-size.3] Array size should be >= 0: SUCCESS
[array-create-negative-size.4] Array size should be >= 0: SUCCESS
[array-create-negative-size.5] Array size should be >= 0: SUCCESS
[array-create-negative-size.6] Array size should be >= 0: SUCCESS
[array-create-negative-size.7] Array size should be >= 0: SUCCESS
[array-create-negative-size.8] Array size should be >= 0: SUCCESS
[array-create-negative-size.9] Array size should be >= 0: SUCCESS
java/lang/Class.java function java::java.lang.Class.<init>:()V
[java::java.lang.Class.<init>:()V.null-pointer-exception.1] line 44 Null pointer check: SUCCESS
[java::java.lang.Class.<init>:()V.null-pointer-exception.2] line 387 Null pointer check: SUCCESS

java/lang/Class.java function java::java.lang.Class.cproverNondetInitialize:()V
[java::java.lang.Class.cproverNondetInitialize:()V.null-pointer-exception.1] line 454 Null pointer check: SUCCESS
[java::java.lang.Class.cproverNondetInitialize:()V.null-pointer-exception.2] line 455 Null pointer check: SUCCESS

java/lang/Class.java function java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;
[java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;.null-pointer-exception.1] line 114 Null pointer check: SUCCESS
[java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;.null-pointer-exception.2] line 115 Null pointer check: SUCCESS

java/lang/Integer.java function java::java.lang.Integer.getInteger:(Ljava/lang/String;)Ljava/lang/Integer;
[java::java.lang.Integer.getInteger:(Ljava/lang/String;)Ljava/lang/Integer;.1] line 786 no uncaught exception: SUCCESS

java/lang/Integer.java function java::java.lang.Integer.getInteger:(Ljava/lang/String;Ljava/lang/Integer;)Ljava/lang/Integer;
[java::java.lang.Integer.getInteger:(Ljava/lang/String;Ljava/lang/Integer;)Ljava/lang/Integer;.recursion] line 874 recursion unwinding assertion: FAILURE

java/lang/Object.java function java::java.lang.Object.<init>:()V
[java::java.lang.Object.<init>:()V.null-pointer-exception.1] line 40 Null pointer check: SUCCESS
VERIFICATION FAILED
mkuppe@mkuppe01:/data/src/TLA/tlaplus$ jbmc java.lang.Long -cp /usr/lib/core-models.jar --verbosity 4 --unwind 1 --function 'java.lang.Long.getLong:(Ljava/lang/String;)Ljava/lang/Long;'

** Results:
[array-create-negative-size.1] Array size should be >= 0: SUCCESS
[array-create-negative-size.2] Array size should be >= 0: SUCCESS
[array-create-negative-size.3] Array size should be >= 0: SUCCESS
[array-create-negative-size.4] Array size should be >= 0: SUCCESS
[array-create-negative-size.5] Array size should be >= 0: SUCCESS
[array-create-negative-size.6] Array size should be >= 0: SUCCESS
[array-create-negative-size.7] Array size should be >= 0: SUCCESS
[array-create-negative-size.8] Array size should be >= 0: SUCCESS
[array-create-negative-size.9] Array size should be >= 0: SUCCESS
function java::java.lang.String.length:()I
[java::java.lang.String.length:()I.1] assertion: SUCCESS

function java::java.lang.String.startsWith:(Ljava/lang/String;I)Z
[java::java.lang.String.startsWith:(Ljava/lang/String;I)Z.1] assertion: SUCCESS
[java::java.lang.String.startsWith:(Ljava/lang/String;I)Z.2] assertion: SUCCESS
[java::java.lang.String.startsWith:(Ljava/lang/String;I)Z.3] assertion: SUCCESS
[java::java.lang.String.startsWith:(Ljava/lang/String;I)Z.4] assertion: SUCCESS

function java::java.lang.StringBuilder.<init>:()V
[java::java.lang.StringBuilder.<init>:()V.1] assertion: SUCCESS

function java::java.lang.StringBuilder.append:(Ljava/lang/String;)Ljava/lang/StringBuilder;
[java::java.lang.StringBuilder.append:(Ljava/lang/String;)Ljava/lang/StringBuilder;.1] assertion: SUCCESS
[java::java.lang.StringBuilder.append:(Ljava/lang/String;)Ljava/lang/StringBuilder;.2] assertion: SUCCESS
[java::java.lang.StringBuilder.append:(Ljava/lang/String;)Ljava/lang/StringBuilder;.3] assertion: SUCCESS
[java::java.lang.StringBuilder.append:(Ljava/lang/String;)Ljava/lang/StringBuilder;.4] assertion: SUCCESS
[java::java.lang.StringBuilder.append:(Ljava/lang/String;)Ljava/lang/StringBuilder;.5] assertion: SUCCESS
[java::java.lang.StringBuilder.append:(Ljava/lang/String;)Ljava/lang/StringBuilder;.6] assertion: SUCCESS

function java::java.lang.StringBuilder.toString:()Ljava/lang/String;
[java::java.lang.StringBuilder.toString:()Ljava/lang/String;.1] assertion: SUCCESS
[java::java.lang.StringBuilder.toString:()Ljava/lang/String;.2] assertion: SUCCESS
[java::java.lang.StringBuilder.toString:()Ljava/lang/String;.3] assertion: SUCCESS

function java::org.cprover.CProverString.charAt:(Ljava/lang/String;I)C
[java::org.cprover.CProverString.charAt:(Ljava/lang/String;I)C.1] assertion: SUCCESS
[java::org.cprover.CProverString.charAt:(Ljava/lang/String;I)C.2] assertion: SUCCESS

function java::org.cprover.CProverString.isValidLong:(Ljava/lang/String;I)Z
[java::org.cprover.CProverString.isValidLong:(Ljava/lang/String;I)Z.1] assertion: SUCCESS
[java::org.cprover.CProverString.isValidLong:(Ljava/lang/String;I)Z.2] assertion: SUCCESS

function java::org.cprover.CProverString.parseLong:(Ljava/lang/String;I)J
[java::org.cprover.CProverString.parseLong:(Ljava/lang/String;I)J.1] assertion: SUCCESS
[java::org.cprover.CProverString.parseLong:(Ljava/lang/String;I)J.2] assertion: SUCCESS

function java::org.cprover.CProverString.substring:(Ljava/lang/String;I)Ljava/lang/String;
[java::org.cprover.CProverString.substring:(Ljava/lang/String;I)Ljava/lang/String;.1] assertion: SUCCESS
[java::org.cprover.CProverString.substring:(Ljava/lang/String;I)Ljava/lang/String;.2] assertion: SUCCESS
[java::org.cprover.CProverString.substring:(Ljava/lang/String;I)Ljava/lang/String;.3] assertion: SUCCESS

function java::org.cprover.CProverString.toString:(I)Ljava/lang/String;
[java::org.cprover.CProverString.toString:(I)Ljava/lang/String;.1] assertion: SUCCESS

java/lang/Class.java function java::java.lang.Class.<init>:()V
[java::java.lang.Class.<init>:()V.null-pointer-exception.1] line 44 Null pointer check: SUCCESS
[java::java.lang.Class.<init>:()V.null-pointer-exception.2] line 387 Null pointer check: SUCCESS

java/lang/Class.java function java::java.lang.Class.cproverNondetInitialize:()V
[java::java.lang.Class.cproverNondetInitialize:()V.null-pointer-exception.1] line 454 Null pointer check: SUCCESS
[java::java.lang.Class.cproverNondetInitialize:()V.null-pointer-exception.2] line 455 Null pointer check: SUCCESS

java/lang/Class.java function java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;
[java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;.null-pointer-exception.1] line 114 Null pointer check: SUCCESS
[java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;.null-pointer-exception.2] line 115 Null pointer check: SUCCESS

java/lang/Exception.java function java::java.lang.Exception.<init>:(Ljava/lang/String;)V
[java::java.lang.Exception.<init>:(Ljava/lang/String;)V.null-pointer-exception.1] line 66 Null pointer check: SUCCESS

java/lang/IllegalArgumentException.java function java::java.lang.IllegalArgumentException.<init>:(Ljava/lang/String;)V
[java::java.lang.IllegalArgumentException.<init>:(Ljava/lang/String;)V.null-pointer-exception.1] line 35 Null pointer check: SUCCESS

java/lang/Long.java function java::java.lang.Long.<init>:(J)V
[java::java.lang.Long.<init>:(J)V.null-pointer-exception.1] line 827 Null pointer check: SUCCESS
[java::java.lang.Long.<init>:(J)V.null-pointer-exception.2] line 828 Null pointer check: SUCCESS

java/lang/Long.java function java::java.lang.Long.decode:(Ljava/lang/String;)Ljava/lang/Long;
[java::java.lang.Long.decode:(Ljava/lang/String;)Ljava/lang/Long;.null-pointer-exception.1] line 765 Null pointer check: SUCCESS
[java::java.lang.Long.decode:(Ljava/lang/String;)Ljava/lang/Long;.null-pointer-exception.2] line 766 Null pointer check: SUCCESS
[java::java.lang.Long.decode:(Ljava/lang/String;)Ljava/lang/Long;.null-pointer-exception.3] line 766 Null pointer check: SUCCESS
[java::java.lang.Long.decode:(Ljava/lang/String;)Ljava/lang/Long;.null-pointer-exception.4] line 776 Null pointer check: SUCCESS
[java::java.lang.Long.decode:(Ljava/lang/String;)Ljava/lang/Long;.null-pointer-exception.5] line 776 Null pointer check: SUCCESS
[java::java.lang.Long.decode:(Ljava/lang/String;)Ljava/lang/Long;.null-pointer-exception.6] line 780 Null pointer check: SUCCESS
[java::java.lang.Long.decode:(Ljava/lang/String;)Ljava/lang/Long;.null-pointer-exception.7] line 784 Null pointer check: SUCCESS
[java::java.lang.Long.decode:(Ljava/lang/String;)Ljava/lang/Long;.null-pointer-exception.8] line 784 Null pointer check: SUCCESS
[java::java.lang.Long.decode:(Ljava/lang/String;)Ljava/lang/Long;.null-pointer-exception.9] line 789 Null pointer check: SUCCESS
[java::java.lang.Long.decode:(Ljava/lang/String;)Ljava/lang/Long;.null-pointer-exception.10] line 789 Null pointer check: SUCCESS
[java::java.lang.Long.decode:(Ljava/lang/String;)Ljava/lang/Long;.null-pointer-exception.11] line 790 Null pointer check: SUCCESS
[java::java.lang.Long.decode:(Ljava/lang/String;)Ljava/lang/Long;.null-pointer-exception.12] line 790 Null pointer check: SUCCESS
[java::java.lang.Long.decode:(Ljava/lang/String;)Ljava/lang/Long;.null-pointer-exception.13] line 798 Null pointer check: SUCCESS
[java::java.lang.Long.decode:(Ljava/lang/String;)Ljava/lang/Long;.null-pointer-exception.14] line 806 Null pointer check: SUCCESS
[java::java.lang.Long.decode:(Ljava/lang/String;)Ljava/lang/Long;.null-pointer-exception.15] line 806 Null pointer check: SUCCESS
[java::java.lang.Long.decode:(Ljava/lang/String;)Ljava/lang/Long;.null-pointer-exception.16] line 806 Null pointer check: SUCCESS
[java::java.lang.Long.decode:(Ljava/lang/String;)Ljava/lang/Long;.null-pointer-exception.17] line 806 Null pointer check: SUCCESS

java/lang/Long.java function java::java.lang.Long.getLong:(Ljava/lang/String;)Ljava/lang/Long;
[java::java.lang.Long.getLong:(Ljava/lang/String;)Ljava/lang/Long;.1] line 992 no uncaught exception: SUCCESS

java/lang/Long.java function java::java.lang.Long.longValue:()J
[java::java.lang.Long.longValue:()J.null-pointer-exception.1] line 880 Null pointer check: SUCCESS

java/lang/Long.java function java::java.lang.Long.parseLong:(Ljava/lang/String;I)J
[java::java.lang.Long.parseLong:(Ljava/lang/String;I)J.null-pointer-exception.1] line 465 Null pointer check: SUCCESS
[java::java.lang.Long.parseLong:(Ljava/lang/String;I)J.null-pointer-exception.2] line 465 Null pointer check: SUCCESS
[java::java.lang.Long.parseLong:(Ljava/lang/String;I)J.null-pointer-exception.3] line 469 Null pointer check: SUCCESS
[java::java.lang.Long.parseLong:(Ljava/lang/String;I)J.null-pointer-exception.4] line 469 Null pointer check: SUCCESS
[java::java.lang.Long.parseLong:(Ljava/lang/String;I)J.null-pointer-exception.5] line 469 Null pointer check: SUCCESS
[java::java.lang.Long.parseLong:(Ljava/lang/String;I)J.null-pointer-exception.6] line 469 Null pointer check: SUCCESS
[java::java.lang.Long.parseLong:(Ljava/lang/String;I)J.null-pointer-exception.7] line 469 Null pointer check: SUCCESS
[java::java.lang.Long.parseLong:(Ljava/lang/String;I)J.null-pointer-exception.8] line 469 Null pointer check: SUCCESS
[java::java.lang.Long.parseLong:(Ljava/lang/String;I)J.null-pointer-exception.9] line 469 Null pointer check: SUCCESS
[java::java.lang.Long.parseLong:(Ljava/lang/String;I)J.null-pointer-exception.10] line 473 Null pointer check: SUCCESS
[java::java.lang.Long.parseLong:(Ljava/lang/String;I)J.null-pointer-exception.11] line 473 Null pointer check: SUCCESS
[java::java.lang.Long.parseLong:(Ljava/lang/String;I)J.null-pointer-exception.12] line 473 Null pointer check: SUCCESS
[java::java.lang.Long.parseLong:(Ljava/lang/String;I)J.null-pointer-exception.13] line 473 Null pointer check: SUCCESS
[java::java.lang.Long.parseLong:(Ljava/lang/String;I)J.null-pointer-exception.14] line 473 Null pointer check: SUCCESS
[java::java.lang.Long.parseLong:(Ljava/lang/String;I)J.null-pointer-exception.15] line 473 Null pointer check: SUCCESS
[java::java.lang.Long.parseLong:(Ljava/lang/String;I)J.null-pointer-exception.16] line 473 Null pointer check: SUCCESS
[java::java.lang.Long.parseLong:(Ljava/lang/String;I)J.null-pointer-exception.17] line 477 Null pointer check: SUCCESS
[java::java.lang.Long.parseLong:(Ljava/lang/String;I)J.null-pointer-exception.18] line 477 Null pointer check: SUCCESS
[java::java.lang.Long.parseLong:(Ljava/lang/String;I)J.null-pointer-exception.19] line 477 Null pointer check: SUCCESS
[java::java.lang.Long.parseLong:(Ljava/lang/String;I)J.null-pointer-exception.20] line 477 Null pointer check: SUCCESS
[java::java.lang.Long.parseLong:(Ljava/lang/String;I)J.null-pointer-exception.21] line 477 Null pointer check: SUCCESS
[java::java.lang.Long.parseLong:(Ljava/lang/String;I)J.null-pointer-exception.22] line 477 Null pointer check: SUCCESS

java/lang/Long.java function java::java.lang.Long.valueOf:(J)Ljava/lang/Long;
[java::java.lang.Long.valueOf:(J)Ljava/lang/Long;.null-pointer-exception.1] line 713 Null pointer check: SUCCESS

java/lang/Number.java function java::java.lang.Number.<init>:()V
[java::java.lang.Number.<init>:()V.null-pointer-exception.1] line 55 Null pointer check: SUCCESS

java/lang/NumberFormatException.java function java::java.lang.NumberFormatException.<init>:(Ljava/lang/String;)V
[java::java.lang.NumberFormatException.<init>:(Ljava/lang/String;)V.null-pointer-exception.1] line 37 Null pointer check: SUCCESS

java/lang/Object.java function java::java.lang.Object.<init>:()V
[java::java.lang.Object.<init>:()V.null-pointer-exception.1] line 40 Null pointer check: SUCCESS

java/lang/RuntimeException.java function java::java.lang.RuntimeException.<init>:(Ljava/lang/String;)V
[java::java.lang.RuntimeException.<init>:(Ljava/lang/String;)V.null-pointer-exception.1] line 36 Null pointer check: SUCCESS

java/lang/StringBuilder.java function java::java.lang.StringBuilder.append:(I)Ljava/lang/StringBuilder;
[java::java.lang.StringBuilder.append:(I)Ljava/lang/StringBuilder;.null-pointer-exception.1] line 295 Null pointer check: SUCCESS

java/lang/Throwable.java function java::java.lang.Throwable.<init>:(Ljava/lang/String;)V
[java::java.lang.Throwable.<init>:(Ljava/lang/String;)V.null-pointer-exception.2] line 201 Null pointer check: SUCCESS
[java::java.lang.Throwable.<init>:(Ljava/lang/String;)V.null-pointer-exception.1] line 280 Null pointer check: SUCCESS
[java::java.lang.Throwable.<init>:(Ljava/lang/String;)V.null-pointer-exception.3] line 282 Null pointer check: SUCCESS
VERIFICATION SUCCESSFUL

Activity

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

      Issue actions