diff --git a/Tests/A4/J1_7_Reachability_AfterIfWithWhileTrue.java b/Tests/A4/J1_7_Reachability_AfterIfWithWhileTrue.java
new file mode 100644
index 0000000000000000000000000000000000000000..d891a852a940cf819fa26a30c1e2cbed857c4012
--- /dev/null
+++ b/Tests/A4/J1_7_Reachability_AfterIfWithWhileTrue.java
@@ -0,0 +1,11 @@
+// REACHABILITY
+public class J1_7_Reachability_AfterIfWithWhileTrue {
+
+ public J1_7_Reachability_AfterIfWithWhileTrue () {}
+
+ public static int test() {
+ int x=123;
+ if (x==122) while (true);
+ return x;
+ }
+}
diff --git a/Tests/A4/J1_7_Reachability_EmptyVoidMethod.java b/Tests/A4/J1_7_Reachability_EmptyVoidMethod.java
new file mode 100644
index 0000000000000000000000000000000000000000..223e6bd8ae0619079733dc366510a1b7bf3e4ebf
--- /dev/null
+++ b/Tests/A4/J1_7_Reachability_EmptyVoidMethod.java
@@ -0,0 +1,11 @@
+// REACHABILITY
+
+public class J1_7_Reachability_EmptyVoidMethod {
+ public J1_7_Reachability_EmptyVoidMethod() {}
+
+ public void empty() {}
+
+ public static int test() {
+ return 123;
+ }
+}
diff --git a/Tests/A4/J1_7_Reachability_IfAndWhile_Return.java b/Tests/A4/J1_7_Reachability_IfAndWhile_Return.java
new file mode 100644
index 0000000000000000000000000000000000000000..47c9e090b7ad09a110cbd1baed5a8c14ad65fe9f
--- /dev/null
+++ b/Tests/A4/J1_7_Reachability_IfAndWhile_Return.java
@@ -0,0 +1,10 @@
+// REACHABILITY
+public class J1_7_Reachability_IfAndWhile_Return {
+ public J1_7_Reachability_IfAndWhile_Return() {}
+ public static int test() {
+ int x=121;
+ if (x==120) return x;
+ while (x==121) return x+2;
+ return x;
+ }
+}
diff --git a/Tests/A4/J1_7_Reachability_IfThenElse_InConstructor.java b/Tests/A4/J1_7_Reachability_IfThenElse_InConstructor.java
new file mode 100644
index 0000000000000000000000000000000000000000..759648a206257647804479dc49b6b7197c23df9a
--- /dev/null
+++ b/Tests/A4/J1_7_Reachability_IfThenElse_InConstructor.java
@@ -0,0 +1,12 @@
+// REACHABILITY
+
+public class J1_7_Reachability_IfThenElse_InConstructor {
+ public J1_7_Reachability_IfThenElse_InConstructor(boolean b) {
+ if (b) return;
+ else return;
+ }
+
+ public static int test() {
+ return 123;
+ }
+}
diff --git a/Tests/A4/J1_7_Reachability_IfThenElse_InValueMethod.java b/Tests/A4/J1_7_Reachability_IfThenElse_InValueMethod.java
new file mode 100644
index 0000000000000000000000000000000000000000..12db939e90325f4af4e1010a89df5d281f93d186
--- /dev/null
+++ b/Tests/A4/J1_7_Reachability_IfThenElse_InValueMethod.java
@@ -0,0 +1,14 @@
+// REACHABILITY
+
+public class J1_7_Reachability_IfThenElse_InValueMethod {
+ public J1_7_Reachability_IfThenElse_InValueMethod() {}
+
+ public int method(boolean b) {
+ if (b) return 42;
+ else return 123;
+ }
+
+ public static int test() {
+ return 123;
+ }
+}
diff --git a/Tests/A4/J1_7_Reachability_IfThenElse_InVoidMethod.java b/Tests/A4/J1_7_Reachability_IfThenElse_InVoidMethod.java
new file mode 100644
index 0000000000000000000000000000000000000000..c7a00c3f8236b1a2c9ea48809478e99e670169d1
--- /dev/null
+++ b/Tests/A4/J1_7_Reachability_IfThenElse_InVoidMethod.java
@@ -0,0 +1,14 @@
+// REACHABILITY
+
+public class J1_7_Reachability_IfThenElse_InVoidMethod {
+ public J1_7_Reachability_IfThenElse_InVoidMethod() {}
+
+ public void method(boolean b) {
+ if (b) return;
+ else return;
+ }
+
+ public static int test() {
+ return 123;
+ }
+}
diff --git a/Tests/A4/J1_7_Reachability_WhileTrue_ConstantFolding.java b/Tests/A4/J1_7_Reachability_WhileTrue_ConstantFolding.java
new file mode 100644
index 0000000000000000000000000000000000000000..74e6c646c816a97d0db1858d1cd597f90ed50b0a
--- /dev/null
+++ b/Tests/A4/J1_7_Reachability_WhileTrue_ConstantFolding.java
@@ -0,0 +1,19 @@
+// REACHABILITY
+/**
+ * Reachability:
+ * - If the body of a method whose return type is not void can
+ * complete normally, produce an error message.
+ *
+ * The condition (false || true) is constant folded into ABooleanConstExp, x, with x.value == true.
+ */
+public class J1_7_Reachability_WhileTrue_ConstantFolding {
+ public J1_7_Reachability_WhileTrue_ConstantFolding() {}
+
+ public int method() {
+ while (false || true) {}
+ }
+
+ public static int test() {
+ return 123;
+ }
+}
diff --git a/Tests/A4/J1_7_Unreachable_IfEqualsNot.java b/Tests/A4/J1_7_Unreachable_IfEqualsNot.java
new file mode 100644
index 0000000000000000000000000000000000000000..b93583d75a8202f78a6c03b3edcca7fd6c394799
--- /dev/null
+++ b/Tests/A4/J1_7_Unreachable_IfEqualsNot.java
@@ -0,0 +1,23 @@
+// REACHABILITY
+/**
+ * Reachability:
+ * - Check that all statements (including empty statements and empty
+ * blocks) are reachable.
+ */
+public class J1_7_Unreachable_IfEqualsNot {
+
+ public J1_7_Unreachable_IfEqualsNot(){}
+
+ public static int test(){
+ return J1_7_Unreachable_IfEqualsNot.bar(true);
+ }
+
+ public static int bar(boolean foo) {
+ if (foo == !foo) {
+ int h = 100;
+ return h;
+ }
+ return 123;
+ }
+
+}
diff --git a/Tests/A4/J1_Reachable1.java b/Tests/A4/J1_Reachable1.java
new file mode 100644
index 0000000000000000000000000000000000000000..778ac3ae21a1b37329364e4beb1f62142d3ab6af
--- /dev/null
+++ b/Tests/A4/J1_Reachable1.java
@@ -0,0 +1,15 @@
+// REACHABILITY
+public class J1_Reachable1 {
+ public J1_Reachable1(){}
+
+ public String test2() {
+ for (int i = 100; i < 50; i=i+1) {
+ i = i + 1;
+ }
+ return "";
+ }
+
+ public static int test() {
+ return 123;
+ }
+}
diff --git a/Tests/A4/J1_Reachable2.java b/Tests/A4/J1_Reachable2.java
new file mode 100644
index 0000000000000000000000000000000000000000..0c16e334ac46d18f5d516bf7d81352ec9a4cb451
--- /dev/null
+++ b/Tests/A4/J1_Reachable2.java
@@ -0,0 +1,13 @@
+// REACHABILITY
+public class J1_Reachable2 {
+
+ public J1_Reachable2(){}
+
+ public static int test() {
+ int i = 1;
+ ;;;
+ int j = 2;
+ return 120 + j + i;
+ }
+
+}
diff --git a/Tests/A4/J1_Reachable3.java b/Tests/A4/J1_Reachable3.java
new file mode 100644
index 0000000000000000000000000000000000000000..310b1d34360bde49314c08fd8685d56704d44186
--- /dev/null
+++ b/Tests/A4/J1_Reachable3.java
@@ -0,0 +1,17 @@
+// REACHABILITY
+public class J1_Reachable3 {
+
+ public J1_Reachable3(){}
+
+ public static int test() {
+ int h = 1;
+
+ {
+
+ }
+
+ int j = 2;
+ return 120 + j + h;
+ }
+
+}
diff --git a/Tests/A4/J1_Reachable4.java b/Tests/A4/J1_Reachable4.java
new file mode 100644
index 0000000000000000000000000000000000000000..04157d4a0bf922e2fe5303b05bdb0e5f7fb02462
--- /dev/null
+++ b/Tests/A4/J1_Reachable4.java
@@ -0,0 +1,10 @@
+// REACHABILITY
+public class J1_Reachable4 {
+ public J1_Reachable4(){}
+
+ public static int test() {
+ int x = 1;
+ if (false) { x=3; }
+ return 122 + x;
+ }
+}
diff --git a/Tests/A4/J1_Unreachable.java b/Tests/A4/J1_Unreachable.java
new file mode 100644
index 0000000000000000000000000000000000000000..18896b6bd73369902e35be5293dcfa5af32b273d
--- /dev/null
+++ b/Tests/A4/J1_Unreachable.java
@@ -0,0 +1,15 @@
+// REACHABILITY
+public class J1_Unreachable {
+
+ public J1_Unreachable(){}
+
+ public static int test() {
+ String foo = "foo";
+ String bar = "bar";
+
+ for (int i = 100; foo.equals((Object) bar); i=i+1) {
+ i = i + 1;
+ }
+ return 123;
+ }
+}
diff --git a/Tests/A4/J1_arbitraryreturn.java b/Tests/A4/J1_arbitraryreturn.java
new file mode 100644
index 0000000000000000000000000000000000000000..0b37a163768882f98d5cb04b80c94ea7fb890b38
--- /dev/null
+++ b/Tests/A4/J1_arbitraryreturn.java
@@ -0,0 +1,21 @@
+// REACHABILITY
+public class J1_arbitraryreturn {
+ public J1_arbitraryreturn() {}
+ public int m(int x) {
+ if (x==42)
+ return 123;
+ else
+ return 117;
+ }
+ public static int test() {
+ J1_arbitraryreturn obj = new J1_arbitraryreturn();
+ int y = obj.m(42);
+ if (y!=123) {
+ return 42;
+ }
+ else {
+ return y;
+ }
+ }
+}
+
diff --git a/Tests/A4/J1_defasn_use_before_declare.java b/Tests/A4/J1_defasn_use_before_declare.java
new file mode 100644
index 0000000000000000000000000000000000000000..6061d3840e3303d15fd0658d8e82436404d843f9
--- /dev/null
+++ b/Tests/A4/J1_defasn_use_before_declare.java
@@ -0,0 +1,12 @@
+// DEFINITE_ASSIGNMENT
+public class J1_defasn_use_before_declare {
+ public J1_defasn_use_before_declare() {}
+ public static int test() {return new J1_defasn_use_before_declare().foo();}
+
+ protected int a = 23;
+ public int foo() {
+ int tmp = a;
+ int a = 100;
+ return a+tmp;
+ }
+}
diff --git a/Tests/A4/J1_ifThenElse.java b/Tests/A4/J1_ifThenElse.java
new file mode 100644
index 0000000000000000000000000000000000000000..505becdfdb7e892a0547d8d92a0ef64c8ae56778
--- /dev/null
+++ b/Tests/A4/J1_ifThenElse.java
@@ -0,0 +1,23 @@
+// PARSER_WEEDER,REACHABILITY
+public class J1_ifThenElse {
+
+ public J1_ifThenElse () {
+
+ }
+
+ public static int test() {
+ if (true)
+ if (false) {
+ return 7;
+ }
+ else {
+ return 123;
+ }
+ else
+ return 7;
+ }
+
+ public static void main(String[] args) {
+ System.out.println(J1_ifThenElse.test());
+ }
+}
diff --git a/Tests/A4/J1_if_then.java b/Tests/A4/J1_if_then.java
new file mode 100644
index 0000000000000000000000000000000000000000..5cc1bc2c003d32001d5c36829bbd42e23d10c144
--- /dev/null
+++ b/Tests/A4/J1_if_then.java
@@ -0,0 +1,11 @@
+// PARSER_WEEDER,REACHABILITY
+public class J1_if_then {
+
+ public J1_if_then() {}
+
+ public static int test() {
+ if (true)
+ return 123;
+ return 7;
+ }
+}
diff --git a/Tests/A4/J1_multipleReturn.java b/Tests/A4/J1_multipleReturn.java
new file mode 100644
index 0000000000000000000000000000000000000000..f12f64f1bc54f7b6b0a19e7335669e18206f0c25
--- /dev/null
+++ b/Tests/A4/J1_multipleReturn.java
@@ -0,0 +1,19 @@
+// REACHABILITY
+public class J1_multipleReturn {
+
+ public J1_multipleReturn () {}
+
+ public static int test() {
+ return new J1_multipleReturn().foo(-1) + new J1_multipleReturn().foo(1);
+ }
+
+
+ public int foo(int j) {
+ if (j <= 0) {
+ return 27;
+ }
+ else {
+ return 96;
+ }
+ }
+}
diff --git a/Tests/A4/J1_omittedvoidreturn.java b/Tests/A4/J1_omittedvoidreturn.java
new file mode 100644
index 0000000000000000000000000000000000000000..402a8c669317e8df398d564ca1ebd1add10da6b1
--- /dev/null
+++ b/Tests/A4/J1_omittedvoidreturn.java
@@ -0,0 +1,14 @@
+// REACHABILITY
+public class J1_omittedvoidreturn {
+ public J1_omittedvoidreturn() {}
+ public int y;
+ public void m() {
+ this.y = 17;
+ // return;
+ }
+ public static int test() {
+ J1_omittedvoidreturn obj = new J1_omittedvoidreturn();
+ obj.m();
+ return obj.y+106;
+ }
+}
diff --git a/Tests/A4/J1_reachability_return/Main.java b/Tests/A4/J1_reachability_return/Main.java
new file mode 100644
index 0000000000000000000000000000000000000000..de4036f8c785da018cc5e2ca64b8934c05a65c2b
--- /dev/null
+++ b/Tests/A4/J1_reachability_return/Main.java
@@ -0,0 +1,35 @@
+// REACHABILITY
+import java.util.Random;
+
+public class Main {
+
+ public Random random = new Random();
+
+ public Main () {}
+
+ public void m() {
+ if (random.nextBoolean()) {
+ System.out.println("then branch completes normally!");
+ }
+ else {
+ return;
+ }
+ }
+
+ public void m1() {
+ if (random.nextBoolean()) {
+ return;
+ }
+ else {
+ return;
+ }
+ }
+
+ public static int test() {
+ Main j = new Main();
+ j.m();
+ j.m1();
+ return 123;
+ }
+
+}
diff --git a/Tests/A4/J1_reachability_return/java/util/Random.java b/Tests/A4/J1_reachability_return/java/util/Random.java
new file mode 100644
index 0000000000000000000000000000000000000000..1158fcc10033d13c0ba2c880df7957156a4d50ed
--- /dev/null
+++ b/Tests/A4/J1_reachability_return/java/util/Random.java
@@ -0,0 +1,8 @@
+package java.util;
+public class Random {
+ public Random() {
+ }
+ public boolean nextBoolean() {
+ return true;
+ }
+}
diff --git a/Tests/A4/J1_reachableIfBody.java b/Tests/A4/J1_reachableIfBody.java
new file mode 100644
index 0000000000000000000000000000000000000000..e33153e3e564161e76edd192ddcbf51b7d56188b
--- /dev/null
+++ b/Tests/A4/J1_reachableIfBody.java
@@ -0,0 +1,12 @@
+// REACHABILITY
+public class J1_reachableIfBody {
+
+ public J1_reachableIfBody () {}
+
+ public static int test() {
+ if (false)
+ return 7;
+ return 123;
+ }
+
+}
diff --git a/Tests/A4/J1_unreachableAutomation.java b/Tests/A4/J1_unreachableAutomation.java
new file mode 100644
index 0000000000000000000000000000000000000000..7fc99c4a6a7d10de76221ec4bf15892af313fad3
--- /dev/null
+++ b/Tests/A4/J1_unreachableAutomation.java
@@ -0,0 +1,16 @@
+// REACHABILITY
+public class J1_unreachableAutomation {
+
+ public J1_unreachableAutomation () {}
+
+ public static int test() {
+ int x = 1135104544;
+ while (1184>x) {
+ return 7;
+ }
+ String s1 = "foo97";
+ return 123;
+ }
+
+
+}
diff --git a/Tests/A4/J1_while1.java b/Tests/A4/J1_while1.java
new file mode 100644
index 0000000000000000000000000000000000000000..184fe77c0cb3af1877fec55884cf7f1cd1f174d5
--- /dev/null
+++ b/Tests/A4/J1_while1.java
@@ -0,0 +1,13 @@
+// REACHABILITY,CODE_GENERATION
+public class J1_while1 {
+ public J1_while1() {}
+ public int m(int x) {
+ while (x>0) x=x-1;
+ return x;
+ }
+ public static int test() {
+ return new J1_while1().m(17)+123;
+ }
+}
+
+
diff --git a/Tests/A4/J1_while2.java b/Tests/A4/J1_while2.java
new file mode 100644
index 0000000000000000000000000000000000000000..d06992cf487d5520e7b7bf02e19b69715baf9219
--- /dev/null
+++ b/Tests/A4/J1_while2.java
@@ -0,0 +1,17 @@
+// REACHABILITY,CODE_GENERATION
+public class J1_while2 {
+ public J1_while2() {}
+ public int m(int x) {
+ while (x>0) {
+ int y = x;
+ y=y-1;
+ x = y;
+ };
+ return x;
+ }
+ public static int test() {
+ return new J1_while2().m(17)+123;
+ }
+}
+
+
diff --git a/Tests/A4/J1_whiletrue1.java b/Tests/A4/J1_whiletrue1.java
new file mode 100644
index 0000000000000000000000000000000000000000..4edf6368696587cd210edbc4b68b3a86de498b57
--- /dev/null
+++ b/Tests/A4/J1_whiletrue1.java
@@ -0,0 +1,11 @@
+// REACHABILITY,CODE_GENERATION
+public class J1_whiletrue1 {
+ public J1_whiletrue1() { }
+ public static int test() {
+ return 123;
+ }
+ public static void foo() {
+ while(true);
+ }
+
+}
diff --git a/Tests/A4/Je_7_DefiniteAssignment_2LazyOr_Assignment.java b/Tests/A4/Je_7_DefiniteAssignment_2LazyOr_Assignment.java
new file mode 100644
index 0000000000000000000000000000000000000000..1b8c7a69f58da87b6fb615db68ba2bb7cdba857e
--- /dev/null
+++ b/Tests/A4/Je_7_DefiniteAssignment_2LazyOr_Assignment.java
@@ -0,0 +1,18 @@
+// JOOS1:DEFINITE_ASSIGNMENT,JOOS1_OMITTED_LOCAL_INITIALIZER
+// JOOS2:DEFINITE_ASSIGNMENT,VARIABLE_MIGHT_NOT_HAVE_BEEN_INITIALIZED
+// JAVAC:UNKNOWN
+
+public class Je_7_DefiniteAssignment_2LazyOr_Assignment {
+ public Je_7_DefiniteAssignment_2LazyOr_Assignment() {}
+
+ public boolean method() {
+ boolean j;
+ boolean i;
+ if ((j=false) || (i=true));
+ return i;
+ }
+
+ public static int test() {
+ return 123;
+ }
+}
diff --git a/Tests/A4/Je_7_DefiniteAssignment_3LazyOr_Assignment.java b/Tests/A4/Je_7_DefiniteAssignment_3LazyOr_Assignment.java
new file mode 100644
index 0000000000000000000000000000000000000000..d266e04ddab54cb6e598d9429158b453e6f8459a
--- /dev/null
+++ b/Tests/A4/Je_7_DefiniteAssignment_3LazyOr_Assignment.java
@@ -0,0 +1,19 @@
+// JOOS1:DEFINITE_ASSIGNMENT,JOOS1_OMITTED_LOCAL_INITIALIZER
+// JOOS2:DEFINITE_ASSIGNMENT,VARIABLE_MIGHT_NOT_HAVE_BEEN_INITIALIZED
+// JAVAC:UNKNOWN
+
+public class Je_7_DefiniteAssignment_3LazyOr_Assignment {
+ public Je_7_DefiniteAssignment_3LazyOr_Assignment() {}
+
+ public boolean method() {
+ boolean a;
+ boolean b;
+ boolean c;
+ boolean d=(a=false) || ((b=false) || (c=false));
+ return c;
+ }
+
+ public static int test() {
+ return 123;
+ }
+}
diff --git a/Tests/A4/Je_7_Reachability_AfterElseReturn.java b/Tests/A4/Je_7_Reachability_AfterElseReturn.java
new file mode 100644
index 0000000000000000000000000000000000000000..fb300ecf0a61a45950e235830cb916ec95363c0b
--- /dev/null
+++ b/Tests/A4/Je_7_Reachability_AfterElseReturn.java
@@ -0,0 +1,26 @@
+// JOOS1:REACHABILITY,UNREACHABLE_STATEMENT
+// JOOS2:REACHABILITY,UNREACHABLE_STATEMENT
+// JAVAC:UNKNOWN
+//
+/**
+ * Reachability:
+ * - Check that all statements (including empty statements and empty
+ * blocks) are reachable.
+ */
+public class Je_7_Reachability_AfterElseReturn {
+
+ public Je_7_Reachability_AfterElseReturn () {}
+
+ public static int test(int j) {
+ if (j == 0) {
+ return 7;
+ }
+ else {
+ int k = 6;
+ return j;
+ int l = 9;
+ }
+ return 123;
+ }
+
+}
diff --git a/Tests/A4/Je_7_Reachability_AfterIfReturn.java b/Tests/A4/Je_7_Reachability_AfterIfReturn.java
new file mode 100644
index 0000000000000000000000000000000000000000..39735db9e5038117086983b11d0fb6e773aad4d5
--- /dev/null
+++ b/Tests/A4/Je_7_Reachability_AfterIfReturn.java
@@ -0,0 +1,22 @@
+// JOOS1:REACHABILITY,UNREACHABLE_STATEMENT
+// JOOS2:REACHABILITY,UNREACHABLE_STATEMENT
+// JAVAC:UNKNOWN
+//
+/**
+ * Reachability:
+ * - Check that all statements (including empty statements and empty
+ * blocks) are reachable.
+ */
+public class Je_7_Reachability_AfterIfReturn {
+
+ public Je_7_Reachability_AfterIfReturn () {}
+
+ public static int test(int j) {
+ if (j == 0) {
+ return 7;
+ int l = 9;
+ }
+ return 123;
+ }
+
+}
diff --git a/Tests/A4/Je_7_Reachability_AfterIfReturnElseReturn.java b/Tests/A4/Je_7_Reachability_AfterIfReturnElseReturn.java
new file mode 100644
index 0000000000000000000000000000000000000000..15048de94f9ecfcd6523a1f9185b208b1044417e
--- /dev/null
+++ b/Tests/A4/Je_7_Reachability_AfterIfReturnElseReturn.java
@@ -0,0 +1,24 @@
+// JOOS1:REACHABILITY,UNREACHABLE_STATEMENT
+// JOOS2:REACHABILITY,UNREACHABLE_STATEMENT
+// JAVAC:UNKNOWN
+//
+/**
+ * Reachability:
+ * - Check that all statements (including empty statements and empty
+ * blocks) are reachable.
+ */
+public class Je_7_Reachability_AfterIfReturnElseReturn {
+
+ public Je_7_Reachability_AfterIfReturnElseReturn () {}
+
+ public static int test(int j) {
+ if (j == 0)
+ return 7;
+ else
+ return j;
+
+ int i = 8;
+ return 123;
+ }
+
+}
diff --git a/Tests/A4/Je_7_Reachability_AfterReturnEmptyBlock.java b/Tests/A4/Je_7_Reachability_AfterReturnEmptyBlock.java
new file mode 100644
index 0000000000000000000000000000000000000000..8345004bb1de06a67e635d992e1ac0438bca91a1
--- /dev/null
+++ b/Tests/A4/Je_7_Reachability_AfterReturnEmptyBlock.java
@@ -0,0 +1,19 @@
+// JOOS1:REACHABILITY,UNREACHABLE_STATEMENT
+// JOOS2:REACHABILITY,UNREACHABLE_STATEMENT
+// JAVAC:UNKNOWN
+//
+/**
+ * Reachability:
+ * - Check that all statements (including empty statements and empty
+ * blocks) are reachable.
+ */
+public class Je_7_Reachability_AfterReturnEmptyBlock {
+
+ public Je_7_Reachability_AfterReturnEmptyBlock () {}
+
+ public static int test(int j) {
+ return 123;
+ {}
+ }
+
+}
diff --git a/Tests/A4/Je_7_Reachability_AfterReturn_Constructor.java b/Tests/A4/Je_7_Reachability_AfterReturn_Constructor.java
new file mode 100644
index 0000000000000000000000000000000000000000..bf7a1add9fba198e2d17e01396b006325a7f9f04
--- /dev/null
+++ b/Tests/A4/Je_7_Reachability_AfterReturn_Constructor.java
@@ -0,0 +1,21 @@
+// JOOS1:REACHABILITY,UNREACHABLE_STATEMENT
+// JOOS2:REACHABILITY,UNREACHABLE_STATEMENT
+// JAVAC:UNKNOWN
+//
+/**
+ * Reachability:
+ * -Check that all statements (including empty statements and empty
+ * blocks) are reachable.
+ */
+public class Je_7_Reachability_AfterReturn_Constructor {
+
+ public Je_7_Reachability_AfterReturn_Constructor() {
+ return;
+ Object a = new Object();
+ }
+
+ public static int test() {
+ return 123;
+ }
+
+}
diff --git a/Tests/A4/Je_7_Reachability_AfterValueReturn.java b/Tests/A4/Je_7_Reachability_AfterValueReturn.java
new file mode 100644
index 0000000000000000000000000000000000000000..960a24f77bfc60d79914c32a3705dd93306298b7
--- /dev/null
+++ b/Tests/A4/Je_7_Reachability_AfterValueReturn.java
@@ -0,0 +1,20 @@
+// JOOS1:REACHABILITY,UNREACHABLE_STATEMENT
+// JOOS2:REACHABILITY,UNREACHABLE_STATEMENT
+// JAVAC:UNKNOWN
+//
+/**
+ * Reachability:
+ * - Check that all statements (including empty statements and empty
+ * blocks) are reachable.
+ */
+public class Je_7_Reachability_AfterValueReturn {
+
+ public Je_7_Reachability_AfterValueReturn () {}
+
+ public static int test() {
+ return 7;
+ int i = 8;
+ return 123;
+ }
+
+}
diff --git a/Tests/A4/Je_7_Reachability_AfterVoidReturn.java b/Tests/A4/Je_7_Reachability_AfterVoidReturn.java
new file mode 100644
index 0000000000000000000000000000000000000000..ddba8cc57717005eeeceba0104e8aa82e5470173
--- /dev/null
+++ b/Tests/A4/Je_7_Reachability_AfterVoidReturn.java
@@ -0,0 +1,19 @@
+// JOOS1:REACHABILITY,UNREACHABLE_STATEMENT
+// JOOS2:REACHABILITY,UNREACHABLE_STATEMENT
+// JAVAC:UNKNOWN
+//
+/**
+ * Reachability:
+ * - Check that all statements (including empty statements and empty
+ * blocks) are reachable.
+ */
+public class Je_7_Reachability_AfterVoidReturn {
+
+ public Je_7_Reachability_AfterVoidReturn () {}
+
+ public static void test() {
+ return;
+ int i = 7;
+ }
+
+}
diff --git a/Tests/A4/Je_7_Reachability_EmptyValueMethod.java b/Tests/A4/Je_7_Reachability_EmptyValueMethod.java
new file mode 100644
index 0000000000000000000000000000000000000000..4672f04dff83ec35de072db40922e77f6434ba81
--- /dev/null
+++ b/Tests/A4/Je_7_Reachability_EmptyValueMethod.java
@@ -0,0 +1,13 @@
+// JOOS1:REACHABILITY,MISSING_RETURN_STATEMENT
+// JOOS2:REACHABILITY,MISSING_RETURN_STATEMENT
+// JAVAC:UNKNOWN
+
+public class Je_7_Reachability_EmptyValueMethod {
+ public Je_7_Reachability_EmptyValueMethod() {}
+
+ public int empty() {}
+
+ public static int test() {
+ return 123;
+ }
+}
diff --git a/Tests/A4/Je_7_Reachability_ForFalse_1.java b/Tests/A4/Je_7_Reachability_ForFalse_1.java
new file mode 100644
index 0000000000000000000000000000000000000000..f7fd9d285507a72aae889170fa5c8ac10d389540
--- /dev/null
+++ b/Tests/A4/Je_7_Reachability_ForFalse_1.java
@@ -0,0 +1,21 @@
+// JOOS1:REACHABILITY,UNREACHABLE_STATEMENT
+// JOOS2:REACHABILITY,UNREACHABLE_STATEMENT
+// JAVAC:UNKNOWN
+//
+/**
+ * Reachability:
+ * - Check that all statements (including empty statements and empty
+ * blocks) are reachable.
+ */
+public class Je_7_Reachability_ForFalse_1 {
+
+ public Je_7_Reachability_ForFalse_1(){}
+
+ public String test() {
+ for (int i = 100; 3 == (5+3*10); i=i+1) {
+ i = i + 1;
+ }
+ return "";
+ }
+
+}
diff --git a/Tests/A4/Je_7_Reachability_ForFalse_2.java b/Tests/A4/Je_7_Reachability_ForFalse_2.java
new file mode 100644
index 0000000000000000000000000000000000000000..54a614a0f33fd158fbed41e45dd846f5c6932c05
--- /dev/null
+++ b/Tests/A4/Je_7_Reachability_ForFalse_2.java
@@ -0,0 +1,21 @@
+// JOOS1:REACHABILITY,UNREACHABLE_STATEMENT
+// JOOS2:REACHABILITY,UNREACHABLE_STATEMENT
+// JAVAC:UNKNOWN
+//
+/**
+ * Reachability:
+ * - Check that all statements (including empty statements and empty
+ * blocks) are reachable.
+ */
+public class Je_7_Reachability_ForFalse_2 {
+
+ public Je_7_Reachability_ForFalse_2(){}
+
+ public static int test(){
+ for (int i = 0; false; i=i+1) {
+ i = i + 1;
+ }
+ return 123;
+ }
+}
+
diff --git a/Tests/A4/Je_7_Reachability_ReturnReturn.java b/Tests/A4/Je_7_Reachability_ReturnReturn.java
new file mode 100644
index 0000000000000000000000000000000000000000..48d261acf67af08ae70c086d25248a8232af1f94
--- /dev/null
+++ b/Tests/A4/Je_7_Reachability_ReturnReturn.java
@@ -0,0 +1,19 @@
+// JOOS1:REACHABILITY,UNREACHABLE_STATEMENT
+// JOOS2:REACHABILITY,UNREACHABLE_STATEMENT
+// JAVAC:UNKNOWN
+//
+/**
+ * Reachability:
+ * - Check that all statements (including empty statements and empty
+ * blocks) are reachable.
+ */
+public class Je_7_Reachability_ReturnReturn {
+
+ public Je_7_Reachability_ReturnReturn(){}
+
+ public static int test() {
+ return 123;
+ return 42;
+ }
+
+}
diff --git a/Tests/A4/Je_7_Reachability_WhileFalse_ConstantFolding.java b/Tests/A4/Je_7_Reachability_WhileFalse_ConstantFolding.java
new file mode 100644
index 0000000000000000000000000000000000000000..0de19be84854e90ff5e552593c85c3589913e5bf
--- /dev/null
+++ b/Tests/A4/Je_7_Reachability_WhileFalse_ConstantFolding.java
@@ -0,0 +1,23 @@
+// JOOS1:REACHABILITY,UNREACHABLE_STATEMENT
+// JOOS2:REACHABILITY,UNREACHABLE_STATEMENT
+// JAVAC:UNKNOWN
+//
+/**
+ * Reachability:
+ * - Check that all statements (including empty statements and empty
+ * blocks) are reachable.
+ *
+ * The condition (true && false) is constant folded into ABooleanConstExp, x, with x.value == false,
+ * but x.getBool() == null. See Util.makeBooleanConstExp().
+ */
+public class Je_7_Reachability_WhileFalse_ConstantFolding {
+ public Je_7_Reachability_WhileFalse_ConstantFolding() {}
+
+ public void method() {
+ while (true && false) {}
+ }
+
+ public static int test() {
+ return 123;
+ }
+}
diff --git a/Tests/A4/Je_7_Reachability_WhileFalse_Empty.java b/Tests/A4/Je_7_Reachability_WhileFalse_Empty.java
new file mode 100644
index 0000000000000000000000000000000000000000..713b71863d196e9497c5f57d1fe83143b2a9560d
--- /dev/null
+++ b/Tests/A4/Je_7_Reachability_WhileFalse_Empty.java
@@ -0,0 +1,18 @@
+// JOOS1:REACHABILITY,UNREACHABLE_STATEMENT
+// JOOS2:REACHABILITY,UNREACHABLE_STATEMENT
+// JAVAC:UNKNOWN
+//
+/**
+ * Reachability:
+ * - Check that all statements (including empty statements and empty
+ * blocks) are reachable.
+ */
+public class Je_7_Reachability_WhileFalse_Empty {
+
+ public Je_7_Reachability_WhileFalse_Empty() { }
+
+ public static int test() {
+ while(false);
+ return 123;
+ }
+}
diff --git a/Tests/A4/Je_7_Reachability_WhileFalse_IfThenElse.java b/Tests/A4/Je_7_Reachability_WhileFalse_IfThenElse.java
new file mode 100644
index 0000000000000000000000000000000000000000..89a4457094dacd0b7512a9cef9dc9eedca49e19d
--- /dev/null
+++ b/Tests/A4/Je_7_Reachability_WhileFalse_IfThenElse.java
@@ -0,0 +1,16 @@
+// JOOS1:REACHABILITY,UNREACHABLE_STATEMENT
+// JOOS2:REACHABILITY,UNREACHABLE_STATEMENT
+// JAVAC:UNKNOWN
+
+public class Je_7_Reachability_WhileFalse_IfThenElse {
+ public Je_7_Reachability_WhileFalse_IfThenElse() {}
+
+ public static int method(boolean b) {
+ while (false) if (b) return 42; else return 43;
+ return 123;
+ }
+
+ public static int test() {
+ return Je_7_Reachability_WhileFalse_IfThenElse.method(true);
+ }
+}
diff --git a/Tests/A4/Je_7_Reachability_WhileTrue.java b/Tests/A4/Je_7_Reachability_WhileTrue.java
new file mode 100644
index 0000000000000000000000000000000000000000..3a12604396704abdc637db0f9512dc462661a422
--- /dev/null
+++ b/Tests/A4/Je_7_Reachability_WhileTrue.java
@@ -0,0 +1,19 @@
+// JOOS1:REACHABILITY,UNREACHABLE_STATEMENT
+// JOOS2:REACHABILITY,UNREACHABLE_STATEMENT
+// JAVAC:UNKNOWN
+//
+/**
+ * Reachability:
+ * - Check that all statements (including empty statements and empty
+ * blocks) are reachable.
+ */
+public class Je_7_Reachability_WhileTrue {
+
+ public Je_7_Reachability_WhileTrue() {}
+
+ public static int test() {
+ while (true) { }
+ return 123;
+ }
+
+}
diff --git a/Tests/A4/Je_7_Reachability_WhileTrue_ConstantFolding.java b/Tests/A4/Je_7_Reachability_WhileTrue_ConstantFolding.java
new file mode 100644
index 0000000000000000000000000000000000000000..6aa67d4347cf2922784e5995ab0dd4da4ea94abb
--- /dev/null
+++ b/Tests/A4/Je_7_Reachability_WhileTrue_ConstantFolding.java
@@ -0,0 +1,23 @@
+// JOOS1:REACHABILITY,UNREACHABLE_STATEMENT
+// JOOS2:REACHABILITY,UNREACHABLE_STATEMENT
+// JAVAC:UNKNOWN
+//
+/**
+ * Reachability:
+ * - Check that all statements (including empty statements and empty
+ * blocks) are reachable.
+ *
+ * The condition (false || true) is constant folded into ABooleanConstExp, x, with x.value == true.
+ */
+public class Je_7_Reachability_WhileTrue_ConstantFolding {
+ public Je_7_Reachability_WhileTrue_ConstantFolding() {}
+
+ public void method() {
+ while (false || true) {}
+ return; // unreachable statement
+ }
+
+ public static int test() {
+ return 123;
+ }
+}
diff --git a/Tests/A4/Je_7_Return_IfElseIf.java b/Tests/A4/Je_7_Return_IfElseIf.java
new file mode 100644
index 0000000000000000000000000000000000000000..0971f4da762d894c8caf08883e3d9877439f6f4a
--- /dev/null
+++ b/Tests/A4/Je_7_Return_IfElseIf.java
@@ -0,0 +1,19 @@
+// JOOS1:REACHABILITY,MISSING_RETURN_STATEMENT
+// JOOS2:REACHABILITY,MISSING_RETURN_STATEMENT
+// JAVAC:UNKNOWN
+//
+/**
+ * Reachability:
+ * - If the body of a method whose return type is not void can
+ * complete normally, produce an error message.
+ */
+public class Je_7_Return_IfElseIf {
+
+ public Je_7_Return_IfElseIf(){}
+
+ public String test(int foo) {
+ if (foo == 1) return "1";
+ else if (foo == 2) return "2";
+ }
+
+}
diff --git a/Tests/A4/Je_7_Return_IfIfNoElseElse.java b/Tests/A4/Je_7_Return_IfIfNoElseElse.java
new file mode 100644
index 0000000000000000000000000000000000000000..8746a2f8fb2eb4b9507c1831fc5adc86a58a2850
--- /dev/null
+++ b/Tests/A4/Je_7_Return_IfIfNoElseElse.java
@@ -0,0 +1,31 @@
+// JOOS1:REACHABILITY,MISSING_RETURN_STATEMENT
+// JOOS2:REACHABILITY,MISSING_RETURN_STATEMENT
+// JAVAC:UNKNOWN
+//
+/**
+ * Reachability:
+ * - If the body of a method whose return type is not void can
+ * complete normally, produce an error message
+ */
+public class Je_7_Return_IfIfNoElseElse {
+
+ public Je_7_Return_IfIfNoElseElse () {}
+
+ public int m() {
+ boolean t = true;
+
+ if (t) {
+ if (t) {
+ return 117;
+ }
+ }
+ else {
+ return 42;
+ }
+ }
+
+ public static int test() {
+ return 123;
+ }
+
+}
diff --git a/Tests/A4/Je_7_Return_IfIfNot.java b/Tests/A4/Je_7_Return_IfIfNot.java
new file mode 100644
index 0000000000000000000000000000000000000000..b8793db8506dbfcb65a1dfe0949869e18e4cbe89
--- /dev/null
+++ b/Tests/A4/Je_7_Return_IfIfNot.java
@@ -0,0 +1,19 @@
+// JOOS1:REACHABILITY,MISSING_RETURN_STATEMENT
+// JOOS2:REACHABILITY,MISSING_RETURN_STATEMENT
+// JAVAC:UNKNOWN
+//
+/**
+ * Reachability:
+ * - If the body of a method whose return type is not void can
+ * complete normally, produce an error message.
+ */
+public class Je_7_Return_IfIfNot {
+
+ public Je_7_Return_IfIfNot(){}
+
+ public int test(boolean foo) {
+ if (foo) return 17;
+ if (!foo) return 42;
+ }
+
+}
diff --git a/Tests/A4/Je_7_Return_MissingInElse.java b/Tests/A4/Je_7_Return_MissingInElse.java
new file mode 100644
index 0000000000000000000000000000000000000000..def8ab4105aba1bdb3566e39623f87c36c7e7a34
--- /dev/null
+++ b/Tests/A4/Je_7_Return_MissingInElse.java
@@ -0,0 +1,22 @@
+// JOOS1:REACHABILITY,MISSING_RETURN_STATEMENT
+// JOOS2:REACHABILITY,MISSING_RETURN_STATEMENT
+// JAVAC:UNKNOWN
+//
+/**
+ * Reachability:
+ * - If the body of a method whose return type is not void can
+ * complete normally, produce an error message.
+ */
+public class Je_7_Return_MissingInElse {
+
+ public Je_7_Return_MissingInElse(){}
+
+ public String test(int foo) {
+ if (foo == 1) return "1";
+ else if (foo == 2) return "2";
+ else {
+ foo = 3;
+ }
+ }
+
+}
diff --git a/Tests/A4/Je_8_DefiniteAssignment_ArrayAssign.java b/Tests/A4/Je_8_DefiniteAssignment_ArrayAssign.java
new file mode 100644
index 0000000000000000000000000000000000000000..5a29a2bf3d201fab5d9db0591bbda23187eac383
--- /dev/null
+++ b/Tests/A4/Je_8_DefiniteAssignment_ArrayAssign.java
@@ -0,0 +1,23 @@
+// JOOS1: DEFINITE_ASSIGNMENT,JOOS1_OMITTED_LOCAL_INITIALIZER
+// JOOS2: DEFINITE_ASSIGNMENT,VARIABLE_MIGHT_NOT_HAVE_BEEN_INITIALIZED
+// JAVAC: UNKNOWN
+/**
+ * Definite Assignment
+ * - (Joos 1) A local variable declaration must have an initializer
+ * - (Joos 2) A local variable must be initialized before it is used.
+ *
+ * This testcase tests whether an array access lvalue is treated as a
+ * local variable in the analysis.
+ */
+public class Je_8_DefiniteAssignment_ArrayAssign{
+
+ public Je_8_DefiniteAssignment_ArrayAssign(){}
+
+ public static int test(){
+ int[] x;
+ x[0] = 7;
+ int [] y = x;
+ return 123;
+ }
+
+}
diff --git a/Tests/A4/Je_8_DefiniteAssignment_ArrayIndexAssign.java b/Tests/A4/Je_8_DefiniteAssignment_ArrayIndexAssign.java
new file mode 100644
index 0000000000000000000000000000000000000000..c3cb4131732d335d26eb39ab505f7d3e10d4d4f6
--- /dev/null
+++ b/Tests/A4/Je_8_DefiniteAssignment_ArrayIndexAssign.java
@@ -0,0 +1,22 @@
+// JOOS1: DEFINITE_ASSIGNMENT,JOOS1_OMITTED_LOCAL_INITIALIZER
+// JOOS2: DEFINITE_ASSIGNMENT,VARIABLE_MIGHT_NOT_HAVE_BEEN_INITIALIZED
+// JAVAC: UNKNOWN
+/**
+ * Definite Assignment
+ * - (Joos 1) A local variable declaration must have an initializer
+ * - (Joos 2) A local variable must be initialized before it is used.
+ *
+ * This testcase tests whether the compiler allows for an array index
+ * to be assigned to without the array being initialized.
+ */
+public class Je_8_DefiniteAssignment_ArrayIndexAssign{
+
+ public Je_8_DefiniteAssignment_ArrayIndexAssign(){}
+
+ public static int test(){
+ int[] x;
+ x[0] = 7;
+ return 123;
+ }
+
+}
diff --git a/Tests/A4/Je_8_DefiniteAssignment_ComplexInitializer.java b/Tests/A4/Je_8_DefiniteAssignment_ComplexInitializer.java
new file mode 100644
index 0000000000000000000000000000000000000000..86676cb8e541f3b7aea8d80a287717f437976857
--- /dev/null
+++ b/Tests/A4/Je_8_DefiniteAssignment_ComplexInitializer.java
@@ -0,0 +1,20 @@
+// JOOS1: DEFINITE_ASSIGNMENT,JOOS1_LOCAL_VARIABLE_IN_OWN_INITIALIZER
+// JOOS2: DEFINITE_ASSIGNMENT,VARIABLE_MIGHT_NOT_HAVE_BEEN_INITIALIZED
+// JAVAC: UNKNOWN
+/**
+ * DefiniteAssignment
+ * - (Joos 1) A local variable must not occur in its own initializer.
+ * - (Joos 2) Whenever a local variable is used in any context which
+ * is not the direct left-hand side of an assignment, it must be
+ * definitely assigned at that point in the program.
+ */
+public class Je_8_DefiniteAssignment_ComplexInitializer {
+
+ public Je_8_DefiniteAssignment_ComplexInitializer () {}
+
+ public static int test() {
+ int i = 1+i*2;
+ return 123;
+ }
+
+}
diff --git a/Tests/A4/Je_8_DefiniteAssignment_FalseAndAssignment.java b/Tests/A4/Je_8_DefiniteAssignment_FalseAndAssignment.java
new file mode 100644
index 0000000000000000000000000000000000000000..c067b88730740d8a526f225fe2c3840a5c67dbfc
--- /dev/null
+++ b/Tests/A4/Je_8_DefiniteAssignment_FalseAndAssignment.java
@@ -0,0 +1,21 @@
+// JOOS1: DEFINITE_ASSIGNMENT,JOOS1_OMITTED_LOCAL_INITIALIZER
+// JOOS2: DEFINITE_ASSIGNMENT,VARIABLE_MIGHT_NOT_HAVE_BEEN_INITIALIZED
+// JAVAC: UNKNOWN
+/**
+ * Definite Assignment:
+ * - (Joos 1) A local variable declaration must have an initializer.
+ * - (Joos 2) Whenever a local variable is used in any context which
+ * is not the direct left-hand side of an assignment, it must be
+ * definitely assigned at that point in the program. (a is not
+ * definitely assigned)
+ */
+public class Je_8_DefiniteAssignment_FalseAndAssignment {
+
+ public Je_8_DefiniteAssignment_FalseAndAssignment() {}
+
+ public static int test() {
+ int a;
+ if (false && (a = 2) == 2) {}
+ return a;
+ }
+}
diff --git a/Tests/A4/Je_8_DefiniteAssignment_FieldWithSameName.java b/Tests/A4/Je_8_DefiniteAssignment_FieldWithSameName.java
new file mode 100644
index 0000000000000000000000000000000000000000..e7442a54c2f7c17918392dc719625394cce22f35
--- /dev/null
+++ b/Tests/A4/Je_8_DefiniteAssignment_FieldWithSameName.java
@@ -0,0 +1,22 @@
+// JOOS1: DEFINITE_ASSIGNMENT,JOOS1_LOCAL_VARIABLE_IN_OWN_INITIALIZER
+// JOOS2: DEFINITE_ASSIGNMENT,VARIABLE_MIGHT_NOT_HAVE_BEEN_INITIALIZED
+// JAVAC: UNKNOWN
+/**
+ * DefiniteAssignment
+ * - (Joos 1) A local variable must not occur in its own initializer.
+ * - (Joos 2) Whenever a local variable is used in any context which
+ * is not the direct left-hand side of an assignment, it must be
+ * definitely assigned at that point in the program.
+ */
+public class Je_8_DefiniteAssignment_FieldWithSameName {
+
+ public int i;
+
+ public Je_8_DefiniteAssignment_FieldWithSameName () {}
+
+ public static int test() {
+ int i = 1+i*2;
+ return 123;
+ }
+
+}
diff --git a/Tests/A4/Je_8_DefiniteAssignment_IfIfNot.java b/Tests/A4/Je_8_DefiniteAssignment_IfIfNot.java
new file mode 100644
index 0000000000000000000000000000000000000000..05cdce46e441a56c9a94a04a135cd7297d030fdd
--- /dev/null
+++ b/Tests/A4/Je_8_DefiniteAssignment_IfIfNot.java
@@ -0,0 +1,27 @@
+// JOOS1: DEFINITE_ASSIGNMENT,JOOS1_OMITTED_LOCAL_INITIALIZER
+// JOOS2: DEFINITE_ASSIGNMENT,VARIABLE_MIGHT_NOT_HAVE_BEEN_INITIALIZED
+// JAVAC: UNKNOWN
+/**
+ * Definite Assignment:
+ * - (Joos 1) A local variable declaration must have an initializer.
+ * - (Joos 2) Whenever a local variable is used in any context which
+ * is not the direct left-hand side of an assignment, it must be
+ * definitely assigned at that point in the program. (a is not
+ * definitely assigned)
+ */
+public class Je_8_DefiniteAssignment_IfIfNot {
+
+ public Je_8_DefiniteAssignment_IfIfNot() {}
+
+ public static int test() {
+ int a;
+ boolean b = true;
+
+ if (b)
+ a = 123;
+ if (!b)
+ a = 42;
+
+ return a;
+ }
+}
diff --git a/Tests/A4/Je_8_DefiniteAssignment_InitToItself.java b/Tests/A4/Je_8_DefiniteAssignment_InitToItself.java
new file mode 100644
index 0000000000000000000000000000000000000000..69a3bbf082119c9e4ee9a31a4d5f2c361fc5a388
--- /dev/null
+++ b/Tests/A4/Je_8_DefiniteAssignment_InitToItself.java
@@ -0,0 +1,20 @@
+// JOOS1: DEFINITE_ASSIGNMENT,JOOS1_LOCAL_VARIABLE_IN_OWN_INITIALIZER
+// JOOS2: DEFINITE_ASSIGNMENT,VARIABLE_MIGHT_NOT_HAVE_BEEN_INITIALIZED
+// JAVAC: UNKNOWN
+/**
+ * Definite Assignment:
+ * - (Joos 1) A local variable must not occur in its own initializer.
+ * - (Joos 2) Whenever a local variable is used in any context which
+ * is not the direct left-hand side of an assignment, it must be
+ * definitely assigned at that point in the program. (a is not
+ * definitely assigned)
+ */
+public class Je_8_DefiniteAssignment_InitToItself {
+
+ public Je_8_DefiniteAssignment_InitToItself() {}
+
+ public static int test() {
+ int a = a;
+ return 123;
+ }
+}
diff --git a/Tests/A4/Je_8_DefiniteAssignment_SomethingAndAssignment.java b/Tests/A4/Je_8_DefiniteAssignment_SomethingAndAssignment.java
new file mode 100644
index 0000000000000000000000000000000000000000..cc7edef9e0f93d37d81eaf6e9d9ad42c97a9b11a
--- /dev/null
+++ b/Tests/A4/Je_8_DefiniteAssignment_SomethingAndAssignment.java
@@ -0,0 +1,26 @@
+// JOOS1: DEFINITE_ASSIGNMENT,JOOS1_OMITTED_LOCAL_INITIALIZER
+// JOOS2: DEFINITE_ASSIGNMENT,VARIABLE_MIGHT_NOT_HAVE_BEEN_INITIALIZED
+// JAVAC: UNKNOWN
+/**
+ * Definite Assignment:
+ * - (Joos 1) A local variable declaration must have an initializer.
+ * - (Joos 2) Whenever a local variable is used in any context which
+ * is not the direct left-hand side of an assignment, it must be
+ * definitely assigned at that point in the program. (a is not
+ * definitely assigned)
+ */
+public class Je_8_DefiniteAssignment_SomethingAndAssignment {
+
+ public Je_8_DefiniteAssignment_SomethingAndAssignment () {}
+
+ public static int test() {
+ boolean i;
+ boolean j = true;
+ if (j && (i=false)) {
+ j = false;
+ }
+ j = i;
+ return 123;
+ }
+
+}
diff --git a/Tests/A4/Je_8_DefiniteAssignment_SomethingOrAssignment.java b/Tests/A4/Je_8_DefiniteAssignment_SomethingOrAssignment.java
new file mode 100644
index 0000000000000000000000000000000000000000..2c3312d348852684cc8b53dab6a8e0890b99f3b0
--- /dev/null
+++ b/Tests/A4/Je_8_DefiniteAssignment_SomethingOrAssignment.java
@@ -0,0 +1,22 @@
+// JOOS1: DEFINITE_ASSIGNMENT,JOOS1_OMITTED_LOCAL_INITIALIZER
+// JOOS2: DEFINITE_ASSIGNMENT,VARIABLE_MIGHT_NOT_HAVE_BEEN_INITIALIZED
+// JAVAC: UNKNOWN
+/**
+ * Definite Assignment:
+ * - (Joos 1) A local variable declaration must have an initializer.
+ * - (Joos 2) Whenever a local variable is used in any context which
+ * is not the direct left-hand side of an assignment, it must be
+ * definitely assigned at that point in the program. (a is not
+ * definitely assigned)
+ */
+public class Je_8_DefiniteAssignment_SomethingOrAssignment {
+
+ public Je_8_DefiniteAssignment_SomethingOrAssignment() {}
+
+ public static int test() {
+ int a;
+ boolean t = false;
+ if (t || (a = 2) == 2) {}
+ return a;
+ }
+}
diff --git a/Tests/A4/Je_8_DefiniteAssignment_UninitializedExpInLvalue.java b/Tests/A4/Je_8_DefiniteAssignment_UninitializedExpInLvalue.java
new file mode 100644
index 0000000000000000000000000000000000000000..e2b0f000f85248cf052b1547c426224485b5aea7
--- /dev/null
+++ b/Tests/A4/Je_8_DefiniteAssignment_UninitializedExpInLvalue.java
@@ -0,0 +1,20 @@
+// JOOS1: DEFINITE_ASSIGNMENT,JOOS1_OMITTED_LOCAL_INITIALIZER
+// JOOS2: DEFINITE_ASSIGNMENT,VARIABLE_MIGHT_NOT_HAVE_BEEN_INITIALIZED
+// JAVAC: UNKNOWN
+/**
+ * Definite Assignment:
+ * - (Joos 1) A local variable must have an initalizer
+ * - (Joos 2) A local variable must be initialized before it is used.
+ */
+public class Je_8_DefiniteAssignment_UninitializedExpInLvalue{
+
+ public Je_8_DefiniteAssignment_UninitializedExpInLvalue(){}
+
+ public static int test(){
+ int[] z = new int[42];
+ int x; //Illegal joos1
+ z[x] = x = 123; //Illegal joos2
+ return x;
+ }
+
+}
diff --git a/Tests/A4/Je_8_DefiniteAssignment_UninitializedInNewArray.java b/Tests/A4/Je_8_DefiniteAssignment_UninitializedInNewArray.java
new file mode 100644
index 0000000000000000000000000000000000000000..d7b189e500a83e20ce7792159ee71d3f5176887e
--- /dev/null
+++ b/Tests/A4/Je_8_DefiniteAssignment_UninitializedInNewArray.java
@@ -0,0 +1,18 @@
+//JOOS1:DEFINITE_ASSIGNMENT,JOOS1_OMITTED_LOCAL_INITIALIZER
+//JOOS2:DEFINITE_ASSIGNMENT,VARIABLE_MIGHT_NOT_HAVE_BEEN_INITIALIZED
+//JAVAC:UNKNOWN
+
+public class Je_8_DefiniteAssignment_UninitializedInNewArray {
+
+ public Je_8_DefiniteAssignment_UninitializedInNewArray() {}
+
+ public int method() {
+ int[] a;
+ a = new int[a[1]];
+ return a[1];
+ }
+
+ public static int test() {
+ return 123;
+ }
+}
diff --git a/Tests/A4/Je_8_DefiniteAssignment_WhileFalse.java b/Tests/A4/Je_8_DefiniteAssignment_WhileFalse.java
new file mode 100644
index 0000000000000000000000000000000000000000..5bcd5adc41d74823bb7178dfcdb611189b1a5297
--- /dev/null
+++ b/Tests/A4/Je_8_DefiniteAssignment_WhileFalse.java
@@ -0,0 +1,26 @@
+// JOOS1: DEFINITE_ASSIGNMENT,JOOS1_OMITTED_LOCAL_INITIALIZER
+// JOOS2: DEFINITE_ASSIGNMENT,VARIABLE_MIGHT_NOT_HAVE_BEEN_INITIALIZED
+// JAVAC: UNKNOWN
+/**
+ * Definite Assignment:
+ * - (Joos 1) A local variable declaration must have an initializer.
+ * - (Joos 2) Whenever a local variable is used in any context which
+ * is not the direct left-hand side of an assignment, it must be
+ * definitely assigned at that point in the program. (a is not
+ * definitely assigned)
+ */
+public class Je_8_DefiniteAssignment_WhileFalse {
+
+ public Je_8_DefiniteAssignment_WhileFalse() {}
+
+ public static int test() {
+ int a;
+ boolean b = false;
+
+ while (b) {
+ a = 123;
+ }
+
+ return a;
+ }
+}
diff --git a/Tests/A4/Je_Widening.java b/Tests/A4/Je_Widening.java
new file mode 100644
index 0000000000000000000000000000000000000000..4b2968c6c69622d52791aa13112539729d13e14a
--- /dev/null
+++ b/Tests/A4/Je_Widening.java
@@ -0,0 +1,7 @@
+public class Je_Widening {
+ public static int test() {
+ char c = 'a' + 'b';
+ return 123;
+ }
+ public Je_Widening(){}
+}