Skip to content

Commit 650d895

Browse files
committed
pointer encoding: tests changed
1 parent 43b8fd2 commit 650d895

File tree

3 files changed

+3
-3
lines changed

3 files changed

+3
-3
lines changed

jbmc/regression/jbmc/lambda-boxing/Boolean.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
BoxingLambda
33
--function BoxingLambda.testBoolean --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
\[java::BoxingLambda\.testBoolean:\(\)V\.assertion\.1\] line 73 assertion at file BoxingLambda\.java line 73 function java::BoxingLambda\.testBoolean:\(\)V bytecode-index 25: SUCCESS

jbmc/regression/jbmc/lambda-boxing/Float.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
BoxingLambda
33
--function BoxingLambda.testFloat --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
\[java::BoxingLambda\.testFloat:\(\)V\.assertion\.1\] line 125 assertion at file BoxingLambda\.java line 125 function java::BoxingLambda\.testFloat:\(\)V bytecode-index 27: SUCCESS

jbmc/regression/jbmc/lambda-boxing/Integer.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
BoxingLambda
33
--function BoxingLambda.testInteger --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
\[java::BoxingLambda\.testInteger:\(\)V\.assertion\.1\] line 138 assertion at file BoxingLambda\.java line 138 function java::BoxingLambda\.testInteger:\(\)V bytecode-index 26: SUCCESS

0 commit comments

Comments
 (0)