- baseLocation = new CompositeLocation(new Location(md, globalLocId));
- } else {
- String thisLocId = ssjava.getMethodLattice(md).getThisLoc();
- baseLocation = new CompositeLocation(new Location(md, thisLocId));
+
+ }
+
+ System.out.println("\n#checkLocationFromMethodInvokeNode=" + min.printNode(0)
+ + " baseLocation=" + baseLocation);
+
+ int compareResult =
+ CompositeLattice.compare(constraint, baseLocation, true, generateErrorMessage(cd, min));
+
+ if (compareResult == ComparisonResult.LESS) {
+ throw new Error("Method invocation does not respect the current branch constraint at "
+ + generateErrorMessage(cd, min));
+ } else if (compareResult != ComparisonResult.GREATER) {
+ // if the current constraint is higher than method's THIS location
+ // no need to check constraints!
+ CompositeLocation calleeConstraint =
+ translateCallerLocToCalleeLoc(calleeMD, baseLocation, constraint);
+ checkMethodBody(calleeMD.getClassDesc(), calleeMD, calleeConstraint);