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;
import edu.uci.eecs.specCompiler.specExtraction.SourceFileInfo;
import edu.uci.eecs.specCompiler.specExtraction.SpecExtractor;
+/**
+ * <p>
+ * A specificaiton semantics checker that checks the consistency of the
+ * specifications after they are extracted from the source code.
+ * </p>
+ *
+ * @author peizhaoo
+ *
+ */
public class SemanticsChecker {
public final HashMap<File, SourceFileInfo> srcFilesInfo;
public final ArrayList<Construct> constructs;
for (int j = 0; j < iConstruct.commitPointSet.size(); j++) {
String label = iConstruct.commitPointSet.get(j);
-// if (!CPLabel2InterfaceConstruct.containsKey(label)) {
-// CPLabel2InterfaceConstruct.put(label,
-// new ArrayList<InterfaceConstruct>());
-// }
-// CPLabel2InterfaceConstruct.get(label).add(iConstruct);
+ // if (!CPLabel2InterfaceConstruct.containsKey(label)) {
+ // CPLabel2InterfaceConstruct.put(label,
+ // new ArrayList<InterfaceConstruct>());
+ // }
+ // CPLabel2InterfaceConstruct.get(label).add(iConstruct);
if (!CPLabel2InterfaceConstruct.containsKey(label)) {
CPLabel2InterfaceConstruct.put(label, iConstruct);
} else {
throw new SemanticsCheckerException(
"Commit point has multiple interfaces!");
}
-
+
}
}
}
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;