edits

[cdsspec-compiler.git] / src / edu / uci / eecs / codeGenerator / CodeGeneratorUtils.java

diff --git a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
index 7dcaaa0acec7a605c3bedca3858964d6a9bb6e47..6a90a72eec1f286786f847cb945124cee8eb6707 100644 (file)
--- a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
+++ b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
@@ -408,6 +408,15 @@ public class CodeGeneratorUtils {
                                        code.addLine(DeclareDefine(SpecNaming.CString,
                                                        SpecNaming.AppendStr(tmpFunc),
                                                        SpecNaming.EmptyCString));
+                               // JustifyingCondition
+                               tmpFunc = name + "_" + SpecNaming.JustifyingCondition;
+                               if (!construct.justifyingCondition.isEmpty())
+                                       code.addLine(DeclareDefine(SpecNaming.CString,
+                                                       SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
+                               else
+                                       code.addLine(DeclareDefine(SpecNaming.CString,
+                                                       SpecNaming.AppendStr(tmpFunc),
+                                                       SpecNaming.EmptyCString));
                                // PostCondition
                                tmpFunc = name + "_" + SpecNaming.PostCondition;
                                if (!construct.postCondition.isEmpty())
@@ -594,13 +603,14 @@ public class CodeGeneratorUtils {
                                if (!construct.preCondition.isEmpty()) {
                                        code.addLine(ShortComment("Define @"
                                                        + SpecNaming.PreCondition + " for " + name));
-                                       code.addLine("bool _" + name + "_"
-                                                       + SpecNaming.PreCondition + "(" + SpecNaming.Method
-                                                       + " " + SpecNaming.Method1 + ") {");
+                                       code.addLine("bool _" + name + "_" + SpecNaming.PreCondition
+                                                       + "(" + SpecNaming.Method + " " + SpecNaming.Method1
+                                                       + ", " + SpecNaming.Method + " " + SpecNaming.Method2
+                                                       + ") {");
 
                                        // Initialize value struct fields
                                        fieldsInit = GenerateInterfaceFieldsInitialization(
-                                                       SpecNaming.Method1, SpecNaming.InterfaceValueInst,
+                                                       SpecNaming.Method2, SpecNaming.InterfaceValueInst,
                                                        construct);
                                        fieldsInit.align(1);
                                        code.addLines(fieldsInit);
@@ -616,19 +626,47 @@ public class CodeGeneratorUtils {
                                        code.addLine("}");
                                        code.addLine("");
 
+                               }
+                               // Define @JustifyingCondition
+                               if (!construct.justifyingCondition.isEmpty()) {
+                                       code.addLine(ShortComment("Define @"
+                                                       + SpecNaming.JustifyingCondition + " for " + name));
+                                       code.addLine("bool _" + name + "_" + SpecNaming.JustifyingCondition
+                                                       + "(" + SpecNaming.Method + " " + SpecNaming.Method1
+                                                       + ", " + SpecNaming.Method + " " + SpecNaming.Method2
+                                                       + ") {");
+
+                                       // Initialize value struct fields
+                                       fieldsInit = GenerateInterfaceFieldsInitialization(
+                                                       SpecNaming.Method2, SpecNaming.InterfaceValueInst,
+                                                       construct);
+                                       fieldsInit.align(1);
+                                       code.addLines(fieldsInit);
+
+                                       construct.justifyingCondition.align(1);
+                                       code.addLine(TabbedLine(ShortComment("Execute JustifyingCondition")));
+                                       code.addLines(construct.justifyingCondition);
+
+                                       // By default, we will return true for @PreCondition
+                                       code.addLine(TabbedLine(ShortComment("By default @JustifyingCondition returns true")));
+                                       code.addLine(TabbedLine("return true;"));
+
+                                       code.addLine("}");
+                                       code.addLine("");
+
                                }
                                // Define @PostCondition
                                if (!construct.postCondition.isEmpty()) {
                                        code.addLine(ShortComment("Define @"
                                                        + SpecNaming.PostCondition + " for " + name));
-                                       code.addLine("bool _" + name + "_"
-                                                       + SpecNaming.PostCondition + "("
-                                                       + SpecNaming.Method + " " + SpecNaming.Method1
+                                       code.addLine("bool _" + name + "_" + SpecNaming.PostCondition
+                                                       + "(" + SpecNaming.Method + " " + SpecNaming.Method1
+                                                       + ", " + SpecNaming.Method + " " + SpecNaming.Method2
                                                        + ") {");
 
                                        // Initialize value struct fields
                                        fieldsInit = GenerateInterfaceFieldsInitialization(
-                                                       SpecNaming.Method1, SpecNaming.InterfaceValueInst,
+                                                       SpecNaming.Method2, SpecNaming.InterfaceValueInst,
                                                        construct);
                                        fieldsInit.align(1);
                                        code.addLines(fieldsInit);
@@ -791,6 +829,20 @@ public class CodeGeneratorUtils {
                                                        + "),";
                                }
                                code.addLine(TabbedLine(line, 2));
+                               // JustifyingCondition
+                               line = "new "
+                                               + SpecNaming.NamedFunction
+                                               + "("
+                                               + SpecNaming.AppendStr(name + "_"
+                                                               + SpecNaming.JustifyingCondition) + ", "
+                                               + SpecNaming.JustifyingConditionType + ", (void*) ";
+                               if (construct.justifyingCondition.isEmpty()) {
+                                       line = line + SpecNaming.NullFunc + "),";
+                               } else {
+                                       line = line + "_" + name + "_" + SpecNaming.JustifyingCondition
+                                                       + "),";
+                               }
+                               code.addLine(TabbedLine(line, 2));
                                // PostCondition
                                line = "new "
                                                + SpecNaming.NamedFunction