Fixing long to char conversion

Author: VincenzoArceri

jlisa/java-testcases/svcomp/long1/Main.java

@@ -0,0 +1,27 @@
+/*
+ * Origin of the benchmark:
+ *     license: 4-clause BSD (see /java/jbmc-regression/LICENSE)
+ *     repo: https://github.com/diffblue/cbmc.git
+ *     branch: develop
+ *     directory: regression/cbmc-java/long1
+ * The benchmark was taken from the repo: 24 January 2018
+ */
+
+class Main {
+  public static void main(String[] args) {
+    long l = 4620693217682128896L;
+
+    // conversions
+    int i = (int) l;
+    char c = (char) l;
+    float f = l;
+    double d = l;
+    short s = (short) l;
+
+    if (i >= 0) assert (long) i == (l & 0x7fffffff);
+
+    if (c >= 0) assert (long) c == (l & 0x7fff);
+
+    if (s >= 0) assert (long) s == (l & 0x7fff);
+  }
+}

jlisa/java-testcases/svcomp/long1/report.json

@@ -0,0 +1,45 @@
+{
+  "warnings" : [ {
+    "message" : "['Main.java':21:16] on 'void Main::main(java.lang.String*[]* args)': [EXPRESSION] DEFINITE: the assertion holds"
+  }, {
+    "message" : "['Main.java':23:16] on 'void Main::main(java.lang.String*[]* args)': [EXPRESSION] DEFINITE: the assertion holds"
+  }, {
+    "message" : "['Main.java':25:16] on 'void Main::main(java.lang.String*[]* args)': [EXPRESSION] DEFINITE: the assertion holds"
+  } ],
+  "files" : [ "report.json", "void_Main.main(java.lang.String_[]__args).json" ],
+  "info" : {
+    "cfgs" : "13",
+    "duration" : "99ms",
+    "end" : "2025-10-08T12:11:19.446+02:00",
+    "expressions" : "80",
+    "files" : "1",
+    "globals" : "27",
+    "members" : "143",
+    "programs" : "1",
+    "start" : "2025-10-08T12:11:19.347+02:00",
+    "statements" : "34",
+    "units" : "48",
+    "version" : "0.1",
+    "warnings" : "3"
+  },
+  "configuration" : {
+    "analysisGraphs" : "NONE",
+    "descendingPhaseType" : "NONE",
+    "dumpForcesUnwinding" : "false",
+    "fixpointWorkingSet" : "OrderBasedWorkingSet",
+    "glbThreshold" : "5",
+    "hotspots" : "unset",
+    "jsonOutput" : "true",
+    "openCallPolicy" : "ReturnTopPolicy",
+    "optimize" : "false",
+    "recursionWideningThreshold" : "5",
+    "semanticChecks" : "AssertChecker",
+    "serializeInputs" : "false",
+    "serializeResults" : "true",
+    "shouldSmashError" : "unset",
+    "syntacticChecks" : "",
+    "useWideningPoints" : "true",
+    "wideningThreshold" : "5",
+    "workdir" : "java-outputs/svcomp/long1"
+  }
+}

jlisa/java-testcases/svcomp/long1/void_Main.main(java.lang.String_[]__args).json

@@ -82,6 +82,7 @@
 import it.unive.jlisa.program.operator.NaryExpression;
 import it.unive.jlisa.program.operator.NaryOperator;
 import it.unive.jlisa.program.type.JavaByteType;
+import it.unive.jlisa.program.type.JavaCharType;
 import it.unive.jlisa.program.type.JavaDoubleType;
 import it.unive.jlisa.program.type.JavaIntType;
 import it.unive.jlisa.program.type.JavaLongType;
@@ -1245,6 +1246,8 @@ else if (right.getValue() instanceof JavaLongType)
 				return new ConstantValue(((Number) left.getValue()).longValue());
 			else if (right.getValue() instanceof JavaDoubleType)
 				return new ConstantValue(((Number) left.getValue()).doubleValue());
+			else if (right.getValue() instanceof JavaCharType)
+				return new ConstantValue((int) (char) ((Number) left.getValue()).longValue());
 
 		return left;
 	}

jlisa/src/main/java/it/unive/jlisa/analysis/value/ConstantPropagation.java

@@ -442,4 +442,11 @@ public void swap1_test() throws IOException {
 				"Main.java");
 		perform(conf);
 	}
+
+	@Test
+	public void long1_test() throws IOException {
+		CronConfiguration conf = TestHelpers.assertCheckerWithConstantPropagation("svcomp", "long1",
+				"Main.java", "../common/");
+		perform(conf);
+	}
 }