pointer encoding: tests changed

kroening · kroening · commit b08c997d3e16 · 2022-04-28T23:00:18.000+01:00
diff --git a/jbmc/regression/jbmc-json-ui/pointer-simplification/test.desc b/jbmc/regression/jbmc-json-ui/pointer-simplification/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 test
 filter.jq --json-ui --trace
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-strings/StringFormatHex/test-hex-eval-upper.desc b/jbmc/regression/jbmc-strings/StringFormatHex/test-hex-eval-upper.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 Test
 --function Test.testHexEvalUpper --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --trace
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc-strings/StringFormatHex/test-hex-eval.desc b/jbmc/regression/jbmc-strings/StringFormatHex/test-hex-eval.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 Test
 --function Test.testHexEval --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --trace
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc-strings/char_escape/test.desc b/jbmc/regression/jbmc-strings/char_escape/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 Test
 --function Test.test --trace --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --json-ui
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc/address_space_size_limit1/test.desc b/jbmc/regression/jbmc/address_space_size_limit1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 Test
 --object-bits 4
 too many addressed objects
diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/class_assume.desc b/jbmc/regression/jbmc/assume-inputs-non-null/class_assume.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 My
 --function My.classArg --java-assume-inputs-non-null
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc/lambda-boxing/Boolean.desc b/jbmc/regression/jbmc/lambda-boxing/Boolean.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 BoxingLambda
 --function BoxingLambda.testBoolean --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 \[java::BoxingLambda\.testBoolean:\(\)V\.assertion\.1\] line 73 assertion at file BoxingLambda\.java line 73 function java::BoxingLambda\.testBoolean:\(\)V bytecode-index 25: SUCCESS
diff --git a/jbmc/regression/jbmc/lambda-boxing/Float.desc b/jbmc/regression/jbmc/lambda-boxing/Float.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 BoxingLambda
 --function BoxingLambda.testFloat --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 \[java::BoxingLambda\.testFloat:\(\)V\.assertion\.1\] line 125 assertion at file BoxingLambda\.java line 125 function java::BoxingLambda\.testFloat:\(\)V bytecode-index 27: SUCCESS
diff --git a/jbmc/regression/jbmc/lambda-boxing/Integer.desc b/jbmc/regression/jbmc/lambda-boxing/Integer.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 BoxingLambda
 --function BoxingLambda.testInteger --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 \[java::BoxingLambda\.testInteger:\(\)V\.assertion\.1\] line 138 assertion at file BoxingLambda\.java line 138 function java::BoxingLambda\.testInteger:\(\)V bytecode-index 26: SUCCESS
diff --git a/jbmc/regression/jbmc/lambda-void-return-type/test.desc b/jbmc/regression/jbmc/lambda-void-return-type/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 Test
 --function Test.test --classpath `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/test.desc b/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 Main
 --function Main.main
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc/string_field_aliasing/test.desc b/jbmc/regression/jbmc/string_field_aliasing/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 Cart
 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --trace --java-max-vla-length 96 --java-unwind-enum-static --max-nondet-string-length 200 --unwind 4 --function Cart.checkTax4 --string-printable
 ^EXIT=10$
diff --git a/jbmc/regression/strings-smoke-tests/java_parseint/test4.desc b/jbmc/regression/strings-smoke-tests/java_parseint/test4.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 Test4
 --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --function Test4.main --trace
 ^EXIT=10$
diff --git a/regression/cbmc-library/fprintf-01/test.desc b/regression/cbmc-library/fprintf-01/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$
diff --git a/regression/cbmc-library/free-01/test.desc b/regression/cbmc-library/free-01/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --pointer-check --bounds-check --stop-on-fail
-free argument must be NULL or valid pointer
+free argument must be (dynamic object|NULL or valid pointer)
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc-primitives/r_w_ok_bug/test.desc b/regression/cbmc-primitives/r_w_ok_bug/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --pointer-check --no-simplify --no-propagation
 ^\[main.pointer_dereference.\d+\] line 8 dereference failure: pointer outside object bounds in \*p1: FAILURE$
diff --git a/regression/cbmc-primitives/r_w_ok_inconsistent_invalid/test-no-cp.desc b/regression/cbmc-primitives/r_w_ok_inconsistent_invalid/test-no-cp.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --pointer-check --no-simplify --no-propagation
 ^EXIT=0$
diff --git a/regression/cbmc-primitives/r_w_ok_inconsistent_invalid/test.desc b/regression/cbmc-primitives/r_w_ok_inconsistent_invalid/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc-primitives/same-object-01/test-no-cp.desc b/regression/cbmc-primitives/same-object-01/test-no-cp.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --no-simplify --no-propagation
 ^EXIT=0$
diff --git a/regression/cbmc-primitives/same-object-01/test.desc b/regression/cbmc-primitives/same-object-01/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer_comparison1/main.c b/regression/cbmc/Pointer_comparison1/main.c
@@ -10,8 +10,7 @@ int main()
     return 0;
 
   if(
-    (unsigned long)p >
-    42) // unsoundly evaluates to true due to pointer encoding
+    (unsigned long)p > 1) // unsoundly evaluates to true due to pointer encoding
   {
     return 0;
   }
diff --git a/regression/cbmc/address_space_size_limit1/test.desc b/regression/cbmc/address_space_size_limit1/test.desc
@@ -1,4 +1,4 @@
-CORE thorough-paths broken-smt-backend
+KNOWNBUG thorough-paths broken-smt-backend
 test.c
 --no-simplify --unwind 300 --object-bits 8
 too many addressed objects
diff --git a/regression/cbmc/hex_trace/main.c b/regression/cbmc/hex_trace/main.c
@@ -6,6 +6,7 @@ int main()
   char *p;
 
   a = 0;
+  b = 0;
   a = -100;
   a = 2147483647;
   b = a * 2;
diff --git a/regression/cbmc/memory_allocation1/test.desc b/regression/cbmc/memory_allocation1/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+KNOWNBUG broken-smt-backend
 main.c
 --pointer-check
 ^EXIT=10$
diff --git a/regression/cbmc/mm_io1/test.desc b/regression/cbmc/mm_io1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/pointer-extra-checks/test.desc b/regression/cbmc/pointer-extra-checks/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --pointer-check
 ^EXIT=10$
diff --git a/regression/contracts/assigns-enforce-malloc-zero/test.desc b/regression/contracts/assigns-enforce-malloc-zero/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --enforce-contract foo _ --malloc-may-fail --malloc-fail-null
 ^\[foo.assigns.\d+\] line 9 Check that POINTER_OBJECT\(\(const void \*\)a\) is valid when a != \(\(char \*\)NULL\): SUCCESS$
diff --git a/regression/contracts/test_struct_member_enforce/test.desc b/regression/contracts/test_struct_member_enforce/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --enforce-contract foo
 ^EXIT=0$

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE`
	`1`	`+KNOWNBUG`
`2`	`2`	`test`
`3`	`3`	`filter.jq --json-ui --trace`
`4`	`4`	`^EXIT=0$`