edits

diff --git a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
index 69c046aa0fbc5bc34e8f03cfedb21bcc05f4b8bc..73176b9566d82152f36f4000db198718aa1d108e 100644 (file)
--- a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
+++ b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
@@ -581,7 +581,7 @@ public class CodeGeneratorUtils {
                                                + SpecNaming.Method1 + ", " + SpecNaming.Method + " " + SpecNaming.Method2 + ") {");
 
                                // Initialize value struct fields
-                               fieldsInit = GenerateInterfaceFieldsInitialization(SpecNaming.Method2, "value", construct);
+                               fieldsInit = GenerateInterfaceFieldsInitialization(SpecNaming.Method2, SpecNaming.InterfaceValueInst, construct);
                                fieldsInit.align(1);
                                code.addLines(fieldsInit);
 
@@ -599,7 +599,7 @@ public class CodeGeneratorUtils {
                                                        + SpecNaming.Method1 + ") {");
 
                                        // Initialize value struct fields
-                                       fieldsInit = GenerateInterfaceFieldsInitialization(SpecNaming.Method1, "value", construct);
+                                       fieldsInit = GenerateInterfaceFieldsInitialization(SpecNaming.Method1, SpecNaming.InterfaceValueInst, construct);
                                        fieldsInit.align(1);
                                        code.addLines(fieldsInit);
 
@@ -618,7 +618,7 @@ public class CodeGeneratorUtils {
                                                        + SpecNaming.Method1 + ") {");
 
                                        // Initialize value struct fields
-                                       fieldsInit = GenerateInterfaceFieldsInitialization(SpecNaming.Method1, "value", construct);
+                                       fieldsInit = GenerateInterfaceFieldsInitialization(SpecNaming.Method1, SpecNaming.InterfaceValueInst, construct);
                                        fieldsInit.align(1);
                                        code.addLines(fieldsInit);
 
@@ -636,7 +636,7 @@ public class CodeGeneratorUtils {
                                                        + SpecNaming.Method1 + ") {");
 
                                        // Initialize value struct fields
-                                       fieldsInit = GenerateInterfaceFieldsInitialization(SpecNaming.Method1, "value", construct);
+                                       fieldsInit = GenerateInterfaceFieldsInitialization(SpecNaming.Method1, SpecNaming.InterfaceValueInst, construct);
                                        fieldsInit.align(1);
                                        code.addLines(fieldsInit);
 
@@ -653,7 +653,7 @@ public class CodeGeneratorUtils {
                                        code.addLine("void _" + name + "_" + SpecNaming.PrintValue + "(" + SpecNaming.Method + " "
                                                        + SpecNaming.Method1 + ") {");
                                        // Initialize value struct fields
-                                       fieldsInit = GenerateInterfaceFieldsInitialization(SpecNaming.Method1, "value", construct);
+                                       fieldsInit = GenerateInterfaceFieldsInitialization(SpecNaming.Method1, SpecNaming.InterfaceValueInst, construct);
                                        fieldsInit.align(1);
                                        code.addLines(fieldsInit);
 
@@ -882,11 +882,11 @@ public class CodeGeneratorUtils {
                String name = construct.getName();
                res.addLine(ShortComment("Initialize fields for " + name));
                // The very first assignment "
-               res.addLine(DeclareDefine(name, "*" + inst, "(" + name + "*) " + methodInst + "->value"));
+               res.addLine(DeclareDefine(name, "*" + inst, "(" + name + "*) " + methodInst + "->" + SpecNaming.MethodValueField));
                // Don't leave out the RET field
                if (!construct.getFunctionHeader().isReturnVoid()) {
                        res.addLine(DeclareDefine(construct.getFunctionHeader().returnType, SpecNaming.RET,
-                                       "value->" + SpecNaming.RET));
+                                       inst + "->" + SpecNaming.RET));
                }
                // For arguments
                for (VariableDeclaration decl : construct.getFunctionHeader().args) {
@@ -1020,20 +1020,20 @@ public class CodeGeneratorUtils {
                // Initialize the value struct
                code.addLine(prefixTabs + "\t" + ShortComment("Initialize the value struct"));
                // The very first assignment "
-               code.addLine(prefixTabs + "\t" + DeclareDefine(name, "*value", SpecNaming.New + Brace(name)));
+               code.addLine(prefixTabs + "\t" + DeclareDefine(name, "*" + SpecNaming.InterfaceValueInst, SpecNaming.New + Brace(name)));
                // Don't leave out the RET field
                if (!construct.getFunctionHeader().isReturnVoid())
-                       code.addLine(prefixTabs + "\t" + AssignToPtr("value", SpecNaming.RET, SpecNaming.RET));
+                       code.addLine(prefixTabs + "\t" + AssignToPtr(SpecNaming.InterfaceValueInst, SpecNaming.RET, SpecNaming.RET));
                // For arguments
                for (VariableDeclaration decl : construct.getFunctionHeader().args)
-                       code.addLine(prefixTabs + "\t" + AssignToPtr("value", decl.name, decl.name));
+                       code.addLine(prefixTabs + "\t" + AssignToPtr(SpecNaming.InterfaceValueInst, decl.name, decl.name));
                code.addLine("");
 
                // Store the value info into the current MethodCall
                // _setInterfaceBeginAnnotationValue(info, value);
                code.addLine(prefixTabs + "\t" + ShortComment("Store the value info into the current MethodCall"));
                code.addLine(prefixTabs + "\t" + SpecNaming.SetInterfaceBeginAnnoValueFunc
-                               + Brace(SpecNaming.AnnoInterfaceInfoInst + ", value") + ";");
+                               + Brace(SpecNaming.AnnoInterfaceInfoInst + ", " + SpecNaming.InterfaceValueInst) + ";");
                code.addLine("");
 
                // Return if necessary

diff --git a/src/edu/uci/eecs/specExtraction/SpecNaming.java b/src/edu/uci/eecs/specExtraction/SpecNaming.java
index d60bf96c6f849fbb074c5fba50d50310bee3deb2..463d2c93e59a25387e5acd5aabb9ea4a17c12bdf 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/SpecNaming.java
+++ b/src/edu/uci/eecs/specExtraction/SpecNaming.java
@@ -145,6 +145,7 @@ public class SpecNaming {
 
        public static final String StateStruct = "StateStruct";
        public static final String Method = "Method";
+       public static final String MethodValueField = "value";
        public static final String CommutativityRule = "CommutativityRule";
        public static final String StateFunctions = "StateFunctions";
        public static final String NamedFunction = "NamedFunction";
@@ -178,6 +179,7 @@ public class SpecNaming {
        public static final String CDSAnnotateFunc = "cdsannotate";
        public static final String PRINT = "PRINT";
        public static final String PrintContainer = "printContainer";
+       public static final String PrintMap = "printMap";
 
        // Special instances
        public static final String Method1 = "_M";
@@ -187,6 +189,7 @@ public class SpecNaming {
        public static final String NewStateInst = "NEW";
        // Specification types and macros
        public static final String RET = "RET";
+       public static final String InterfaceValueInst = "__value";
        
        // The wrapper prefix that we want to attach to the function name
        public static final String WrapperPrefix = "Wrapper";

diff --git a/src/edu/uci/eecs/specExtraction/SpecUtils.java b/src/edu/uci/eecs/specExtraction/SpecUtils.java
index 71512d864cbb3c3ae55ac5174a9e647faab2977f..b8d0479bbb9a82dca06e63c0288b7953df4d9021 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/SpecUtils.java
+++ b/src/edu/uci/eecs/specExtraction/SpecUtils.java
@@ -279,7 +279,11 @@ public class SpecUtils {
                        // printContainer(&q);
                        // model_print("\n");
                        code.addLine(SpecNaming.PRINT + "(\"\\t" + name + ": \");");
-                       code.addLine(SpecNaming.PrintContainer + "(&" + name + ");");
+                       if (type.equals("IntMap")) {
+                               code.addLine(SpecNaming.PrintMap + "(&" + name + ");");
+                       } else {
+                               code.addLine(SpecNaming.PrintContainer + "(&" + name + ");");
+                       }
                        code.addLine(SpecNaming.PRINT + "(\"\\n\");");
                } else if (type.equals("IntList *") || type.equals("IntSet *")
                                || type.equals("IntMap *")) {
@@ -288,7 +292,11 @@ public class SpecUtils {
                        // printContainer(q);
                        // model_print("\n");
                        code.addLine(SpecNaming.PRINT + "(\"\\t" + name + ": \");");
-                       code.addLine(SpecNaming.PrintContainer + "(" + name + ");");
+                       if (type.equals("IntMap *")) {
+                               code.addLine(SpecNaming.PrintMap + "(" + name + ");");
+                       } else {
+                               code.addLine(SpecNaming.PrintContainer + "(" + name + ");");
+                       }
                        code.addLine(SpecNaming.PRINT + "(\"\\n\");");
                } else if (type.equals("void")) {
                        // Just do nothing!