| transformTargetFunction(FunctionDefinitionNode, boolean) |  | 0% | | 0% | 14 | 14 | 77 | 77 | 1 | 1 |
| transformContractedFunction(FunctionDeclarationNode, boolean) | | 0% | | 0% | 15 | 15 | 79 | 79 | 1 | 1 |
| condition2Range(ExpressionNode) | | 0% | | 0% | 27 | 27 | 73 | 73 | 1 | 1 |
| transformRemoteInQuantifiedExpressionWork(QuantifiedExpressionNode) | | 0% | | 0% | 14 | 14 | 60 | 60 | 1 | 1 |
| replaceOldExpressionNodes4Local(ExpressionNode, boolean) | | 0% | | 0% | 6 | 6 | 51 | 51 | 1 | 1 |
| getAndReplaceValidExprNodes(boolean, ExpressionNode) | | 0% | | 0% | 7 | 7 | 45 | 45 | 1 | 1 |
| transformLambdaWtRemoteInExtendedQuantifiedExpressionWork(ExtendedQuantifiedExpressionNode) | | 0% | | 0% | 6 | 6 | 46 | 46 | 1 | 1 |
| transformCollectiveEnsures4Target(ContractTransformerWorker.ParsedContractBlock) | | 0% | | 0% | 4 | 4 | 35 | 35 | 1 | 1 |
| createMallocStatementSequenceForValid(OperatorNode, FunctionDeclarationNode) | | 0% | | 0% | 7 | 7 | 38 | 38 | 1 | 1 |
| transformCoRequirements4Target(ContractTransformerWorker.ParsedContractBlock, Source, Source) | | 0% | | 0% | 7 | 7 | 31 | 31 | 1 | 1 |
| createMallocStatementSequenceForMPIValid(MPIContractExpressionNode) | | 0% | | n/a | 1 | 1 | 28 | 28 | 1 | 1 |
| createMallocStatementSequenceForMPIValid2(MPIContractExpressionNode) | | 0% | | 0% | 4 | 4 | 28 | 28 | 1 | 1 |
| transform(AST) | | 0% | | 0% | 9 | 9 | 35 | 35 | 1 | 1 |
| createStatements4AssignsArgumentSCRIPT(ExpressionNode, ExpressionNode, ExpressionNode) | | 0% | | 0% | 2 | 2 | 25 | 25 | 1 | 1 |
| translateEnsurance2Inference(ExpressionNode, ExpressionNode, ExpressionNode, List) | | 0% | | 0% | 6 | 6 | 22 | 22 | 1 | 1 |
| transformMPIDatatype2extentofDatatype(ExpressionNode) | | 0% | | 0% | 6 | 6 | 30 | 30 | 1 | 1 |
| conditionalAssigns4NT(ContractTransformerWorker.ConditionalClauses) | | 0% | | 0% | 6 | 6 | 25 | 25 | 1 | 1 |
| transformCoRequirements4NT(ContractTransformerWorker.ParsedContractBlock) | | 0% | | 0% | 3 | 3 | 23 | 23 | 1 | 1 |
| processSourceFileNodes(List, boolean) | | 0% | | 0% | 9 | 9 | 30 | 30 | 1 | 1 |
| mainFunction(FunctionDefinitionNode, boolean) | | 0% | | 0% | 2 | 2 | 23 | 23 | 1 | 1 |
| parseClausesInBehavior(SequenceNode, ContractTransformerWorker.ParsedContractBlock) | | 0% | | 0% | 12 | 12 | 31 | 31 | 1 | 1 |
| createMallocStatementWorker(ExpressionNode, ExpressionNode, TypeNode, Source) | | 0% | | n/a | 1 | 1 | 16 | 16 | 1 | 1 |
| translateConditionalPredicates(boolean, ExpressionNode, ExpressionNode) | | 0% | | 0% | 5 | 5 | 19 | 19 | 1 | 1 |
| processAssignsArgument(ExpressionNode) | | 0% | | 0% | 5 | 5 | 20 | 20 | 1 | 1 |
| createCollateArrivedCall(List, ExpressionNode) | | 0% | | 0% | 2 | 2 | 16 | 16 | 1 | 1 |
| createStatements4AssignsArgument(Stack, ExpressionNode, ExpressionNode) | | 0% | | 0% | 6 | 6 | 23 | 23 | 1 | 1 |
| commEmptyInAndOut(ExpressionNode, MPICollectiveBlockNode.MPICollectiveKind) | | 0% | | 0% | 2 | 2 | 13 | 13 | 1 | 1 |
| transformCoEnsurances4NT(ContractTransformerWorker.ParsedContractBlock) | | 0% | | 0% | 3 | 3 | 18 | 18 | 1 | 1 |
| parseFunctionContracts(SequenceNode) | | 0% | | 0% | 7 | 7 | 16 | 16 | 1 | 1 |
| createVariableDeclsAndInitsForDriver(FunctionTypeNode) | | 0% | | 0% | 4 | 4 | 21 | 21 | 1 | 1 |
| replaceOldExpressionNodes4collective(ExpressionNode, ExpressionNode) | | 0% | | 0% | 5 | 5 | 21 | 21 | 1 | 1 |
| processAssignsArgumentWorker(Stack, ExpressionNode, IdentifierExpressionNode) | | 0% | | 0% | 7 | 7 | 16 | 16 | 1 | 1 |
| createAssignAllGlobalFunction(Pair) | | 0% | | 0% | 2 | 2 | 14 | 14 | 1 | 1 |
| createMPIInitCall() | | 0% | | n/a | 1 | 1 | 13 | 13 | 1 | 1 |
| createTmpVarForDatatype(ExpressionNode, boolean) | | 0% | | 0% | 2 | 2 | 8 | 8 | 1 | 1 |
| createConditionalFreeCalls(ExpressionNode, List) | | 0% | | 0% | 3 | 3 | 14 | 14 | 1 | 1 |
| parseValidArgument(ExpressionNode) | | 0% | | 0% | 6 | 6 | 10 | 10 | 1 | 1 |
| transformRemoteInQuantifiedExpression(ASTNode) | | 0% | | 0% | 6 | 6 | 14 | 14 | 1 | 1 |
| transformLambdaWtRemoteInExtendedQuantifiedExpression(ASTNode) | | 0% | | 0% | 6 | 6 | 14 | 14 | 1 | 1 |
| getMPIValidExpressionNodes(boolean, ExpressionNode) | | 0% | | 0% | 6 | 6 | 15 | 15 | 1 | 1 |
| validArrayTypeCondition(ArrayTypeNode) | | 0% | | 0% | 4 | 4 | 17 | 17 | 1 | 1 |
| transformBoundVariableInValueAtOrRemoteWork(ASTNode) | | 0% | | 0% | 6 | 6 | 17 | 17 | 1 | 1 |
| createMPIContractEntered(List, ExpressionNode) | | 0% | | 0% | 2 | 2 | 8 | 8 | 1 | 1 |
| processConditionalAssignsArgumentNode(ExpressionNode, List) | | 0% | | 0% | 4 | 4 | 9 | 9 | 1 | 1 |
| isSourceFileFunctionContracted(FunctionDeclarationNode) | | 0% | | 0% | 7 | 7 | 14 | 14 | 1 | 1 |
| ContractTransformerWorker(ASTFactory, String) | | 0% | | n/a | 1 | 1 | 13 | 13 | 1 | 1 |
| hasNonTrivialSubExpressionWork(ExpressionNode) | | 0% | | 0% | 8 | 8 | 14 | 14 | 1 | 1 |
| createHavocCall(ExpressionNode) | | 0% | | n/a | 1 | 1 | 8 | 8 | 1 | 1 |
| havocForGlobalVariables(List) | | 0% | | 0% | 3 | 3 | 10 | 10 | 1 | 1 |
| isBoundVariableReference(IdentifierExpressionNode) | | 0% | | 0% | 8 | 8 | 13 | 13 | 1 | 1 |
| parseMPICollectiveBlock(MPICollectiveBlockNode) | | 0% | | 0% | 3 | 3 | 8 | 8 | 1 | 1 |
| elaboratePid4Remote(ASTNode) | | 0% | | 0% | 5 | 5 | 11 | 11 | 1 | 1 |
| createMPISnapshotCall(ExpressionNode) | | 0% | | n/a | 1 | 1 | 7 | 7 | 1 | 1 |
| createCollateStateDeclaration(String, ExpressionNode) | | 0% | | n/a | 1 | 1 | 7 | 7 | 1 | 1 |
| createMPICommRankCall(ExpressionNode, ExpressionNode) | | 0% | | n/a | 1 | 1 | 6 | 6 | 1 | 1 |
| createMPICommSizeCall(ExpressionNode, ExpressionNode) | | 0% | | n/a | 1 | 1 | 6 | 6 | 1 | 1 |
| createMPIAssignsCalls(MPIContractExpressionNode) | | 0% | | n/a | 1 | 1 | 6 | 6 | 1 | 1 |
| transformBoundVariableInValueAtOrRemote(ASTNode) | | 0% | | 0% | 5 | 5 | 11 | 11 | 1 | 1 |
| hasRemoteExpression(ASTNode) | | 0% | | 0% | 6 | 6 | 11 | 11 | 1 | 1 |
| replaceResultNode2Identifier(ExpressionNode) | | 0% | | 0% | 3 | 3 | 11 | 11 | 1 | 1 |
| hasNonTrivialSubExpression(ASTNode) | | 0% | | 0% | 4 | 4 | 8 | 8 | 1 | 1 |
| createMPIUnsnapshotCall(ExpressionNode, ExpressionNode) | | 0% | | n/a | 1 | 1 | 5 | 5 | 1 | 1 |
| createMPIContractEnters(ExpressionNode) | | 0% | | n/a | 1 | 1 | 5 | 5 | 1 | 1 |
| elaboratePid4RemoteWork(RemoteOnExpressionNode) | | 0% | | 0% | 3 | 3 | 6 | 6 | 1 | 1 |
| createAssertion(ExpressionNode) | | 0% | | n/a | 1 | 1 | 6 | 6 | 1 | 1 |
| createAssumption(ExpressionNode) | | 0% | | n/a | 1 | 1 | 6 | 6 | 1 | 1 |
| mpiConstantsInitialization(ExpressionNode) | | 0% | | n/a | 1 | 1 | 6 | 6 | 1 | 1 |
| execAfterComplete(ExpressionNode, StatementNode, Source) | | 0% | | 0% | 3 | 3 | 4 | 4 | 1 | 1 |
| declareTmpStateVar4OldExpr(Source, TypeNode, ExpressionNode) | | 0% | | n/a | 1 | 1 | 2 | 2 | 1 | 1 |
| checkWaitsfors(ExpressionNode, List, ExpressionNode, Source) | | 0% | | 0% | 2 | 2 | 6 | 6 | 1 | 1 |
| createTmpHeapVariable(Source, TypeNode) | | 0% | | n/a | 1 | 1 | 2 | 2 | 1 | 1 |
| isLHSorCastedLHSExpression(ExpressionNode) | | 0% | | 0% | 3 | 3 | 7 | 7 | 1 | 1 |
| createCollateCompleteCall(ExpressionNode, Source) | | 0% | | n/a | 1 | 1 | 3 | 3 | 1 | 1 |
| createMPIFinalizeCall() | | 0% | | n/a | 1 | 1 | 5 | 5 | 1 | 1 |
| transformRemoteWtBoundVariable(ExpressionNode) | | 0% | | 0% | 3 | 3 | 6 | 6 | 1 | 1 |
| makeItRange(ExpressionNode) | | 0% | | 0% | 2 | 2 | 4 | 4 | 1 | 1 |
| createMPIExtentofCall(ExpressionNode) | | 0% | | n/a | 1 | 1 | 2 | 2 | 1 | 1 |
| createSizeofDatatype(ExpressionNode) | | 0% | | n/a | 1 | 1 | 2 | 2 | 1 | 1 |
| factorOutSequentialBlock(List) | | 0% | | 0% | 2 | 2 | 5 | 5 | 1 | 1 |
| runAfterComplete(ExpressionNode, StatementNode, Source) | | 0% | | n/a | 1 | 1 | 2 | 2 | 1 | 1 |
| isLGTEOperator(OperatorNode.Operator) | | 0% | | 0% | 2 | 2 | 3 | 3 | 1 | 1 |
| static {...} | | 0% | | 0% | 2 | 2 | 1 | 1 | 1 | 1 |