From 5dd4167441628565eef89e53e9afb1884e8d7181 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 28 Jul 2026 22:48:33 +0000
Subject: [PATCH] OptionalInt model: of/empty/isPresent/isEmpty/getAsInt/orElse

Minimal executable model of java.util.OptionalInt: a (present, value)
pair with deterministic of()/empty() constructors, isPresent()/isEmpty()
accessors, getAsInt() throwing NoSuchElementException on the absent value
per the JDK contract, and orElse(int).

empty() deliberately allocates per call rather than caching a static
singleton as the JDK internals do: OptionalInt's javadoc explicitly
disclaims singleton-ness of empty() and forbids == comparison, so per-call
allocation is contract-conformant -- and a static object field (the first
in this model library) would become nondeterministic under JBMC's
--nondet-static, making empty().isPresent() spuriously satisfiable.

Carries the standard OpenJDK GPLv2+Classpath header, consistent with the
sibling java.util model files.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 src/main/java/java/util/OptionalInt.java | 78 ++++++++++++++++++++++++
 1 file changed, 78 insertions(+)
 create mode 100644 src/main/java/java/util/OptionalInt.java

diff --git a/src/main/java/java/util/OptionalInt.java b/src/main/java/java/util/OptionalInt.java
new file mode 100644
index 0000000..7a02f67
--- /dev/null
+++ b/src/main/java/java/util/OptionalInt.java
@@ -0,0 +1,78 @@
+/*
+ * Copyright (c) 2012, 2013, Oracle and/or its affiliates. All rights reserved.
+ * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.
+ *
+ * This code is free software; you can redistribute it and/or modify it
+ * under the terms of the GNU General Public License version 2 only, as
+ * published by the Free Software Foundation.  Oracle designates this
+ * particular file as subject to the "Classpath" exception as provided
+ * by Oracle in the LICENSE file that accompanied this code.
+ *
+ * This code is distributed in the hope that it will be useful, but WITHOUT
+ * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
+ * FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
+ * version 2 for more details (a copy is included in the LICENSE file that
+ * accompanied this code).
+ *
+ * You should have received a copy of the GNU General Public License version
+ * 2 along with this work; if not, write to the Free Software Foundation,
+ * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
+ *
+ * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA
+ * or visit www.oracle.com if you need additional information or have any
+ * questions.
+ */
+
+package java.util;
+
+/**
+ * JBMC model of java.util.OptionalInt.
+ * A simple value container: either empty or holds an int.
+ */
+public final class OptionalInt {
+    private final boolean isPresent;
+    private final int value;
+
+    private OptionalInt() {
+        this.isPresent = false;
+        this.value = 0;
+    }
+
+    private OptionalInt(int value) {
+        this.isPresent = true;
+        this.value = value;
+    }
+
+    public static OptionalInt empty() {
+        // DIFFBLUE MODEL LIBRARY Deliberately NOT a cached static singleton
+        // (unlike the JDK internals): OptionalInt's javadoc explicitly
+        // disclaims singleton-ness of empty() and forbids == comparison, so
+        // per-call allocation is contract-conformant -- and a static object
+        // field would become nondeterministic under JBMC's --nondet-static,
+        // making empty().isPresent() spuriously satisfiable.
+        return new OptionalInt();
+    }
+
+    public static OptionalInt of(int value) {
+        return new OptionalInt(value);
+    }
+
+    public boolean isPresent() {
+        return isPresent;
+    }
+
+    public boolean isEmpty() {
+        return !isPresent;
+    }
+
+    public int getAsInt() {
+        if (!isPresent) {
+            throw new NoSuchElementException("No value present");
+        }
+        return value;
+    }
+
+    public int orElse(int other) {
+        return isPresent ? value : other;
+    }
+}