Skip to content

Add Null Support #143

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
rcosta358 wants to merge 13 commits into
base: main
Choose a base branch
from
Draft

Add Null Support #143

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
7a8de62
Add Null & Boxed Types Support
rcosta358 Feb 7, 2026
c2ae323
Add Tests
rcosta358 Feb 7, 2026
d73b81c
Minor Changes
rcosta358 Feb 7, 2026
f24dc28
Unused Imports
rcosta358 Feb 8, 2026
cb50d1e
Minor Improvements
rcosta358 Feb 10, 2026
65e938d
Merge branch 'main' into null-support
rcosta358 Feb 11, 2026
aef5189
Mark Uninitialized Fields as Null
rcosta358 Feb 12, 2026
e959ce6
Merge branch 'main' into null-support
rcosta358 Feb 12, 2026
4c4661c
Fix Merge
rcosta358 Feb 12, 2026
8998f23
Remove Boxed Types
rcosta358 Feb 13, 2026
d8e500d
Merge branch 'main' into null-support
rcosta358 Feb 13, 2026
31bd897
Change `CorrectNullChecks` Test
rcosta358 Feb 15, 2026
c739e5f
Remove Fields Implicit Null Refinement
rcosta358 Feb 15, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Remove Boxed Types
  • Loading branch information
@rcosta358
rcosta358 committed Feb 13, 2026
commit 8998f2380f264df511eea00461532fc57a0772e1
12 changes: 0 additions & 12 deletions liquidjava-example/src/main/java/testSuite/ErrorBoxedBoolean.java
View file
Open in desktop

This file was deleted.

12 changes: 0 additions & 12 deletions liquidjava-example/src/main/java/testSuite/ErrorBoxedDouble.java
View file
Open in desktop

This file was deleted.

12 changes: 0 additions & 12 deletions liquidjava-example/src/main/java/testSuite/ErrorBoxedInteger.java
View file
Open in desktop

This file was deleted.

18 changes: 9 additions & 9 deletions liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,10 +42,10 @@ public static void storeVariablesSubtypes(Context z3, List<RefinedVariable> vari
private static Expr<?> getExpr(Context z3, String name, CtTypeReference<?> type) {
String typeName = type.getQualifiedName();
return switch (typeName) {
case "int", "short", "java.lang.Integer", "java.lang.Short" -> z3.mkIntConst(name);
case "boolean", "java.lang.Boolean" -> z3.mkBoolConst(name);
case "long", "java.lang.Long" -> z3.mkRealConst(name);
case "float", "double", "java.lang.Float", "java.lang.Double" -> (FPExpr) z3.mkConst(name, z3.mkFPSort64());
case "int", "short" -> z3.mkIntConst(name);
case "boolean" -> z3.mkBoolConst(name);
case "long" -> z3.mkRealConst(name);
case "float", "double" -> (FPExpr) z3.mkConst(name, z3.mkFPSort64());
case "int[]" -> z3.mkArrayConst(name, z3.mkIntSort(), z3.mkIntSort());
default -> z3.mkConst(name, z3.mkUninterpretedSort(typeName));
};
Expand Down Expand Up @@ -81,11 +81,11 @@ private static void addBuiltinFunctions(Context z3, Map<String, FuncDecl<?>> fun

static Sort getSort(Context z3, String sort) {
return switch (sort) {
case "int", "short", "java.lang.Integer", "java.lang.Short" -> z3.getIntSort();
case "boolean", "java.lang.Boolean" -> z3.getBoolSort();
case "long", "java.lang.Long" -> z3.getRealSort();
case "float", "java.lang.Float" -> z3.mkFPSort32();
case "double", "java.lang.Double" -> z3.mkFPSortDouble();
case "int" -> z3.getIntSort();
case "boolean" -> z3.getBoolSort();
case "long" -> z3.getRealSort();
case "float" -> z3.mkFPSort32();
case "double" -> z3.mkFPSortDouble();
case "int[]" -> z3.mkArraySort(z3.mkIntSort(), z3.mkIntSort());
case "String" -> z3.getStringSort();
case "void" -> z3.mkUninterpretedSort("void");
Expand Down
Loading