From 9d60b5b715f2b57c4e2e2521dc0821b7863b4388 Mon Sep 17 00:00:00 2001 From: Sven Meyer Date: Sun, 10 Mar 2024 15:24:13 +0100 Subject: [PATCH] Report IncompleteOperationErrors only once for each dataflow path with a missing call --- .../AnalysisSeedWithSpecification.java | 124 +++++++++++---- .../errors/IncompleteOperationError.java | 147 ++++++++++++------ .../headless/BouncyCastleHeadlessTest.java | 2 +- .../headless/BragaCryptoGoodusesTest.java | 20 +-- .../headless/BragaCryptoMisusesTest.java | 42 ++--- .../headless/StaticAnalysisDemoTest.java | 2 +- 6 files changed, 230 insertions(+), 107 deletions(-) diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java b/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java index 92374b81a..0cbdf635f 100644 --- a/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java +++ b/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java @@ -1,17 +1,11 @@ package crypto.analysis; -import java.util.ArrayList; -import java.util.Arrays; -import java.util.Collection; -import java.util.Collections; -import java.util.HashSet; -import java.util.List; -import java.util.Map; -import java.util.Map.Entry; -import java.util.Optional; -import java.util.Set; -import java.util.stream.Collectors; - +import boomerang.callgraph.ObservableICFG; +import boomerang.debugger.Debugger; +import boomerang.jimple.AllocVal; +import boomerang.jimple.Statement; +import boomerang.jimple.Val; +import boomerang.results.ForwardBoomerangResults; import com.google.common.collect.HashMultimap; import com.google.common.collect.Lists; import com.google.common.collect.Maps; @@ -19,13 +13,6 @@ import com.google.common.collect.Sets; import com.google.common.collect.Table; import com.google.common.collect.Table.Cell; - -import boomerang.callgraph.ObservableICFG; -import boomerang.debugger.Debugger; -import boomerang.jimple.AllocVal; -import boomerang.jimple.Statement; -import boomerang.jimple.Val; -import boomerang.results.ForwardBoomerangResults; import crypto.analysis.errors.AbstractError; import crypto.analysis.errors.IncompleteOperationError; import crypto.analysis.errors.RequiredPredicateError; @@ -61,7 +48,6 @@ import soot.jimple.Constant; import soot.jimple.IntConstant; import soot.jimple.InvokeExpr; -import soot.jimple.Stmt; import soot.jimple.StringConstant; import soot.jimple.ThrowStmt; import sync.pds.solver.nodes.Node; @@ -69,6 +55,18 @@ import typestate.finiteautomata.ITransition; import typestate.finiteautomata.State; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.Collection; +import java.util.Collections; +import java.util.HashMap; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Map.Entry; +import java.util.Set; +import java.util.stream.Collectors; + public class AnalysisSeedWithSpecification extends IAnalysisSeed { private final ClassSpecification spec; @@ -182,9 +180,10 @@ private void computeTypestateErrorUnits() { private void computeTypestateErrorsForEndOfObjectLifeTime() { Table endPathOfPropagation = results.getObjectDestructingStatements(); + Map> incompleteOperations = new HashMap<>(); for (Cell c : endPathOfPropagation.cellSet()) { - Set expectedMethodsToBeCalled = Sets.newHashSet(); + Set expectedMethodsToBeCalled = new HashSet<>(); for (ITransition n : c.getValue().values()) { if (n.to() == null) { @@ -209,18 +208,89 @@ private void computeTypestateErrorsForEndOfObjectLifeTime() { } if (!expectedMethodsToBeCalled.isEmpty()) { - Statement s = c.getRowKey(); - Val val = c.getColumnKey(); + incompleteOperations.put(c.getRowKey(), expectedMethodsToBeCalled); + } + } + + // No incomplete operations were found + if (incompleteOperations.entrySet().isEmpty()) { + return; + } + + /* If there is only one incomplete operation, then there is only one dataflow path. Hence, + * the error can be reported directly. + */ + if (incompleteOperations.entrySet().size() == 1) { + Entry> entry = incompleteOperations.entrySet().iterator().next(); + Statement s = entry.getKey(); + Set methodsToBeCalled = entry.getValue(); + + if (!s.getUnit().isPresent()) { + return; + } + + if (s.getUnit().get() instanceof ThrowStmt) { + return; + } + + IncompleteOperationError incompleteOperationError = new IncompleteOperationError(this, s, spec.getRule(), methodsToBeCalled); + this.addError(incompleteOperationError); + cryptoScanner.getAnalysisListener().reportError(this, incompleteOperationError); + } + + /* Multiple incomplete operations were found. Depending on the dataflow paths, the + * errors are reported: + * 1) A dataflow path ends in an accepting state: No error is reported + * 2) A dataflow path does not end in an accepting state: Report the error on the last used statement on this path + */ + if (incompleteOperations.size() > 1) { + for (Entry> entry : incompleteOperations.entrySet()) { + Statement statement = entry.getKey(); + Set expectedMethodsToBeCalled = entry.getValue(); + + // Extract the called SootMethod from the statement + if (!statement.getUnit().isPresent()) { + continue; + } + + if (statement.getUnit().get() instanceof ThrowStmt) { + continue; + } + + if (!statement.getUnit().get().containsInvokeExpr()) { + continue; + } - if (!(s.getUnit().get() instanceof ThrowStmt)) { - IncompleteOperationError incompleteOperationError = new IncompleteOperationError(s, val, getSpec().getRule(), this, expectedMethodsToBeCalled); - this.addError(incompleteOperationError); - cryptoScanner.getAnalysisListener().reportError(this, incompleteOperationError); + // Only if the path does not end in an accepting state, the error should be reported + InvokeExpr invokeExpr = statement.getUnit().get().getInvokeExpr(); + if (isMethodToAcceptingState(invokeExpr.getMethod())) { + continue; } + + IncompleteOperationError incompleteOperationError = new IncompleteOperationError(this, statement, spec.getRule(), expectedMethodsToBeCalled, true); + this.addError(incompleteOperationError); + cryptoScanner.getAnalysisListener().reportError(this, incompleteOperationError); } } } + private boolean isMethodToAcceptingState(SootMethod method) { + Collection transitions = spec.getRule().getUsagePattern().getAllTransitions(); + Collection methods = CrySLMethodToSootMethod.v().convert(method); + + for (TransitionEdge edge : transitions) { + if (edge.getLabel().stream().noneMatch(e -> methods.contains(e))) { + continue; + } + + if (edge.to().getAccepting()) { + return true; + } + } + + return false; + } + private void typeStateChangeAtStatement(Statement curr, State stateNode) { if (typeStateChange.put(curr, stateNode)) { if (stateNode instanceof ReportingErrorStateNode) { diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/errors/IncompleteOperationError.java b/CryptoAnalysis/src/main/java/crypto/analysis/errors/IncompleteOperationError.java index e02762d29..3f04cecf8 100644 --- a/CryptoAnalysis/src/main/java/crypto/analysis/errors/IncompleteOperationError.java +++ b/CryptoAnalysis/src/main/java/crypto/analysis/errors/IncompleteOperationError.java @@ -1,52 +1,69 @@ package crypto.analysis.errors; -import java.util.Collection; -import java.util.HashSet; -import java.util.Set; - +import boomerang.jimple.Statement; import com.google.common.base.Joiner; -import com.google.common.base.Optional; import com.google.common.collect.Sets; - -import boomerang.jimple.Statement; -import boomerang.jimple.Val; import crypto.analysis.IAnalysisSeed; import crypto.rules.CrySLRule; import soot.SootMethod; import soot.jimple.InvokeExpr; import soot.jimple.Stmt; +import java.util.Collection; +import java.util.HashSet; +import java.util.Optional; +import java.util.Set; -/** This class defines-IncompleteOperationError: - * - *Found when the usage of an object may be incomplete + +/**

This class defines-IncompleteOperationError:

* - *For example a Cipher object may be initialized but never been used for encryption or decryption, this may render the code dead. - *This error heavily depends on the computed call graph (CHA by default) + *

Found when the usage of an object may be incomplete. If there are + * multiple paths, and at least one path introduces an incomplete operation, + * the analysis indicates that there is a potential path with missing calls.

* - * */ - + *

For example a Cipher object may be initialized but never been used for encryption or decryption, this may render the code dead. + * This error heavily depends on the computed call graph (CHA by default).

+ */ public class IncompleteOperationError extends ErrorWithObjectAllocation{ - private Val errorVariable; - private Collection expectedMethodCalls; - private Set expectedMethodCallsSet = Sets.newHashSet(); + private final Collection expectedMethodCalls; + private final Set expectedMethodCallsSet; + private final boolean multiplePaths; - public IncompleteOperationError(Statement errorLocation, - Val errorVariable, CrySLRule rule, IAnalysisSeed objectLocation, Collection expectedMethodsToBeCalled) { + /** + * Create an IncompleteOperationError, if there is only one dataflow path, where the + * incomplete operation occurs. + * + * @param objectLocation the seed for the incomplete operation + * @param errorLocation the statement of the last usage of the seed + * @param rule the CrySL rule for the seed + * @param expectedMethodsToBeCalled the methods that are expected to be called + */ + public IncompleteOperationError(IAnalysisSeed objectLocation, Statement errorLocation, CrySLRule rule, Collection expectedMethodsToBeCalled) { + this(objectLocation, errorLocation, rule, expectedMethodsToBeCalled, false); + } + + /** + * Create an IncompleteOperationError, if there is at least one dataflow path, where an + * incomplete operation occurs. + * + * @param objectLocation the seed for the incomplete operation + * @param errorLocation the statement of the last usage of the seed + * @param rule the CrySL rule for the seed + * @param expectedMethodsToBeCalled the methods that are expected to be called + * @param multiplePaths set to true, if there are multiple paths (default: false) + */ + public IncompleteOperationError(IAnalysisSeed objectLocation, Statement errorLocation, CrySLRule rule, Collection expectedMethodsToBeCalled, boolean multiplePaths) { super(errorLocation, rule, objectLocation); - this.errorVariable = errorVariable; - this.expectedMethodCalls = expectedMethodsToBeCalled; - + this.expectedMethodCalls = expectedMethodsToBeCalled; + this.multiplePaths = multiplePaths; + + this.expectedMethodCallsSet = new HashSet<>(); for (SootMethod method : expectedMethodCalls) { this.expectedMethodCallsSet.add(method.getSignature()); - } + } } - public Val getErrorVariable() { - return errorVariable; - } - public Collection getExpectedMethodCalls() { return expectedMethodCalls; } @@ -57,21 +74,52 @@ public void accept(ErrorVisitor visitor){ @Override public String toErrorMarkerString() { - Collection expectedCalls = getExpectedMethodCalls(); - final StringBuilder msg = new StringBuilder(); + if (multiplePaths) { + return getErrorMarkerStringForMultipleDataflowPaths(); + } else { + return getErrorMarkerStringForSingleDataflowPath(); + } + } + + private String getErrorMarkerStringForSingleDataflowPath() { + StringBuilder msg = new StringBuilder(); msg.append("Operation"); msg.append(getObjectType()); - msg.append(" object not completed. Expected call to "); - final Set altMethods = new HashSet<>(); - for (final SootMethod expectedCall : expectedCalls) { + msg.append(" not completed. Expected call to "); + + Set altMethods = getFormattedExpectedCalls(); + msg.append(Joiner.on(", ").join(altMethods)); + return msg.toString(); + } + + private String getErrorMarkerStringForMultipleDataflowPaths() { + if (!getErrorLocation().isCallsite() || !getErrorLocation().getUnit().isPresent()) { + return "Unable to describe error"; + } + StringBuilder msg = new StringBuilder(); + msg.append("Call to "); + + InvokeExpr invokeExpr = getErrorLocation().getUnit().get().getInvokeExpr(); + msg.append(invokeExpr.getMethod().getName()); + msg.append(getObjectType()); + msg.append(" is on a dataflow path with an incomplete operation. Potential missing call to "); + + Set altMethods = getFormattedExpectedCalls(); + msg.append(Joiner.on(", ").join(altMethods)); + return msg.toString(); + } + + private Set getFormattedExpectedCalls() { + Set altMethods = new HashSet<>(); + + for (SootMethod expectedCall : getExpectedMethodCalls()) { if (stmtInvokesExpectedCallName(expectedCall.getName())){ altMethods.add(expectedCall.getSignature().replace("<", "").replace(">", "")); } else { altMethods.add(expectedCall.getName().replace("<", "").replace(">", "")); } } - msg.append(Joiner.on(", ").join(altMethods)); - return msg.toString(); + return altMethods; } /** @@ -80,19 +128,24 @@ public String toErrorMarkerString() { */ private boolean stmtInvokesExpectedCallName(String expectedCallName){ Statement errorLocation = getErrorLocation(); - if (errorLocation.isCallsite()){ - Optional stmtOptional = errorLocation.getUnit(); - if (stmtOptional.isPresent()){ - Stmt stmt = stmtOptional.get(); - if (stmt.containsInvokeExpr()){ - InvokeExpr call = stmt.getInvokeExpr(); - SootMethod calledMethod = call.getMethod(); - if (calledMethod.getName().equals(expectedCallName)){ - return true; - } - } - } + + if (!errorLocation.isCallsite()) { + return false; } + + Optional stmtOptional = errorLocation.getUnit().toJavaUtil(); + + if (!stmtOptional.isPresent()) { + return false; + } + + Stmt stmt = stmtOptional.get(); + if (stmt.containsInvokeExpr()) { + InvokeExpr call = stmt.getInvokeExpr(); + SootMethod calledMethod = call.getMethod(); + return calledMethod.getName().equals(expectedCallName); + } + return false; } diff --git a/CryptoAnalysis/src/test/java/tests/headless/BouncyCastleHeadlessTest.java b/CryptoAnalysis/src/test/java/tests/headless/BouncyCastleHeadlessTest.java index 142d4aac3..804aceacd 100644 --- a/CryptoAnalysis/src/test/java/tests/headless/BouncyCastleHeadlessTest.java +++ b/CryptoAnalysis/src/test/java/tests/headless/BouncyCastleHeadlessTest.java @@ -35,7 +35,7 @@ public void testBCMacExamples() { setErrorsCount("", RequiredPredicateError.class, 1); setErrorsCount("", TypestateError.class, 1); - setErrorsCount("", IncompleteOperationError.class, 2); + setErrorsCount("", IncompleteOperationError.class, 1); setErrorsCount("", RequiredPredicateError.class, 1); setErrorsCount("", RequiredPredicateError.class, 3); diff --git a/CryptoAnalysis/src/test/java/tests/headless/BragaCryptoGoodusesTest.java b/CryptoAnalysis/src/test/java/tests/headless/BragaCryptoGoodusesTest.java index a86d28503..95b3db1d7 100644 --- a/CryptoAnalysis/src/test/java/tests/headless/BragaCryptoGoodusesTest.java +++ b/CryptoAnalysis/src/test/java/tests/headless/BragaCryptoGoodusesTest.java @@ -46,7 +46,7 @@ public void alwaysDefineCSPExamples() { setErrorsCount("", ConstraintError.class, 1); setErrorsCount("", TypestateError.class, 1); setErrorsCount("", ConstraintError.class, 1); - setErrorsCount("", IncompleteOperationError.class, 4); + setErrorsCount("", IncompleteOperationError.class, 2); setErrorsCount("", RequiredPredicateError.class, 5); scanner.exec(); @@ -67,7 +67,7 @@ public void avoidCodingErrorsExamples() { setErrorsCount("", RequiredPredicateError.class, 4); setErrorsCount("", ForbiddenMethodError.class, 1); setErrorsCount("", TypestateError.class, 1); - setErrorsCount("", IncompleteOperationError.class, 4); + setErrorsCount("", IncompleteOperationError.class, 2); setErrorsCount("", RequiredPredicateError.class, 4); setErrorsCount("", TypestateError.class, 2); @@ -103,25 +103,25 @@ public void avoidDeterministicRSAExamples() { HeadlessCryptoScanner scanner = createScanner(mavenProject); // positive test case - setErrorsCount("", IncompleteOperationError.class, 4); + setErrorsCount("", IncompleteOperationError.class, 2); setErrorsCount("", RequiredPredicateError.class, 0); setErrorsCount("", ConstraintError.class, 0); setErrorsCount("", TypestateError.class, 0); // negative test case - setErrorsCount("", IncompleteOperationError.class, 4); + setErrorsCount("", IncompleteOperationError.class, 2); setErrorsCount("", RequiredPredicateError.class, 5); setErrorsCount("", ConstraintError.class, 1); setErrorsCount("", TypestateError.class, 0); // positive test case - setErrorsCount("", IncompleteOperationError.class, 4); + setErrorsCount("", IncompleteOperationError.class, 2); setErrorsCount("", RequiredPredicateError.class, 0); setErrorsCount("", ConstraintError.class, 0); setErrorsCount("", TypestateError.class, 0); // negative test case - setErrorsCount("", IncompleteOperationError.class, 4); + setErrorsCount("", IncompleteOperationError.class, 2); setErrorsCount("", RequiredPredicateError.class, 5); setErrorsCount("", ConstraintError.class, 1); setErrorsCount("", TypestateError.class, 0); @@ -261,10 +261,10 @@ public void avoidInsecureDefaultsExamples() { setErrorsCount("", ForbiddenMethodError.class, 1); setErrorsCount("", TypestateError.class, 1); setErrorsCount("", ConstraintError.class, 1); - setErrorsCount("", IncompleteOperationError.class, 4); + setErrorsCount("", IncompleteOperationError.class, 3); setErrorsCount("", RequiredPredicateError.class, 5); setErrorsCount("", TypestateError.class, 2); - setErrorsCount("", IncompleteOperationError.class, 4); + setErrorsCount("", IncompleteOperationError.class, 3); setErrorsCount("", RequiredPredicateError.class, 5); setErrorsCount("", TypestateError.class, 2); @@ -736,10 +736,10 @@ public void randomIVExamples() { setErrorsCount("", ConstraintError.class, 2); setErrorsCount("", TypestateError.class, 2); setErrorsCount("", RequiredPredicateError.class, 1); - setErrorsCount("", IncompleteOperationError.class, 4); + setErrorsCount("", IncompleteOperationError.class, 3); setErrorsCount("", TypestateError.class, 2); setErrorsCount("", RequiredPredicateError.class, 1); - setErrorsCount("", IncompleteOperationError.class, 4); + setErrorsCount("", IncompleteOperationError.class, 3); setErrorsCount("", TypestateError.class, 2); setErrorsCount("", ConstraintError.class, 2); diff --git a/CryptoAnalysis/src/test/java/tests/headless/BragaCryptoMisusesTest.java b/CryptoAnalysis/src/test/java/tests/headless/BragaCryptoMisusesTest.java index 558459bff..01c8a15a7 100644 --- a/CryptoAnalysis/src/test/java/tests/headless/BragaCryptoMisusesTest.java +++ b/CryptoAnalysis/src/test/java/tests/headless/BragaCryptoMisusesTest.java @@ -103,10 +103,10 @@ public void buggyIVgenExamples() { setErrorsCount("", TypestateError.class, 2); setErrorsCount("", RequiredPredicateError.class, 7); - setErrorsCount("", IncompleteOperationError.class, 4); + setErrorsCount("", IncompleteOperationError.class, 2); setErrorsCount("", TypestateError.class, 2); setErrorsCount("", RequiredPredicateError.class, 7); - setErrorsCount("", IncompleteOperationError.class, 4); + setErrorsCount("", IncompleteOperationError.class, 2); scanner.exec(); assertErrors(); @@ -120,10 +120,10 @@ public void constantIVExamples() { MavenProject mavenProject = createAndCompile(mavenProjectPath); HeadlessCryptoScanner scanner = createScanner(mavenProject); - setErrorsCount("", IncompleteOperationError.class, 4); + setErrorsCount("", IncompleteOperationError.class, 2); setErrorsCount("", TypestateError.class, 2); setErrorsCount("", RequiredPredicateError.class, 7); - setErrorsCount("", IncompleteOperationError.class, 4); + setErrorsCount("", IncompleteOperationError.class, 2); setErrorsCount("", TypestateError.class, 2); setErrorsCount("", RequiredPredicateError.class, 7); setErrorsCount("", RequiredPredicateError.class, 1); @@ -217,19 +217,19 @@ public void deterministicCryptoExamples() { setErrorsCount("", ForbiddenMethodError.class, 1); setErrorsCount("", ConstraintError.class, 1); - setErrorsCount("", IncompleteOperationError.class, 4); + setErrorsCount("", IncompleteOperationError.class, 2); setErrorsCount("", RequiredPredicateError.class, 5); setErrorsCount("", TypestateError.class, 0); setErrorsCount("", ConstraintError.class, 3); - setErrorsCount("", IncompleteOperationError.class, 4); + setErrorsCount("", IncompleteOperationError.class, 2); setErrorsCount("", RequiredPredicateError.class, 5); setErrorsCount("", TypestateError.class, 0); setErrorsCount("", ConstraintError.class, 1); - setErrorsCount("", IncompleteOperationError.class, 4); + setErrorsCount("", IncompleteOperationError.class, 2); setErrorsCount("", RequiredPredicateError.class, 5); setErrorsCount("", TypestateError.class, 0); setErrorsCount("", ConstraintError.class, 1); - setErrorsCount("", IncompleteOperationError.class, 4); + setErrorsCount("", IncompleteOperationError.class, 2); setErrorsCount("", RequiredPredicateError.class, 5); setErrorsCount("", TypestateError.class, 0); @@ -246,10 +246,10 @@ public void deterministicSymEncExamples() { HeadlessCryptoScanner scanner = createScanner(mavenProject); setErrorsCount("", ConstraintError.class, 6); - setErrorsCount("", IncompleteOperationError.class, 12); + setErrorsCount("", IncompleteOperationError.class, 6); setErrorsCount("", TypestateError.class, 0); setErrorsCount("", ForbiddenMethodError.class, 1); - setErrorsCount("", IncompleteOperationError.class, 4); + setErrorsCount("", IncompleteOperationError.class, 2); setErrorsCount("", TypestateError.class, 0); scanner.exec(); @@ -267,7 +267,7 @@ public void fixedSeedExamples() { setErrorsCount("", TypestateError.class, 4); setErrorsCount("", RequiredPredicateError.class, 10); setErrorsCount("", ConstraintError.class, 2); - setErrorsCount("", IncompleteOperationError.class, 6); + setErrorsCount("", IncompleteOperationError.class, 4); setErrorsCount("", RequiredPredicateError.class, 2); setErrorsCount("", RequiredPredicateError.class, 2); setErrorsCount("", RequiredPredicateError.class, 2); @@ -425,13 +425,13 @@ public void insecureDefaultExamples() { setErrorsCount("", TypestateError.class, 1); // positive test case - setErrorsCount("", IncompleteOperationError.class, 4); + setErrorsCount("", IncompleteOperationError.class, 2); setErrorsCount("", RequiredPredicateError.class, 0); setErrorsCount("", TypestateError.class, 0); setErrorsCount("", ConstraintError.class, 0); // negative test case - setErrorsCount("", IncompleteOperationError.class, 4); + setErrorsCount("", IncompleteOperationError.class, 2); setErrorsCount("", RequiredPredicateError.class, 5); setErrorsCount("", TypestateError.class, 0); setErrorsCount("", ConstraintError.class, 1); @@ -450,37 +450,37 @@ public void insecurePaddingExamples() { // positive test case setErrorsCount("", TypestateError.class, 0); - setErrorsCount("", IncompleteOperationError.class, 4); + setErrorsCount("", IncompleteOperationError.class, 2); setErrorsCount("", RequiredPredicateError.class, 0); setErrorsCount("", ConstraintError.class, 2); // negative test case setErrorsCount("", TypestateError.class, 0); - setErrorsCount("", IncompleteOperationError.class, 4); + setErrorsCount("", IncompleteOperationError.class, 2); setErrorsCount("", RequiredPredicateError.class, 5); setErrorsCount("", ConstraintError.class, 3); // positive test case setErrorsCount("", TypestateError.class, 0); - setErrorsCount("", IncompleteOperationError.class, 4); + setErrorsCount("", IncompleteOperationError.class, 2); setErrorsCount("", RequiredPredicateError.class, 0); setErrorsCount("", ConstraintError.class, 0); // negative test case setErrorsCount("", TypestateError.class, 0); - setErrorsCount("", IncompleteOperationError.class, 4); + setErrorsCount("", IncompleteOperationError.class, 2); setErrorsCount("", RequiredPredicateError.class, 5); setErrorsCount("", ConstraintError.class, 1); // positive test case setErrorsCount("", TypestateError.class, 0); - setErrorsCount("", IncompleteOperationError.class, 4); + setErrorsCount("", IncompleteOperationError.class, 2); setErrorsCount("", RequiredPredicateError.class, 0); setErrorsCount("", ConstraintError.class, 0); // negative test case setErrorsCount("", TypestateError.class, 0); - setErrorsCount("", IncompleteOperationError.class, 4); + setErrorsCount("", IncompleteOperationError.class, 2); setErrorsCount("", RequiredPredicateError.class, 5); setErrorsCount("", ConstraintError.class, 1); @@ -562,7 +562,7 @@ public void insecureStreamCipherExamples() { setErrorsCount("", TypestateError.class, 1); setErrorsCount("", RequiredPredicateError.class, 7); - setErrorsCount("", IncompleteOperationError.class, 3); + setErrorsCount("", IncompleteOperationError.class, 1); setErrorsCount("", RequiredPredicateError.class, 5); setErrorsCount("", TypestateError.class, 2); @@ -848,7 +848,7 @@ public void undefinedCSPExamples() { setErrorsCount("", ConstraintError.class, 2); setErrorsCount("", ConstraintError.class, 1); setErrorsCount("", RequiredPredicateError.class, 5); - setErrorsCount("", IncompleteOperationError.class, 4); + setErrorsCount("", IncompleteOperationError.class, 2); scanner.exec(); assertErrors(); diff --git a/CryptoAnalysis/src/test/java/tests/headless/StaticAnalysisDemoTest.java b/CryptoAnalysis/src/test/java/tests/headless/StaticAnalysisDemoTest.java index 93edcb4b0..90df1fd50 100644 --- a/CryptoAnalysis/src/test/java/tests/headless/StaticAnalysisDemoTest.java +++ b/CryptoAnalysis/src/test/java/tests/headless/StaticAnalysisDemoTest.java @@ -113,7 +113,7 @@ public void oracleExample() { setErrorsCount("", ConstraintError.class, 1); //TODO: This is wrong. setErrorsCount("", TypestateError.class, 0); - setErrorsCount("", IncompleteOperationError.class, 2); + setErrorsCount("", IncompleteOperationError.class, 1); setErrorsCount("", ConstraintError.class, 1); scanner.exec();