add INTERFACE_END

diff --git a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
index 272f4aae6c68ad08ddda366f473ea0909620f14b..7dcaaa0acec7a605c3bedca3858964d6a9bb6e47 100644 (file)
--- a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
+++ b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
@@ -1112,6 +1112,14 @@ public class CodeGeneratorUtils {
                                                + SpecNaming.InterfaceValueInst) + ";");
                code.addLine("");
 
+               // Instrument with the INTERFACE_END annotations
+               code.addLine(prefixTabs + "\t"
+                               + ShortComment("Instrument with the INTERFACE_END annotation"));
+               // _createInterfaceEndAnnotation(_DEQ_str);
+               code.addLine(prefixTabs + "\t"
+                               + SpecNaming.CreateInterfaceEndAnnoFunc
+                               + Brace(SpecNaming.AppendStr(name)) + ";");
+
                // Return if necessary
                if (!construct.getFunctionHeader().isReturnVoid())
                        code.addLine(prefixTabs + "\treturn " + SpecNaming.RET + ";");

diff --git a/src/edu/uci/eecs/specExtraction/SpecNaming.java b/src/edu/uci/eecs/specExtraction/SpecNaming.java
index 78ea9039c9d970f4ef1a09f5e7e7c14ffc24970c..8355b75fc696b2d7a0fa5fd11e6f3661b41dbcec 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/SpecNaming.java
+++ b/src/edu/uci/eecs/specExtraction/SpecNaming.java
@@ -169,6 +169,7 @@ public class SpecNaming {
        public static final String CreateInitAnnoFunc = "_createInitAnnotation";
        public static final String CreateInterfaceBeginAnnoFunc = "_createInterfaceBeginAnnotation";
        public static final String SetInterfaceBeginAnnoValueFunc = "_setInterfaceBeginAnnotationValue";
+       public static final String CreateInterfaceEndAnnoFunc = "_createInterfaceEndAnnotation";
        public static final String CreateOPDefineAnnoFunc = "_createOPDefineAnnotation";
        public static final String CreateOPDefineUnattachedFunc = "_createOPDefineUnattached";
        public static final String CreateOPClearDefineUnattachedFunc = "_createOPClearDefineUnattached";