diff --git a/jbmc/regression/jbmc/main-args-elements-non-null1/Main.class b/jbmc/regression/jbmc/main-args-elements-non-null1/Main.class new file mode 100644 index 00000000000..4734b3ec778 Binary files /dev/null and b/jbmc/regression/jbmc/main-args-elements-non-null1/Main.class differ diff --git a/jbmc/regression/jbmc/main-args-elements-non-null1/Main.java b/jbmc/regression/jbmc/main-args-elements-non-null1/Main.java new file mode 100644 index 00000000000..8a81ebbfed6 --- /dev/null +++ b/jbmc/regression/jbmc/main-args-elements-non-null1/Main.java @@ -0,0 +1,11 @@ +public class Main +{ + public static void main(String[] args) + { + if(args.length>1) + { + assert(args[0] != null); // must hold + assert(args[1] != null); // must hold + } + } +} diff --git a/jbmc/regression/jbmc/main-args-elements-non-null1/test.desc b/jbmc/regression/jbmc/main-args-elements-non-null1/test.desc new file mode 100644 index 00000000000..3866f268f76 --- /dev/null +++ b/jbmc/regression/jbmc/main-args-elements-non-null1/test.desc @@ -0,0 +1,8 @@ +CORE +Main.class + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/main-args-elements-non-null2/Main.class b/jbmc/regression/jbmc/main-args-elements-non-null2/Main.class new file mode 100644 index 00000000000..396d39badf4 Binary files /dev/null and b/jbmc/regression/jbmc/main-args-elements-non-null2/Main.class differ diff --git a/jbmc/regression/jbmc/main-args-elements-non-null2/Main.java b/jbmc/regression/jbmc/main-args-elements-non-null2/Main.java new file mode 100644 index 00000000000..498f6d43056 --- /dev/null +++ b/jbmc/regression/jbmc/main-args-elements-non-null2/Main.java @@ -0,0 +1,9 @@ +public class Main +{ + public static void main(String[] args) + { + if(args.length>0) { + assert(args[0] != null); // must not fail + } + } +} diff --git a/jbmc/regression/jbmc/main-args-elements-non-null2/test.desc b/jbmc/regression/jbmc/main-args-elements-non-null2/test.desc new file mode 100644 index 00000000000..3866f268f76 --- /dev/null +++ b/jbmc/regression/jbmc/main-args-elements-non-null2/test.desc @@ -0,0 +1,8 @@ +CORE +Main.class + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/main-args-non-null-with-function1/Main.class b/jbmc/regression/jbmc/main-args-non-null-with-function1/Main.class new file mode 100644 index 00000000000..53745bf4248 Binary files /dev/null and b/jbmc/regression/jbmc/main-args-non-null-with-function1/Main.class differ diff --git a/jbmc/regression/jbmc/main-args-non-null-with-function1/Main.java b/jbmc/regression/jbmc/main-args-non-null-with-function1/Main.java new file mode 100644 index 00000000000..3ecee27827a --- /dev/null +++ b/jbmc/regression/jbmc/main-args-non-null-with-function1/Main.java @@ -0,0 +1,7 @@ +public class Main +{ + public static void main(String[] args) + { + assert(args != null); // must hold + } +} diff --git a/jbmc/regression/jbmc/main-args-non-null-with-function1/test.desc b/jbmc/regression/jbmc/main-args-non-null-with-function1/test.desc new file mode 100644 index 00000000000..9e275150f52 --- /dev/null +++ b/jbmc/regression/jbmc/main-args-non-null-with-function1/test.desc @@ -0,0 +1,8 @@ +CORE +Main.class +--function Main.main +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/main-args-non-null1/Main.class b/jbmc/regression/jbmc/main-args-non-null1/Main.class new file mode 100644 index 00000000000..53745bf4248 Binary files /dev/null and b/jbmc/regression/jbmc/main-args-non-null1/Main.class differ diff --git a/jbmc/regression/jbmc/main-args-non-null1/Main.java b/jbmc/regression/jbmc/main-args-non-null1/Main.java new file mode 100644 index 00000000000..3ecee27827a --- /dev/null +++ b/jbmc/regression/jbmc/main-args-non-null1/Main.java @@ -0,0 +1,7 @@ +public class Main +{ + public static void main(String[] args) + { + assert(args != null); // must hold + } +} diff --git a/jbmc/regression/jbmc/main-args-non-null1/test.desc b/jbmc/regression/jbmc/main-args-non-null1/test.desc new file mode 100644 index 00000000000..3866f268f76 --- /dev/null +++ b/jbmc/regression/jbmc/main-args-non-null1/test.desc @@ -0,0 +1,8 @@ +CORE +Main.class + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/no-main-args-elements-maybe-null1/Main.class b/jbmc/regression/jbmc/no-main-args-elements-maybe-null1/Main.class new file mode 100644 index 00000000000..6e052a7f6f2 Binary files /dev/null and b/jbmc/regression/jbmc/no-main-args-elements-maybe-null1/Main.class differ diff --git a/jbmc/regression/jbmc/no-main-args-elements-maybe-null1/Main.java b/jbmc/regression/jbmc/no-main-args-elements-maybe-null1/Main.java new file mode 100644 index 00000000000..14e556fa2a2 --- /dev/null +++ b/jbmc/regression/jbmc/no-main-args-elements-maybe-null1/Main.java @@ -0,0 +1,8 @@ +public class Main +{ + static void main(String[] args) // not public! + { + if(args != null && args.length>0) + assert(args[0] != null); // allowed to fail + } +} diff --git a/jbmc/regression/jbmc/no-main-args-elements-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-args-elements-maybe-null1/test.desc new file mode 100644 index 00000000000..c23c81e2d8d --- /dev/null +++ b/jbmc/regression/jbmc/no-main-args-elements-maybe-null1/test.desc @@ -0,0 +1,8 @@ +CORE +Main.class +--function Main.main +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/Main.class b/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/Main.class new file mode 100644 index 00000000000..cd3d63768c1 Binary files /dev/null and b/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/Main.class differ diff --git a/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/Main.java b/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/Main.java new file mode 100644 index 00000000000..97ad6061c78 --- /dev/null +++ b/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/Main.java @@ -0,0 +1,9 @@ +public class Main +{ + static void main(String[] args) // not public! + { + if(args != null && args.length>0) { + assert(args[0] == null); // allowed to fail + } + } +} 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 new file mode 100644 index 00000000000..c23c81e2d8d --- /dev/null +++ b/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/test.desc @@ -0,0 +1,8 @@ +CORE +Main.class +--function Main.main +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/no-main-args-maybe-null1/Main.class b/jbmc/regression/jbmc/no-main-args-maybe-null1/Main.class new file mode 100644 index 00000000000..3131f084ffc Binary files /dev/null and b/jbmc/regression/jbmc/no-main-args-maybe-null1/Main.class differ diff --git a/jbmc/regression/jbmc/no-main-args-maybe-null1/Main.java b/jbmc/regression/jbmc/no-main-args-maybe-null1/Main.java new file mode 100644 index 00000000000..aa61bf38859 --- /dev/null +++ b/jbmc/regression/jbmc/no-main-args-maybe-null1/Main.java @@ -0,0 +1,7 @@ +public class Main +{ + public void main(String[] args) // not static! + { + assert(args != null); // allowed to fail + } +} diff --git a/jbmc/regression/jbmc/no-main-args-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-args-maybe-null1/test.desc new file mode 100644 index 00000000000..c23c81e2d8d --- /dev/null +++ b/jbmc/regression/jbmc/no-main-args-maybe-null1/test.desc @@ -0,0 +1,8 @@ +CORE +Main.class +--function Main.main +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/no-main-args-maybe-null2/Main.class b/jbmc/regression/jbmc/no-main-args-maybe-null2/Main.class new file mode 100644 index 00000000000..203057c9f92 Binary files /dev/null and b/jbmc/regression/jbmc/no-main-args-maybe-null2/Main.class differ diff --git a/jbmc/regression/jbmc/no-main-args-maybe-null2/Main.java b/jbmc/regression/jbmc/no-main-args-maybe-null2/Main.java new file mode 100644 index 00000000000..0fae3e13177 --- /dev/null +++ b/jbmc/regression/jbmc/no-main-args-maybe-null2/Main.java @@ -0,0 +1,7 @@ +public class Main +{ + public void main(String[] args) // not static! + { + assert(args == null); // allowed to fail + } +} diff --git a/jbmc/regression/jbmc/no-main-args-maybe-null2/test.desc b/jbmc/regression/jbmc/no-main-args-maybe-null2/test.desc new file mode 100644 index 00000000000..c23c81e2d8d --- /dev/null +++ b/jbmc/regression/jbmc/no-main-args-maybe-null2/test.desc @@ -0,0 +1,8 @@ +CORE +Main.class +--function Main.main +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/no-main-int-array-maybe-null1/Main.class b/jbmc/regression/jbmc/no-main-int-array-maybe-null1/Main.class new file mode 100644 index 00000000000..69f688d31f1 Binary files /dev/null and b/jbmc/regression/jbmc/no-main-int-array-maybe-null1/Main.class differ diff --git a/jbmc/regression/jbmc/no-main-int-array-maybe-null1/Main.java b/jbmc/regression/jbmc/no-main-int-array-maybe-null1/Main.java new file mode 100644 index 00000000000..956afcb9993 --- /dev/null +++ b/jbmc/regression/jbmc/no-main-int-array-maybe-null1/Main.java @@ -0,0 +1,16 @@ +public class Main +{ + public static void main(int[] args) + { + assert(args == null); // allowed to fail + assert(args != null); // allowed to fail + if(args != null && args.length > 0) { + try { + int i = args[0]; + } + catch(Exception e) { + assert false; // must hold + } + } + } +} diff --git a/jbmc/regression/jbmc/no-main-int-array-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-int-array-maybe-null1/test.desc new file mode 100644 index 00000000000..46abab6236b --- /dev/null +++ b/jbmc/regression/jbmc/no-main-int-array-maybe-null1/test.desc @@ -0,0 +1,12 @@ +CORE +Main.class +--function Main.main --java-throw-runtime-exceptions +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +assertion at file Main\.java line 5 function .* bytecode-index 6: FAILURE +assertion at file Main\.java line 6 function .* bytecode-index 14: FAILURE +assertion at file Main\.java line 12 function .* bytecode-index 31: SUCCESS +\*\* 2 of .* failed +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/Main.class b/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/Main.class new file mode 100644 index 00000000000..5a56689bdfb Binary files /dev/null and b/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/Main.class differ diff --git a/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/Main.java b/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/Main.java new file mode 100644 index 00000000000..7841b610d1f --- /dev/null +++ b/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/Main.java @@ -0,0 +1,11 @@ +public class Main +{ + public static void main(String[][] args) + { + assert(args == null || + args.length == 0 || + args[0] == null || + args[0].length == 0 || + args[0][0] != null); // allowed to fail + } +} diff --git a/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/test.desc new file mode 100644 index 00000000000..a631452f5f6 --- /dev/null +++ b/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/test.desc @@ -0,0 +1,10 @@ +CORE +Main.class +--function Main.main +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +assertion at file Main\.java line 5 function .* bytecode-index 24: FAILURE +\*\* 1 of .* failed +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/Main.class b/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/Main.class new file mode 100644 index 00000000000..ee7b474bda8 Binary files /dev/null and b/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/Main.class differ diff --git a/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/Main.java b/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/Main.java new file mode 100644 index 00000000000..cf11207135f --- /dev/null +++ b/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/Main.java @@ -0,0 +1,11 @@ +public class Main +{ + public static void main(String[][] args) + { + assert(args == null || + args.length == 0 || + args[0] == null || + args[0].length == 0 || + args[0][0] == null); // allowed to fail + } +} diff --git a/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/test.desc b/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/test.desc new file mode 100644 index 00000000000..a631452f5f6 --- /dev/null +++ b/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/test.desc @@ -0,0 +1,10 @@ +CORE +Main.class +--function Main.main +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +assertion at file Main\.java line 5 function .* bytecode-index 24: FAILURE +\*\* 1 of .* failed +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/Main.class b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/Main.class new file mode 100644 index 00000000000..3a9613e9e3c Binary files /dev/null and b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/Main.class differ diff --git a/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/Main.java b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/Main.java new file mode 100644 index 00000000000..f05363fe682 --- /dev/null +++ b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/Main.java @@ -0,0 +1,9 @@ +public class Main +{ + public static void main(Main[] args) + { + if(args != null && args.length > 0) { + assert(args[0] == null); // allowed to fail + } + } +} diff --git a/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/test.desc new file mode 100644 index 00000000000..49668103f1f --- /dev/null +++ b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/test.desc @@ -0,0 +1,10 @@ +CORE +Main.class +--function Main.main +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +assertion at file Main\.java line 12 function .* bytecode-index 15: FAILURE +\*\* 1 of .* failed +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/Main.class b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/Main.class new file mode 100644 index 00000000000..1f0d7a7f55d Binary files /dev/null and b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/Main.class differ diff --git a/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/Main.java b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/Main.java new file mode 100644 index 00000000000..2e8139a9e42 --- /dev/null +++ b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/Main.java @@ -0,0 +1,9 @@ +public class Main +{ + public static void main(Main[] args) + { + if(args != null && args.length > 0) { + assert(args[0] != null); // allowed to fail + } + } +} diff --git a/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/test.desc b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/test.desc new file mode 100644 index 00000000000..49668103f1f --- /dev/null +++ b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/test.desc @@ -0,0 +1,10 @@ +CORE +Main.class +--function Main.main +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +assertion at file Main\.java line 12 function .* bytecode-index 15: FAILURE +\*\* 1 of .* failed +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/no-main-object-array-maybe-null1/Main$A.class b/jbmc/regression/jbmc/no-main-object-array-maybe-null1/Main$A.class new file mode 100644 index 00000000000..47ea25c867b Binary files /dev/null and b/jbmc/regression/jbmc/no-main-object-array-maybe-null1/Main$A.class differ diff --git a/jbmc/regression/jbmc/no-main-object-array-maybe-null1/Main.class b/jbmc/regression/jbmc/no-main-object-array-maybe-null1/Main.class new file mode 100644 index 00000000000..a1dc746c063 Binary files /dev/null and b/jbmc/regression/jbmc/no-main-object-array-maybe-null1/Main.class differ diff --git a/jbmc/regression/jbmc/no-main-object-array-maybe-null1/Main.java b/jbmc/regression/jbmc/no-main-object-array-maybe-null1/Main.java new file mode 100644 index 00000000000..44b9b6e14f4 --- /dev/null +++ b/jbmc/regression/jbmc/no-main-object-array-maybe-null1/Main.java @@ -0,0 +1,18 @@ +public class Main +{ + public static class A { + int x; + } + public A a; + + public static void main(Main[] args) + { + assert(args != null); // allowed to fail + if(args != null && args.length > 0) { + Main m = args[0]; + if(m != null) { + assert(m.a == null); // allowed to fail + } + } + } +} diff --git a/jbmc/regression/jbmc/no-main-object-array-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-object-array-maybe-null1/test.desc new file mode 100644 index 00000000000..58989b56c0c --- /dev/null +++ b/jbmc/regression/jbmc/no-main-object-array-maybe-null1/test.desc @@ -0,0 +1,11 @@ +CORE +Main.class +--function Main.main +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +assertion at file Main\.java line 10 function .* bytecode-index 6: FAILURE +assertion at file Main\.java line 14 function .* bytecode-index 26: FAILURE +\*\* 2 of .* failed +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/no-main-object-array-maybe-null2/Main$A.class b/jbmc/regression/jbmc/no-main-object-array-maybe-null2/Main$A.class new file mode 100644 index 00000000000..47ea25c867b Binary files /dev/null and b/jbmc/regression/jbmc/no-main-object-array-maybe-null2/Main$A.class differ diff --git a/jbmc/regression/jbmc/no-main-object-array-maybe-null2/Main.class b/jbmc/regression/jbmc/no-main-object-array-maybe-null2/Main.class new file mode 100644 index 00000000000..59d39c36a21 Binary files /dev/null and b/jbmc/regression/jbmc/no-main-object-array-maybe-null2/Main.class differ diff --git a/jbmc/regression/jbmc/no-main-object-array-maybe-null2/Main.java b/jbmc/regression/jbmc/no-main-object-array-maybe-null2/Main.java new file mode 100644 index 00000000000..fd829647796 --- /dev/null +++ b/jbmc/regression/jbmc/no-main-object-array-maybe-null2/Main.java @@ -0,0 +1,18 @@ +public class Main +{ + public static class A { + int x; + } + public A a; + + public static void main(Main[] args) + { + assert(args != null); // allowed to fail + if(args != null && args.length > 0) { + Main m = args[0]; + if(m != null) { + assert(m.a != null); // allowed to fail + } + } + } +} diff --git a/jbmc/regression/jbmc/no-main-object-array-maybe-null2/test.desc b/jbmc/regression/jbmc/no-main-object-array-maybe-null2/test.desc new file mode 100644 index 00000000000..58989b56c0c --- /dev/null +++ b/jbmc/regression/jbmc/no-main-object-array-maybe-null2/test.desc @@ -0,0 +1,11 @@ +CORE +Main.class +--function Main.main +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +assertion at file Main\.java line 10 function .* bytecode-index 6: FAILURE +assertion at file Main\.java line 14 function .* bytecode-index 26: FAILURE +\*\* 2 of .* failed +-- +^warning: ignoring