fix cp clear

diff --git a/benchmark/linuxrwlocks/linuxrwlocks.c b/benchmark/linuxrwlocks/linuxrwlocks.c
index 0a1a7b203f02f6477623c5ed8f64765ca341a10a..a4e58b69f4418f9779001cf1f386eadf709d095e 100644 (file)
--- a/benchmark/linuxrwlocks/linuxrwlocks.c
+++ b/benchmark/linuxrwlocks/linuxrwlocks.c
@@ -269,7 +269,7 @@ static inline void read_unlock(rwlock_t *rw)
 /**
        @Begin
        @Interface: Write_Unlock
-       @Commit_point_set: Write_Unlock_Point
+       @Commit_point_set: Write_Unlock_Point | Write_Unlock_Clear
        @Check:
                reader_lock_cnt == 0 && writer_lock_acquired
        @Action: 
@@ -285,6 +285,13 @@ static inline void write_unlock(rwlock_t *rw)
                @Label: Write_Unlock_Point
                @End
        */
+
+       /**
+               //@Begin
+               @Commit_point_clear: true
+               @Label: Write_Unlock_Clear
+               @End
+       */
 }
 
 rwlock_t mylock;

diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
index fb1b520202f77d755c22a73f2d6936e009468842..4c4fc87b9cc04374455745591cde258391af1dc7 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
@@ -49,6 +49,7 @@ public class CodeVariables {
        public static final String SPEC_ANNO_TYPE_INTERFACE_END = "INTERFACE_END";
        public static final String SPEC_ANNO_TYPE_POTENTIAL_CP_DEFINE = "POTENTIAL_CP_DEFINE";
        public static final String SPEC_ANNO_TYPE_CP_DEFINE_CHECK = "CP_DEFINE_CHECK";
+       public static final String SPEC_ANNO_TYPE_CP_CLEAR = "CP_CLEAR";
        public static final String SPEC_ANNO_TYPE_CP_DEFINE = "CP_DEFINE";
        public static final String SPEC_ANNOTATION = "spec_annotation";
        public static final String SPEC_ANNOTATION_FIELD_TYPE = "type";
@@ -855,7 +856,7 @@ public class CodeVariables {
                newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "interface_num", interfaceNum));
                newCode.add("\t\t" + STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
                newCode.add("\t\t"
-                               + ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_CP_DEFINE_CHECK));
+                               + ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_CP_CLEAR));
                newCode.add("\t\t" + ASSIGN_TO_PTR(anno, "annotation", structName));
                newCode.add("\t\t" + ANNOTATE(semantics, anno));
                newCode.add("\t" + "}");

diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java b/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java
index e5b5f9da16f8d75c62f9b4a88f91b1dc799eca90..23dad2f4f2b296ec576c5820f3b6de91fa58c2b8 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java
@@ -6,6 +6,7 @@ import java.util.HashMap;
 import java.util.HashSet;
 
 import edu.uci.eecs.specCompiler.grammerParser.ParseException;
+import edu.uci.eecs.specCompiler.specExtraction.CPClearConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.ClassBeginConstruct;
@@ -270,6 +271,15 @@ public class SemanticsChecker {
                                commitPointLabel2Num.put(label, _commitPointNum++);
                                num2CommitPointLabel.put(_commitPointNum, label);
 
+                               CPLabel2Construct.put(label, construct);
+                       } else if (construct instanceof CPClearConstruct) {
+                               CPClearConstruct theConstruct = (CPClearConstruct) construct;
+                               label = theConstruct.label;
+                               checkLabelDuplication(construct, label);
+                               // Number the commit point define check label
+                               commitPointLabel2Num.put(label, _commitPointNum++);
+                               num2CommitPointLabel.put(_commitPointNum, label);
+
                                CPLabel2Construct.put(label, construct);
                        } else if (construct instanceof CPDefineConstruct) {
                                CPDefineConstruct theConstruct = (CPDefineConstruct) construct;