| createMemUnionWidening2(String, String, String) |  | 0% | | n/a | 1 | 1 | 5 | 5 | 1 | 1 |
| createMemHavocSidecond(String, String) | | 0% | | n/a | 1 | 1 | 4 | 4 | 1 | 1 |
| createMemWidening(String) | | 0% | | n/a | 1 | 1 | 4 | 4 | 1 | 1 |
| transformCore(AST) |  | 83% | | 87% | 1 | 5 | 2 | 15 | 0 | 1 |
| joinSource(Iterable) | | 85% | | 83% | 1 | 4 | 1 | 9 | 0 | 1 |
| inductionStepWithAssigns(LoopContractBlock) | | 96% | | 50% | 1 | 2 | 0 | 24 | 0 | 1 |
| createConclusion(LoopContractBlock, String) | | 95% | | 75% | 1 | 3 | 0 | 19 | 0 | 1 |
| transformLoopInFunction(BlockItemNode) | | 96% | | 90% | 1 | 6 | 1 | 22 | 0 | 1 |
| inductionStepInferringAssigns(LoopContractBlock, String) | | 100% | | n/a | 0 | 1 | 0 | 27 | 0 | 1 |
| unionLoopAssigns(List, String) | | 100% | | 100% | 0 | 2 | 0 | 16 | 0 | 1 |
| transformLoopWorker(LoopContractBlock) | | 100% | | 100% | 0 | 2 | 0 | 17 | 0 | 1 |
| createAssertion(ExpressionNode, int) | | 100% | | 100% | 0 | 5 | 0 | 16 | 0 | 1 |
| toNDBranch(LoopContractBlock, List) | | 100% | | n/a | 0 | 1 | 0 | 12 | 0 | 1 |
| getForLoopInitializers(LoopContractBlock) | | 100% | | 100% | 0 | 5 | 0 | 13 | 0 | 1 |
| createMemUnionWidening(String, String, String) | | 100% | | n/a | 0 | 1 | 0 | 8 | 0 | 1 |
| LoopContractTransformerWorker(String, ASTFactory) | | 100% | | n/a | 0 | 1 | 0 | 10 | 0 | 1 |
| checkFrameCondition(String, String) | | 100% | | n/a | 0 | 1 | 0 | 8 | 0 | 1 |
| createMemHavoc(String) | | 100% | | n/a | 0 | 1 | 0 | 8 | 0 | 1 |
| endlessWhileLoop() | | 100% | | n/a | 0 | 1 | 0 | 5 | 0 | 1 |
| wrapLoopBody(LoopContractBlock) | | 100% | | n/a | 0 | 1 | 0 | 6 | 0 | 1 |
| getForLoopIncrementors(LoopContractBlock) | | 100% | | 100% | 0 | 3 | 0 | 7 | 0 | 1 |
| createAssumptionPush(ExpressionNode) | | 100% | | n/a | 0 | 1 | 0 | 5 | 0 | 1 |
| createNDBinaryChoice() | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| createAssumptionPop() | | 100% | | n/a | 0 | 1 | 0 | 5 | 0 | 1 |
| createWriteSetPush() | | 100% | | n/a | 0 | 1 | 0 | 5 | 0 | 1 |
| createWriteSetPop(String) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| createAssignment(ExpressionNode, ExpressionNode) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| memTypeVariableDeclaration(String) | | 100% | | n/a | 0 | 1 | 0 | 3 | 0 | 1 |
| isLoopNode(ASTNode) | | 100% | | 100% | 0 | 3 | 0 | 3 | 0 | 1 |
| createMemEmptyCall() | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| isContractedLoop(LoopNode) | | 100% | | 75% | 1 | 3 | 0 | 2 | 0 | 1 |
| nextLoopTmpIdentifier() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| isFunctionDefinition(ASTNode) | | 100% | | 100% | 0 | 2 | 0 | 1 | 0 | 1 |
| isForLoop(LoopNode) | | 100% | | 100% | 0 | 2 | 0 | 1 | 0 | 1 |
| static {...} | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |