edits

[cdsspec-compiler.git] / src / edu / uci / eecs / specExtraction / InterfaceConstruct.java

diff --git a/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java b/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java
index 1ff0cb05514cc3c8e7c01d56587cee307c6bcd03..ddc26145f8f136c40576cb8ec00657d43f6a05ff 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java
+++ b/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java
@@ -30,7 +30,9 @@ public class InterfaceConstruct extends Construct {
        // have other name conflict
        private String structName;
        public final Code preCondition;
+       public final Code justifyingPrecondition;
        public final Code transition;
+       public final Code justifyingPostcondition;
        public final Code postCondition;
        public final Code print;
 
@@ -53,7 +55,9 @@ public class InterfaceConstruct extends Construct {
                this.name = null;
                this.structName = null;
                this.preCondition = new Code();
+               this.justifyingPrecondition = new Code();
                this.transition = new Code();
+               this.justifyingPostcondition = new Code();
                this.postCondition = new Code();
                this.print = new Code();
 
@@ -92,9 +96,9 @@ public class InterfaceConstruct extends Construct {
         */
        private Code generateAutoPrintFunction() {
                Code code = new Code();
-               // For RET
+               // For C_RET
                code.addLines(SpecUtils.generatePrintStatement(funcHeader.returnType,
-                               SpecNaming.RET));
+                               SpecNaming.C_RET));
                // For arguments
                for (VariableDeclaration decl : funcHeader.args) {
                        String type = decl.type;
@@ -122,7 +126,9 @@ public class InterfaceConstruct extends Construct {
                if (!name.equals(SpecNaming.Interface)
                                && !name.equals(SpecNaming.Transition)
                                && !name.equals(SpecNaming.PreCondition)
+                               && !name.equals(SpecNaming.JustifyingPrecondition)
                                && !name.equals(SpecNaming.SideEffect)
+                               && !name.equals(SpecNaming.JustifyingPostcondition)
                                && !name.equals(SpecNaming.PostCondition)
                                && !name.equals(SpecNaming.PrintValue)) {
                        WrongAnnotationException.err(file, lineNum, name
@@ -178,6 +184,10 @@ public class InterfaceConstruct extends Construct {
                                this.transition.addLines(primitive.contents);
                        } else if (name.equals(SpecNaming.PreCondition)) {
                                this.preCondition.addLines(primitive.contents);
+                       } else if (name.equals(SpecNaming.JustifyingPrecondition)) {
+                               this.justifyingPrecondition.addLines(primitive.contents);
+                       } else if (name.equals(SpecNaming.JustifyingPostcondition)) {
+                               this.justifyingPostcondition.addLines(primitive.contents);
                        } else if (name.equals(SpecNaming.PostCondition)) {
                                this.postCondition.addLines(primitive.contents);
                        } else if (name.equals(SpecNaming.PrintValue)) {