JBMC does not support AtomicBoolean.

[ben-Draeger]

Observation: In the following java program:

import java.util.concurrent.atomic.AtomicBoolean;

    public class Simple {

        public static void main(String[] args) {

            AtomicBoolean b = new AtomicBoolean(true);
                        assert(b.get() == true);
        }                           

    }

JBMC fails to verify the assert() statement although the assertion obviously holds and executing the program with

java -ea Simple

Gives no Assertion violation in 100% of the cases.

Interpretation: Since the same program using a boolean verifies, my guess is that JBMC does not support AtomicBoolean. Is it possible to provide an annotated interface for this class to allow ModelChecking simple programs like this?

CBMC version: 5.95.1 Operating system: MS Windows 11 Enterprise Version 22H2, Build 22621.3447 Exact command line resulting in the issue: "C:\Program Files\cbmc\bin\jbmc.exe" Simple What behaviour did you expect: I would have expected the assertion to verify. What happened instead: JBMC reports a FAILURE.

[peterschrammel]

Two observations:

1. The command needs to be: jbmc Simple --classpath .:jbmc/lib/java-models-library/target/core-models.jar:jbmc/lib/java-models-library/target/cprover-api.jar
2. core-models.jar currently doesn't have AtomicBoolean. See https://github.com/diffblue/java-models-library/tree/sv-comp23. This class would need to be added from https://github.com/AdoptOpenJDK/openjdk-jdk8u/blob/master/jdk/src/share/classes/java/util/concurrent/atomic/AtomicBoolean.java and modified to replace low-level functionality in a JBMC-friendly way. Note that you can use functionality from https://github.com/diffblue/java-cprover-api/blob/master/src/main/java/org/cprover/CProver.java (e.g. nondeterminism and assumptions).