edits

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

diff --git a/src/edu/uci/eecs/specExtraction/SpecExtractor.java b/src/edu/uci/eecs/specExtraction/SpecExtractor.java
index f8925fbd0d7fb1a2d8f42c21e4874bd4911031a8..a12ce256cfe7e72f924524bdec7850117021daba 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/SpecExtractor.java
+++ b/src/edu/uci/eecs/specExtraction/SpecExtractor.java
@@ -624,7 +624,7 @@ public class SpecExtractor {
                        lineReader = new LineNumberReader(br);
                        // "/\*\*\s*@(DeclareState|Interface)"
                        Pattern regexpBegin = Pattern
-                                       .compile("/\\*\\*\\s*@(DeclareState|Interface|PreCondition|JustifyingCondition|Transition|PostCondition|Define)");
+                                       .compile("/\\*\\*\\s*@(DeclareState|Interface|PreCondition|JustifyingCondition|Transition|JustifyingPostcondition|PostCondition|Define)");
                        Matcher matcher = regexpBegin.matcher("");
 
                        String line;
@@ -654,8 +654,9 @@ public class SpecExtractor {
                                                                beginLineNum);
                                        } else if (constructName.equals(SpecNaming.Interface)
                                                        || constructName.equals(SpecNaming.PreCondition)
-                                                       || constructName.equals(SpecNaming.JustifyingCondition)
+                                                       || constructName.equals(SpecNaming.JustifyingPrecondition)
                                                        || constructName.equals(SpecNaming.Transition)
+                                                       || constructName.equals(SpecNaming.JustifyingPostcondition)
                                                        || constructName.equals(SpecNaming.PostCondition)) {
                                                extractInterfaceConstruct(file, lineReader, line,
                                                                beginLineNum);