| allocate4ACSLValid(OperatorNode) |  | 0% | | 0% | 8 | 8 | 36 | 36 | 1 | 1 |
| refreshMemoryLocationSetExpression(ExpressionNode) |  | 19% | | 38% | 4 | 5 | 20 | 27 | 0 | 1 |
| processLvalueSetExpression(ExpressionNode, Map) | | 0% | | 0% | 5 | 5 | 20 | 20 | 1 | 1 |
| result2intermediate(ExpressionNode, MPIContractUtilities.TransformConfiguration) | | 35% | | 45% | 8 | 11 | 15 | 24 | 0 | 1 |
| old2ValueAt(ExpressionNode, ExpressionNode, MPIContractUtilities.TransformConfiguration) | | 48% | | 67% | 4 | 7 | 4 | 18 | 0 | 1 |
| createHavocCall(ExpressionNode) | | 0% | | n/a | 1 | 1 | 7 | 7 | 1 | 1 |
| allocation4Valids(ExpressionNode, MPIContractUtilities.TransformConfiguration) | | 75% | | 70% | 5 | 11 | 4 | 24 | 0 | 1 |
| createMPIBarrier(ExpressionNode) | | 0% | | n/a | 1 | 1 | 5 | 5 | 1 | 1 |
| mpidatatypeExtent2intermediateVariable(ExpressionNode, LinkedList) | | 84% | | 44% | 6 | 9 | 5 | 39 | 0 | 1 |
| makeItRange(ExpressionNode) | | 28% | | 17% | 3 | 4 | 3 | 5 | 0 | 1 |
| withStatementWrapper(StatementNode, ExpressionNode, List, MPIContractUtilities.TransformConfiguration) | | 89% | | 77% | 5 | 12 | 3 | 37 | 0 | 1 |
| substituteAllValid2True(ExpressionNode) | | 82% | | 67% | 4 | 10 | 3 | 24 | 0 | 1 |
| ACSLPrimitives2CIVLC(ExpressionNode, MPIContractUtilities.TransformConfiguration) | | 0% | | n/a | 1 | 1 | 2 | 2 | 1 | 1 |
| decast(ExpressionNode) | | 0% | | 0% | 2 | 2 | 4 | 4 | 1 | 1 |
| replaceWithValueAt(ExpressionNode, ExpressionNode, ExpressionNode, ExpressionNode, ExpressionNode) | | 78% | | 25% | 4 | 5 | 2 | 15 | 0 | 1 |
| transformClause2Assumption(ExpressionNode, ExpressionNode, ExpressionNode, List, MPIContractUtilities.TransformConfiguration) | | 96% | | 86% | 2 | 8 | 1 | 27 | 0 | 1 |
| transformClause2Checking(ExpressionNode, ExpressionNode, ExpressionNode, List, MPIContractUtilities.TransformConfiguration) | | 92% | | 80% | 2 | 6 | 1 | 17 | 0 | 1 |
| on2ValueAt(ExpressionNode, ExpressionNode, MPIContractUtilities.TransformConfiguration) | | 95% | | 80% | 2 | 6 | 0 | 14 | 0 | 1 |
| MPIDatatype2datatypeExtentSERemove(ExpressionNode) | | 93% | | 86% | 2 | 8 | 0 | 13 | 0 | 1 |
| mpiRegion2assign(MPIContractExpressionNode) | | 93% | | 50% | 2 | 3 | 0 | 10 | 0 | 1 |
| mpiExtentSERemove(ExpressionNode) | | 91% | | 80% | 2 | 6 | 0 | 12 | 0 | 1 |
| static {...} | | 75% | | 50% | 1 | 2 | 0 | 1 | 0 | 1 |
| createMPICommEmptyCall(ExpressionNode, MPICollectiveBlockNode.MPICommunicatorMode) | | 98% | | 50% | 1 | 2 | 0 | 8 | 0 | 1 |
| transformMPICollectiveBlock4Target(FunctionContractBlock, MPIContractUtilities.TransformConfiguration) | | 100% | | 100% | 0 | 4 | 0 | 42 | 0 | 1 |
| transformMPICollectiveBlock4Callee(FunctionContractBlock, MPIContractUtilities.TransformConfiguration) | | 100% | | 100% | 0 | 4 | 0 | 38 | 0 | 1 |
| createElaborateFor(ExpressionNode) | | 100% | | n/a | 0 | 1 | 0 | 22 | 0 | 1 |
| createAllocation(ExpressionNode, TypeNode, ExpressionNode, Source) | | 100% | | n/a | 0 | 1 | 0 | 21 | 0 | 1 |
| transformAssignsClause(FunctionContractBlock.ConditionalClauses) | | 100% | | 88% | 1 | 5 | 0 | 17 | 0 | 1 |
| allocate4MPIValid(MPIContractExpressionNode) | | 100% | | n/a | 0 | 1 | 0 | 8 | 0 | 1 |
| mpiConstantsInitialization(ExpressionNode) | | 100% | | n/a | 0 | 1 | 0 | 10 | 0 | 1 |
| createMPICommRankCall(ExpressionNode, ExpressionNode) | | 100% | | n/a | 0 | 1 | 0 | 9 | 0 | 1 |
| createMPICommSizeCall(ExpressionNode, ExpressionNode) | | 100% | | n/a | 0 | 1 | 0 | 9 | 0 | 1 |
| ACSLSideEffectRemoving(ExpressionNode, MPIContractUtilities.TransformConfiguration) | | 100% | | 100% | 0 | 2 | 0 | 9 | 0 | 1 |
| createMPISnapshotCall(ExpressionNode) | | 100% | | n/a | 0 | 1 | 0 | 7 | 0 | 1 |
| createAssertion(ExpressionNode) | | 100% | | n/a | 0 | 1 | 0 | 7 | 0 | 1 |
| createCollateStateInitializer(String, ExpressionNode) | | 100% | | n/a | 0 | 1 | 0 | 6 | 0 | 1 |
| ContractClauseTransformer(ASTFactory) | | 100% | | n/a | 0 | 1 | 0 | 9 | 0 | 1 |
| createMPIExtentofCall(ExpressionNode) | | 100% | | n/a | 0 | 1 | 0 | 5 | 0 | 1 |
| createAssumption(ExpressionNode) | | 100% | | n/a | 0 | 1 | 0 | 6 | 0 | 1 |
| ACSLPrimitives2CIVLC(ExpressionNode, ExpressionNode, MPIContractUtilities.TransformConfiguration) | | 100% | | n/a | 0 | 1 | 0 | 5 | 0 | 1 |
| createCollateGetStateCall(ExpressionNode, Source) | | 100% | | n/a | 0 | 1 | 0 | 3 | 0 | 1 |
| identifierExpressionNode(Source, String) | | 100% | | n/a | 0 | 1 | 0 | 2 | 0 | 1 |