From af3a358e7956071737c3d0c12ed2e6d3177e1c04 Mon Sep 17 00:00:00 2001
From: Peizhao Ou <peizhaoo@uci.edu>
Date: Sun, 28 Feb 2016 23:50:42 -0800
Subject: [PATCH] edits

---
 .../codeGenerator/CodeGeneratorUtils.java     | 47 +++++++++----------
 .../uci/eecs/codeGenerator/Environment.java   |  3 +-
 .../eecs/specExtraction/GlobalConstruct.java  |  2 +
 3 files changed, 27 insertions(+), 25 deletions(-)

diff --git a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
index 694695c..04f3be9 100644
--- a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
+++ b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
@@ -248,6 +248,7 @@ public class CodeGeneratorUtils {
 
 		Code code = new Code();
 		String line = null;
+		Code fieldsInit = null;
 
 		// Add auto-generated comments
 		code.addLine("/**");
@@ -461,29 +462,27 @@ public class CodeGeneratorUtils {
 		code.addLine("");
 
 		// Define @Print
-		if (!globalConstruct.printState.isEmpty()) {
-			code.addLine(ShortComment("Define @" + SpecNaming.PrintState));
-			code.addLine("void _" + SpecNaming.PrintState.toLowerCase() + "("
-					+ SpecNaming.Method + " " + SpecNaming.Method1 + ") {");
-
-			// Initialize state struct fields
-			Code fieldsInit = GenerateStateFieldsInitialization(
-					SpecNaming.Method1, SpecNaming.StateInst, globalConstruct);
-			fieldsInit.align(1);
-			code.addLines(fieldsInit);
-			code.addLine("");
-			if (!globalConstruct.autoGenPrint)
-				code.addLine(TabbedLine(ShortComment("Execute user-defined state printing code")));
-			else
-				// Auto-generated the copy function
-				code.addLine(TabbedLine(ShortComment("Execute auto-generated state printing code")));
-
-			// Align the code with one tab
-			globalConstruct.printState.align(1);
-			code.addLines(globalConstruct.printState);
-			code.addLine("}");
-			code.addLine("");
-		}
+		code.addLine(ShortComment("Define @" + SpecNaming.PrintState));
+		code.addLine("void _" + SpecNaming.PrintState.toLowerCase() + "("
+				+ SpecNaming.Method + " " + SpecNaming.Method1 + ") {");
+
+		// Initialize state struct fields
+		fieldsInit = GenerateStateFieldsInitialization(SpecNaming.Method1,
+				SpecNaming.StateInst, globalConstruct);
+		fieldsInit.align(1);
+		code.addLines(fieldsInit);
+		code.addLine("");
+		if (!globalConstruct.autoGenPrint)
+			code.addLine(TabbedLine(ShortComment("Execute user-defined state printing code")));
+		else
+			// Auto-generated the copy function
+			code.addLine(TabbedLine(ShortComment("Execute auto-generated state printing code")));
+
+		// Align the code with one tab
+		globalConstruct.printState.align(1);
+		code.addLines(globalConstruct.printState);
+		code.addLine("}");
+		code.addLine("");
 
 		// Define @Commutativity
 		code.addLine(ShortComment("Define commutativity checking functions"));
@@ -517,7 +516,7 @@ public class CodeGeneratorUtils {
 		for (File file : interfaceListMap.keySet()) {
 			ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
 			for (InterfaceConstruct construct : list) {
-				Code fieldsInit = null;
+				fieldsInit = null;
 
 				// Define interface functions
 				String name = construct.getName();
diff --git a/src/edu/uci/eecs/codeGenerator/Environment.java b/src/edu/uci/eecs/codeGenerator/Environment.java
index 563babb..5e16b15 100644
--- a/src/edu/uci/eecs/codeGenerator/Environment.java
+++ b/src/edu/uci/eecs/codeGenerator/Environment.java
@@ -22,7 +22,8 @@ public class Environment {
 			+ "/test-cdsspec/";
 	public final static String GeneratedFilesDir = ModelCheckerTestDir;
 
-	public final static String REGISTER = "register";
+	public final static String REGISTER_ACQREL = "register-acqrel";
+	public final static String REGISTER_RELAXED = "register-relaxed";
 	public final static String MS_QUEUE = "ms-queue";
 	public final static String LINUXRWLOCKS = "linuxrwlocks";
 	public final static String MCS_LOCK = "mcs-lock";
diff --git a/src/edu/uci/eecs/specExtraction/GlobalConstruct.java b/src/edu/uci/eecs/specExtraction/GlobalConstruct.java
index d8f6dd4..cfd935c 100644
--- a/src/edu/uci/eecs/specExtraction/GlobalConstruct.java
+++ b/src/edu/uci/eecs/specExtraction/GlobalConstruct.java
@@ -54,6 +54,8 @@ public class GlobalConstruct extends Construct {
 		if (emptyState) {
 			WrongAnnotationException.warning(file, beginLineNum,
 					"The state is empty. Make sure that's what you want!");
+			// Add a fake state declaration
+			declState.add(new VariableDeclaration("int", "FakeState"));
 		}
 
 		autoGenInitial = initState.isEmpty();
-- 
2.34.1