Fix rule-conversion bug that omitted optional constraint.

Signed-off-by: Stefan Krueger <stefan.krueger@crossing.tu-darmstadt.de>
CROSSINGTUD · Jun 9, 2020 · c013f5f · c013f5f
1 parent 080356d
commit c013f5f
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 4 deletions.
diff --git a/CryptoAnalysis/src/main/java/crypto/cryslhandler/CrySLModelReader.java b/CryptoAnalysis/src/main/java/crypto/cryslhandler/CrySLModelReader.java
@@ -218,7 +218,7 @@ private CrySLRule createRuleFromResource(Resource resource) throws CryptoAnalysi
 				actPreds.add(pred.tobasicPredicate());
 			} else {
 				actPreds.add(new CrySLCondPredicate(pred.getBaseObject(), pred.getPredName(), pred.getParameters(), pred.isNegated(),
-						getStatesForMethods(CryslReaderUtils.resolveAggregateToMethodeNames(cond))));
+						getStatesForMethods(CryslReaderUtils.resolveAggregateToMethodeNames(cond)), pred.getConstraint()));
 			}
 		}
 		return new CrySLRule(curClass, objects, this.forbiddenMethods, this.smg, constraints, actPreds);
@@ -729,7 +729,6 @@ private CrySLPredicate extractReqPred(final ReqPred pred) {
 
 	private ISLConstraint getPredicate(Pred pred) {
 		final List<ICrySLPredicateParameter> variables = new ArrayList<>();
-//		PredLit innerPred = (PredLit) pred;
 		if (pred.getParList() != null) {
 			for (final SuPar var : pred.getParList().getParameters()) {
 				if (var.getVal() != null) {

diff --git a/CryptoAnalysis/src/main/java/crypto/rules/CrySLCondPredicate.java b/CryptoAnalysis/src/main/java/crypto/rules/CrySLCondPredicate.java
@@ -2,8 +2,8 @@
 
 import java.util.List;
 import java.util.Set;
-
 import crypto.interfaces.ICrySLPredicateParameter;
+import crypto.interfaces.ISLConstraint;
 
 public class CrySLCondPredicate extends CrySLPredicate {
 
@@ -14,7 +14,11 @@ public class CrySLCondPredicate extends CrySLPredicate {
 	private final Set<StateNode> conditionalNodes;
 
 	public CrySLCondPredicate(ICrySLPredicateParameter baseObj, String name, List<ICrySLPredicateParameter> variables, Boolean not, Set<StateNode> label) {
-		super(baseObj, name, variables, not);
+		this(baseObj, name, variables, not, label, null);
+	}
+
+	public CrySLCondPredicate(ICrySLPredicateParameter baseObj, String name, List<ICrySLPredicateParameter> variables, Boolean not, Set<StateNode> label, ISLConstraint cons) {
+		super(baseObj, name, variables, not, cons);
 		conditionalNodes = label;
 	}