From e94f3833a96035fd1da94dc3e241bc0b674df345 Mon Sep 17 00:00:00 2001
From: Xun Yang <x299yang@uwaterloo.ca>
Date: Sun, 8 Mar 2020 16:04:49 -0400
Subject: [PATCH] add a4 tests
---
...1_7_Reachability_AfterIfWithWhileTrue.java | 11 ++++++
.../A4/J1_7_Reachability_EmptyVoidMethod.java | 11 ++++++
.../J1_7_Reachability_IfAndWhile_Return.java | 10 ++++++
...Reachability_IfThenElse_InConstructor.java | 12 +++++++
...Reachability_IfThenElse_InValueMethod.java | 14 ++++++++
..._Reachability_IfThenElse_InVoidMethod.java | 14 ++++++++
...eachability_WhileTrue_ConstantFolding.java | 19 ++++++++++
Tests/A4/J1_7_Unreachable_IfEqualsNot.java | 23 ++++++++++++
Tests/A4/J1_Reachable1.java | 15 ++++++++
Tests/A4/J1_Reachable2.java | 13 +++++++
Tests/A4/J1_Reachable3.java | 17 +++++++++
Tests/A4/J1_Reachable4.java | 10 ++++++
Tests/A4/J1_Unreachable.java | 15 ++++++++
Tests/A4/J1_arbitraryreturn.java | 21 +++++++++++
Tests/A4/J1_defasn_use_before_declare.java | 12 +++++++
Tests/A4/J1_ifThenElse.java | 23 ++++++++++++
Tests/A4/J1_if_then.java | 11 ++++++
Tests/A4/J1_multipleReturn.java | 19 ++++++++++
Tests/A4/J1_omittedvoidreturn.java | 14 ++++++++
Tests/A4/J1_reachability_return/Main.java | 35 +++++++++++++++++++
.../java/util/Random.java | 8 +++++
Tests/A4/J1_reachableIfBody.java | 12 +++++++
Tests/A4/J1_unreachableAutomation.java | 16 +++++++++
Tests/A4/J1_while1.java | 13 +++++++
Tests/A4/J1_while2.java | 17 +++++++++
Tests/A4/J1_whiletrue1.java | 11 ++++++
...DefiniteAssignment_2LazyOr_Assignment.java | 18 ++++++++++
...DefiniteAssignment_3LazyOr_Assignment.java | 19 ++++++++++
.../A4/Je_7_Reachability_AfterElseReturn.java | 26 ++++++++++++++
Tests/A4/Je_7_Reachability_AfterIfReturn.java | 22 ++++++++++++
..._Reachability_AfterIfReturnElseReturn.java | 24 +++++++++++++
..._7_Reachability_AfterReturnEmptyBlock.java | 19 ++++++++++
..._Reachability_AfterReturn_Constructor.java | 21 +++++++++++
.../Je_7_Reachability_AfterValueReturn.java | 20 +++++++++++
.../A4/Je_7_Reachability_AfterVoidReturn.java | 19 ++++++++++
.../Je_7_Reachability_EmptyValueMethod.java | 13 +++++++
Tests/A4/Je_7_Reachability_ForFalse_1.java | 21 +++++++++++
Tests/A4/Je_7_Reachability_ForFalse_2.java | 21 +++++++++++
Tests/A4/Je_7_Reachability_ReturnReturn.java | 19 ++++++++++
...achability_WhileFalse_ConstantFolding.java | 23 ++++++++++++
.../Je_7_Reachability_WhileFalse_Empty.java | 18 ++++++++++
..._7_Reachability_WhileFalse_IfThenElse.java | 16 +++++++++
Tests/A4/Je_7_Reachability_WhileTrue.java | 19 ++++++++++
...eachability_WhileTrue_ConstantFolding.java | 23 ++++++++++++
Tests/A4/Je_7_Return_IfElseIf.java | 19 ++++++++++
Tests/A4/Je_7_Return_IfIfNoElseElse.java | 31 ++++++++++++++++
Tests/A4/Je_7_Return_IfIfNot.java | 19 ++++++++++
Tests/A4/Je_7_Return_MissingInElse.java | 22 ++++++++++++
.../Je_8_DefiniteAssignment_ArrayAssign.java | 23 ++++++++++++
...8_DefiniteAssignment_ArrayIndexAssign.java | 22 ++++++++++++
...DefiniteAssignment_ComplexInitializer.java | 20 +++++++++++
...DefiniteAssignment_FalseAndAssignment.java | 21 +++++++++++
..._DefiniteAssignment_FieldWithSameName.java | 22 ++++++++++++
Tests/A4/Je_8_DefiniteAssignment_IfIfNot.java | 27 ++++++++++++++
.../Je_8_DefiniteAssignment_InitToItself.java | 20 +++++++++++
...niteAssignment_SomethingAndAssignment.java | 26 ++++++++++++++
...initeAssignment_SomethingOrAssignment.java | 22 ++++++++++++
...teAssignment_UninitializedExpInLvalue.java | 20 +++++++++++
...iteAssignment_UninitializedInNewArray.java | 18 ++++++++++
.../Je_8_DefiniteAssignment_WhileFalse.java | 26 ++++++++++++++
Tests/A4/Je_Widening.java | 7 ++++
61 files changed, 1122 insertions(+)
create mode 100644 Tests/A4/J1_7_Reachability_AfterIfWithWhileTrue.java
create mode 100644 Tests/A4/J1_7_Reachability_EmptyVoidMethod.java
create mode 100644 Tests/A4/J1_7_Reachability_IfAndWhile_Return.java
create mode 100644 Tests/A4/J1_7_Reachability_IfThenElse_InConstructor.java
create mode 100644 Tests/A4/J1_7_Reachability_IfThenElse_InValueMethod.java
create mode 100644 Tests/A4/J1_7_Reachability_IfThenElse_InVoidMethod.java
create mode 100644 Tests/A4/J1_7_Reachability_WhileTrue_ConstantFolding.java
create mode 100644 Tests/A4/J1_7_Unreachable_IfEqualsNot.java
create mode 100644 Tests/A4/J1_Reachable1.java
create mode 100644 Tests/A4/J1_Reachable2.java
create mode 100644 Tests/A4/J1_Reachable3.java
create mode 100644 Tests/A4/J1_Reachable4.java
create mode 100644 Tests/A4/J1_Unreachable.java
create mode 100644 Tests/A4/J1_arbitraryreturn.java
create mode 100644 Tests/A4/J1_defasn_use_before_declare.java
create mode 100644 Tests/A4/J1_ifThenElse.java
create mode 100644 Tests/A4/J1_if_then.java
create mode 100644 Tests/A4/J1_multipleReturn.java
create mode 100644 Tests/A4/J1_omittedvoidreturn.java
create mode 100644 Tests/A4/J1_reachability_return/Main.java
create mode 100644 Tests/A4/J1_reachability_return/java/util/Random.java
create mode 100644 Tests/A4/J1_reachableIfBody.java
create mode 100644 Tests/A4/J1_unreachableAutomation.java
create mode 100644 Tests/A4/J1_while1.java
create mode 100644 Tests/A4/J1_while2.java
create mode 100644 Tests/A4/J1_whiletrue1.java
create mode 100644 Tests/A4/Je_7_DefiniteAssignment_2LazyOr_Assignment.java
create mode 100644 Tests/A4/Je_7_DefiniteAssignment_3LazyOr_Assignment.java
create mode 100644 Tests/A4/Je_7_Reachability_AfterElseReturn.java
create mode 100644 Tests/A4/Je_7_Reachability_AfterIfReturn.java
create mode 100644 Tests/A4/Je_7_Reachability_AfterIfReturnElseReturn.java
create mode 100644 Tests/A4/Je_7_Reachability_AfterReturnEmptyBlock.java
create mode 100644 Tests/A4/Je_7_Reachability_AfterReturn_Constructor.java
create mode 100644 Tests/A4/Je_7_Reachability_AfterValueReturn.java
create mode 100644 Tests/A4/Je_7_Reachability_AfterVoidReturn.java
create mode 100644 Tests/A4/Je_7_Reachability_EmptyValueMethod.java
create mode 100644 Tests/A4/Je_7_Reachability_ForFalse_1.java
create mode 100644 Tests/A4/Je_7_Reachability_ForFalse_2.java
create mode 100644 Tests/A4/Je_7_Reachability_ReturnReturn.java
create mode 100644 Tests/A4/Je_7_Reachability_WhileFalse_ConstantFolding.java
create mode 100644 Tests/A4/Je_7_Reachability_WhileFalse_Empty.java
create mode 100644 Tests/A4/Je_7_Reachability_WhileFalse_IfThenElse.java
create mode 100644 Tests/A4/Je_7_Reachability_WhileTrue.java
create mode 100644 Tests/A4/Je_7_Reachability_WhileTrue_ConstantFolding.java
create mode 100644 Tests/A4/Je_7_Return_IfElseIf.java
create mode 100644 Tests/A4/Je_7_Return_IfIfNoElseElse.java
create mode 100644 Tests/A4/Je_7_Return_IfIfNot.java
create mode 100644 Tests/A4/Je_7_Return_MissingInElse.java
create mode 100644 Tests/A4/Je_8_DefiniteAssignment_ArrayAssign.java
create mode 100644 Tests/A4/Je_8_DefiniteAssignment_ArrayIndexAssign.java
create mode 100644 Tests/A4/Je_8_DefiniteAssignment_ComplexInitializer.java
create mode 100644 Tests/A4/Je_8_DefiniteAssignment_FalseAndAssignment.java
create mode 100644 Tests/A4/Je_8_DefiniteAssignment_FieldWithSameName.java
create mode 100644 Tests/A4/Je_8_DefiniteAssignment_IfIfNot.java
create mode 100644 Tests/A4/Je_8_DefiniteAssignment_InitToItself.java
create mode 100644 Tests/A4/Je_8_DefiniteAssignment_SomethingAndAssignment.java
create mode 100644 Tests/A4/Je_8_DefiniteAssignment_SomethingOrAssignment.java
create mode 100644 Tests/A4/Je_8_DefiniteAssignment_UninitializedExpInLvalue.java
create mode 100644 Tests/A4/Je_8_DefiniteAssignment_UninitializedInNewArray.java
create mode 100644 Tests/A4/Je_8_DefiniteAssignment_WhileFalse.java
create mode 100644 Tests/A4/Je_Widening.java
diff --git a/Tests/A4/J1_7_Reachability_AfterIfWithWhileTrue.java b/Tests/A4/J1_7_Reachability_AfterIfWithWhileTrue.java
new file mode 100644
index 0000000..d891a85
--- /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 0000000..223e6bd
--- /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 0000000..47c9e09
--- /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 0000000..759648a
--- /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 0000000..12db939
--- /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 0000000..c7a00c3
--- /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 0000000..74e6c64
--- /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 0000000..b93583d
--- /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 0000000..778ac3a
--- /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 0000000..0c16e33
--- /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 0000000..310b1d3
--- /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 0000000..04157d4
--- /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 0000000..18896b6
--- /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 0000000..0b37a16
--- /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 0000000..6061d38
--- /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 0000000..505becd
--- /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 0000000..5cc1bc2
--- /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 0000000..f12f64f
--- /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 0000000..402a8c6
--- /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 0000000..de4036f
--- /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 0000000..1158fcc
--- /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 0000000..e33153e
--- /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 0000000..7fc99c4
--- /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 0000000..184fe77
--- /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 0000000..d06992c
--- /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 0000000..4edf636
--- /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 0000000..1b8c7a6
--- /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 0000000..d266e04
--- /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 0000000..fb300ec
--- /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 0000000..39735db
--- /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 0000000..15048de
--- /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 0000000..8345004
--- /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 0000000..bf7a1ad
--- /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 0000000..960a24f
--- /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 0000000..ddba8cc
--- /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 0000000..4672f04
--- /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 0000000..f7fd9d2
--- /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 0000000..54a614a
--- /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 0000000..48d261a
--- /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 0000000..0de19be
--- /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 0000000..713b718
--- /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 0000000..89a4457
--- /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 0000000..3a12604
--- /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 0000000..6aa67d4
--- /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 0000000..0971f4d
--- /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 0000000..8746a2f
--- /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 0000000..b8793db
--- /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 0000000..def8ab4
--- /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 0000000..5a29a2b
--- /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 0000000..c3cb413
--- /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 0000000..86676cb
--- /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 0000000..c067b88
--- /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 0000000..e7442a5
--- /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 0000000..05cdce4
--- /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 0000000..69a3bbf
--- /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 0000000..cc7edef
--- /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 0000000..2c3312d
--- /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 0000000..e2b0f00
--- /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 0000000..d7b189e
--- /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 0000000..5bcd5ad
--- /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 0000000..4b2968c
--- /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(){}
+}
--
GitLab