From: Peizhao Ou <peizhaoo@uci.edu>
Date: Mon, 14 Mar 2016 19:18:28 +0000 (-0700)
Subject: add INTERFACE_END
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=195f28450704612d09341f8262b31254e7852b62

add INTERFACE_END
---

diff --git a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
index 272f4aa..7dcaaa0 100644
--- 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 78ea903..8355b75 100644
--- 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";