edits

diff --git a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
index 694695cf48ca9db30cae73666101a9ccb75ef066..04f3be95f4fba9983f04473a7e84f082159a7dc3 100644 (file)
--- 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 code = new Code();
                String line = null;

+               Code fieldsInit = null;

 
                // Add auto-generated comments
                code.addLine("/**");
 
                // Add auto-generated comments
                code.addLine("/**");


@@ -461,29 +462,27 @@ public class CodeGeneratorUtils {
                code.addLine("");
 
                // Define @Print
                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"));
 
                // 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) {
                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();
 
                                // 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 563babbbd15d518706dda3b8cb77ec11fbf1789a..5e16b15f672ec3a039082d3bf4a43afe4bb29eec 100644 (file)
--- 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;
 
                        + "/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";
        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 d8f6dd42491bfaaa62b17b9e3c06efd8840a4e6e..cfd935c8e6d77d09176f1c3ea95c2830ca1a3b52 100644 (file)
--- 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!");
                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();
                }
 
                autoGenInitial = initState.isEmpty();