Skip to content

Commit 73a54a6

Browse files
Kirill GolubevKirill Golubev
Kirill Golubev
authored and
Kirill Golubev
committed
tests are working again
1 parent 9c54eee commit 73a54a6

File tree

2 files changed

+5
-74
lines changed

2 files changed

+5
-74
lines changed

‎liquidjava/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java‎

Lines changed: 4 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -236,7 +236,7 @@ public <T, A extends T> void visitCtAssignment(CtAssignment<T, A> assignement) {
236236

237237
// corresponding ghost function update
238238
try {
239-
updateGhostField(fw);
239+
AuxStateHandler.updateGhostField(fw, this);
240240
} catch (ParsingException e) {
241241
ErrorHandler.printCostumeError(assignement, "ParsingException in `" + assignement + "` in class `"
242242
+ f.getDeclaringType() + "` : " + e.getMessage(), errorEmitter);
@@ -538,9 +538,8 @@ private void checkAssignment(String name, CtTypeReference<?> type, CtExpression<
538538
}
539539
}
540540
Optional<VariableInstance> r = context.getLastVariableInstance(name);
541-
if (r.isPresent()) {
542-
vcChecker.removePathVariableThatIncludes(r.get().getName());// AQUI!!
543-
}
541+
// AQUI!!
542+
r.ifPresent(variableInstance -> vcChecker.removePathVariableThatIncludes(variableInstance.getName()));
544543

545544
vcChecker.removePathVariableThatIncludes(name);// AQUI!!
546545
try {
@@ -592,6 +591,7 @@ private Predicate substituteAllVariablesForLastInstance(Predicate c) {
592591
/**
593592
* @param <T>
594593
* @param elem
594+
* @param name
595595
* Cannot be null
596596
*/
597597
private <T> void getPutVariableMetadada(CtElement elem, String name) {
@@ -604,42 +604,4 @@ private <T> void getPutVariableMetadada(CtElement elem, String name) {
604604
elem.putMetadata(REFINE_KEY, cref);
605605
}
606606

607-
private void updateGhostField(CtFieldWrite<?> fw) throws ParsingException {
608-
CtField<?> f = fw.getVariable().getDeclaration();
609-
String updatedVarName = String.format(thisFormat, fw.getVariable().getSimpleName());
610-
611-
// transition method construction
612-
CtMethod<?> transitionMethod = factory.createMethod();
613-
transitionMethod.setType(factory.createCtTypeReference(void.class));
614-
transitionMethod.setBody(factory.createCtBlock(factory.createCodeSnippetStatement()));
615-
transitionMethod.setSimpleName("_");
616-
617-
transitionMethod.setParent(f.getDeclaringType());
618-
CtAnnotation<?> ann = factory.createAnnotation(factory.createCtTypeReference(StateRefinement.class));
619-
620-
// state transition annotation construction
621-
String stateChangeRefinementTo = f.getSimpleName() + "(this) == " + updatedVarName;
622-
String stateChangeRefinementFrom = "true";
623-
ann.addValue("to", stateChangeRefinementTo);
624-
ann.addValue("from", stateChangeRefinementFrom);
625-
626-
transitionMethod.addAnnotation(ann);
627-
628-
// extracting target from assignment
629-
System.out.println("Target for invocation: " + fw.getTarget());
630-
CtInvocation<?> inv = factory.createInvocation(fw.getTarget(), transitionMethod.getReference(),
631-
Collections.emptyList());
632-
633-
// Refined function construction for invocation facilities reuse
634-
RefinedFunction rf = new RefinedFunction();
635-
rf.setName(transitionMethod.getSimpleName());
636-
rf.setType(transitionMethod.getType());
637-
rf.setRefReturn(new Predicate());
638-
rf.setClass(transitionMethod.getDeclaringType().getQualifiedName());
639-
640-
// applying transition:
641-
AuxStateHandler.handleMethodState(transitionMethod, rf, this);
642-
AuxStateHandler.checkTargetChanges(this, rf, inv.getTarget(), Collections.emptyMap(), inv);
643-
}
644-
645607
}

‎liquidjava/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java‎

Lines changed: 1 addition & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -191,20 +191,11 @@ private List<RefinedVariable> getVariables(Predicate c, String varName) {
191191
}
192192

193193
private void getVariablesFromContext(List<String> lvars, List<RefinedVariable> allVars, String notAdd) {
194-
lvars.stream().filter(name -> name.equals(notAdd) && context.hasVariable(name)).map(context::getVariableByName)
194+
lvars.stream().filter(name -> !name.equals(notAdd) && context.hasVariable(name)).map(context::getVariableByName)
195195
.filter(rv -> !allVars.contains(rv)).forEach(rv -> {
196196
allVars.add(rv);
197197
recAuxGetVars(rv, allVars);
198198
});
199-
200-
// for (String name : lvars)
201-
// if (!name.equals(notAdd) && context.hasVariable(name)) {
202-
// RefinedVariable rv = context.getVariableByName(name);
203-
// if (!allVars.contains(rv)) {
204-
// allVars.add(rv);
205-
// recAuxGetVars(rv, allVars);
206-
// }
207-
// }
208199
}
209200

210201
private void recAuxGetVars(RefinedVariable var, List<RefinedVariable> newVars) {
@@ -214,15 +205,6 @@ private void recAuxGetVars(RefinedVariable var, List<RefinedVariable> newVars) {
214205
String varName = var.getName();
215206
List<String> l = c.getVariableNames();
216207
getVariablesFromContext(l, newVars, varName);
217-
// for (String name : l) {
218-
// if (!name.equals(varName) && context.hasVariable(name)) {
219-
// RefinedVariable rv = context.getVariableByName(name);
220-
// if (!newVars.contains(rv)) {
221-
// newVars.add(rv);
222-
// recAuxGetVars(rv, newVars);
223-
// }
224-
// }
225-
// }
226208
}
227209

228210
public boolean smtChecks(Predicate cSMT, Predicate expectedType, CtElement elem) {
@@ -269,11 +251,6 @@ private void smtChecking(Predicate cSMT, Predicate expectedType, CtElement eleme
269251
private Predicate substituteByMap(Predicate c, HashMap<String, String> map) {
270252
map.keySet().forEach(s -> c.substituteVariable(s, map.get(s)));
271253
return c;
272-
273-
// Predicate c1 = c;
274-
// for (String s : map.keySet())
275-
// c1 = c1.substituteVariable(s, map.get(s));
276-
// return c1;
277254
}
278255

279256
public void addPathVariable(RefinedVariable rv) {
@@ -287,14 +264,6 @@ public void removePathVariable(RefinedVariable rv) {
287264
void removePathVariableThatIncludes(String otherVar) {
288265
pathVariables.stream().filter(rv -> rv.getRefinement().getVariableNames().contains(otherVar))
289266
.collect(Collectors.toList()).forEach(pathVariables::remove);
290-
291-
// List<RefinedVariable> toRemove = new ArrayList<>();
292-
// for (RefinedVariable rv : pathVariables)
293-
// if (rv.getRefinement().getVariableNames().contains(otherVar))
294-
// toRemove.add(rv);
295-
//
296-
// for (RefinedVariable rv : toRemove)
297-
// pathVariables.remove(rv);
298267
}
299268

300269
private void printVCs(String string, String stringSMT, Predicate expectedType) {

0 commit comments

Comments
 (0)