Skip to content

Commit ea78522

Browse files
authored
IVC and MCS bugs (#17)
* Added missing Kind 2 Object value * Changed error handling to ignore some empty cases of analyses
1 parent 5b34578 commit ea78522

File tree

2 files changed

+11
-4
lines changed

2 files changed

+11
-4
lines changed

src/main/java/edu/uiowa/cs/clc/kind2/results/Object.java

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,8 @@ public enum Object
2323
postAnalysisEnd("postAnalysisEnd"),
2424
modelElementSet("modelElementSet"),
2525
progress("progress"),
26-
lsp("lsp");
26+
lsp("lsp"),
27+
modelSetEnumeration("modelSetEnumeration");
2728

2829
private final String value;
2930

@@ -60,6 +61,8 @@ public static Object getKind2Object(String kind2Object)
6061
return progress;
6162
case "lsp":
6263
return lsp;
64+
case "modelSetEnumeration":
65+
return modelSetEnumeration;
6366
default:
6467
throw new UnsupportedOperationException("Value " + kind2Object + " is not defined");
6568
}

src/main/java/edu/uiowa/cs/clc/kind2/results/Result.java

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -161,7 +161,7 @@ public void initialize(String json) {
161161
Analysis kind2Analysis = null;
162162
// for post analysis
163163
Analysis previousAnalysis = null;
164-
164+
boolean emptyAnalysis = false;
165165
for (JsonElement jsonElement : jsonArray) {
166166
String objectType = jsonElement.getAsJsonObject().get(Labels.objectType).getAsString();
167167
Object kind2Object = Object.getKind2Object(objectType);
@@ -250,14 +250,17 @@ public void initialize(String json) {
250250
PostAnalysis postAnalysis = new PostAnalysis(previousAnalysis, jsonElement);
251251
previousAnalysis.setPostAnalysis(postAnalysis);
252252
} else {
253-
throw new RuntimeException("Can not parse kind2 json output");
253+
// This can occur sometimes with no previous analysis when the node had no properties to check.
254+
emptyAnalysis = true;
254255
}
255256
}
256257

257258
if (kind2Object == Object.postAnalysisEnd) {
258259
if (previousAnalysis != null && previousAnalysis.getPostAnalysis() != null) {
259260
// finish the post analysis
260261
previousAnalysis = null;
262+
} else if (emptyAnalysis){
263+
//Do nothing, had a no-analysis postAnalysisStart beforehand.
261264
} else {
262265
throw new RuntimeException("Failed to analyze kind2 json output");
263266
}
@@ -269,7 +272,8 @@ public void initialize(String json) {
269272
ModelElementSet elementSet = new ModelElementSet(postAnalysis, jsonElement);
270273
postAnalysis.addModelElementSet(elementSet);
271274
} else {
272-
throw new RuntimeException("Can not parse kind2 json output");
275+
// This branch gets hit sometimes when we have empty (nonexistent) analyses of nodes with
276+
// no properties to check, causing missing analyses before postAnalyses, as well as this object.
273277
}
274278
}
275279
}

0 commit comments

Comments
 (0)