| translateLoopFocusWindow(CommonTree, SimpleScope) |  | 0% | | 0% | 8 | 8 | 24 | 24 | 1 | 1 |
| translateRelationalChain(Source, CommonTree, SimpleScope) |  | 63% | | 46% | 16 | 23 | 15 | 62 | 0 | 1 |
| translateExpression(CommonTree, SimpleScope) | | 63% | | 63% | 12 | 32 | 16 | 44 | 0 | 1 |
| translateOperatorExpression(Source, CommonTree, SimpleScope) | | 59% | | 46% | 22 | 36 | 39 | 72 | 0 | 1 |
| translateFocusOrderedStatement(CommonTree, SimpleScope) | | 0% | | 0% | 3 | 3 | 14 | 14 | 1 | 1 |
| translateMPIExpressionNode(CommonTree, Source, SimpleScope) | | 56% | | 41% | 7 | 11 | 23 | 45 | 0 | 1 |
| translateLogicType(CommonTree, SimpleScope) | | 0% | | 0% | 6 | 6 | 12 | 12 | 1 | 1 |
| translateFocusAssert(CommonTree, Source) | | 0% | | 0% | 4 | 4 | 10 | 10 | 1 | 1 |
| translateFocusLoop(CommonTree, Source, SimpleScope) | | 0% | | 0% | 2 | 2 | 10 | 10 | 1 | 1 |
| generateContractNodes(SimpleScope) | | 67% | | 63% | 4 | 9 | 10 | 31 | 0 | 1 |
| translateSizeOf(Source, CommonTree, SimpleScope) | | 0% | | 0% | 3 | 3 | 8 | 8 | 1 | 1 |
| translateIdList(CommonTree, SimpleScope) | | 0% | | 0% | 2 | 2 | 7 | 7 | 1 | 1 |
| translateCompleteness(CommonTree, SimpleScope) | | 0% | | 0% | 3 | 3 | 11 | 11 | 1 | 1 |
| translateTransformContract(CommonTree, SimpleScope) | | 0% | | 0% | 3 | 3 | 7 | 7 | 1 | 1 |
| translateRelOp(CommonTree) | | 0% | | 0% | 6 | 6 | 14 | 14 | 1 | 1 |
| translateVariableIdent(CommonTree, SimpleScope, TypeNode) | | 58% | | 50% | 2 | 4 | 9 | 22 | 0 | 1 |
| translateTransform(CommonTree, SimpleScope) | | 0% | | 0% | 3 | 3 | 6 | 6 | 1 | 1 |
| translatePredicateClause(CommonTree, SimpleScope) | | 0% | | n/a | 1 | 1 | 6 | 6 | 1 | 1 |
| translateQuantifiedExpression(CommonTree, Source, SimpleScope) | | 79% | | 33% | 6 | 7 | 5 | 28 | 0 | 1 |
| checkIsSimpleInteger(ExpressionNode) | | 0% | | 0% | 5 | 5 | 7 | 7 | 1 | 1 |
| translateLoopContractBlock(CommonTree, SimpleScope) | | 63% | | 50% | 4 | 6 | 5 | 16 | 0 | 1 |
| translateContractClause(CommonTree, SimpleScope) | | 65% | | 63% | 4 | 11 | 4 | 13 | 0 | 1 |
| translateDependsEvent(CommonTree, SimpleScope) | | 50% | | 40% | 3 | 5 | 5 | 10 | 0 | 1 |
| translateLogicFunctionBody(CommonTree, CommonTree, TypeNode, SimpleScope) | | 81% | | 50% | 2 | 3 | 3 | 23 | 0 | 1 |
| translateFunctionContractBlock(CommonTree, SimpleScope) | | 76% | | 66% | 3 | 7 | 4 | 21 | 0 | 1 |
| translateRegularRange(Source, CommonTree, SimpleScope) | | 57% | | 25% | 2 | 3 | 4 | 10 | 0 | 1 |
| translateDependsEventBase(CommonTree, SimpleScope) | | 82% | | 62% | 3 | 8 | 3 | 23 | 0 | 1 |
| translateCType(CommonTree, CommonTree, SimpleScope) | | 68% | | 50% | 2 | 4 | 3 | 12 | 0 | 1 |
| translateWaitsfor(CommonTree, SimpleScope) | | 0% | | n/a | 1 | 1 | 3 | 3 | 1 | 1 |
| translateExtendedQuantification(Source, CommonTree, SimpleScope) | | 71% | | 16% | 5 | 6 | 9 | 20 | 0 | 1 |
| translateAllocation(CommonTree, SimpleScope, boolean) | | 0% | | n/a | 1 | 1 | 3 | 3 | 1 | 1 |
| translateObjectOf(Source, CommonTree, SimpleScope) | | 0% | | n/a | 1 | 1 | 3 | 3 | 1 | 1 |
| translateOld(Source, CommonTree, SimpleScope) | | 0% | | n/a | 1 | 1 | 3 | 3 | 1 | 1 |
| translateVariableIdentBase(CommonTree, Source, SimpleScope, TypeNode) | | 54% | | 33% | 2 | 3 | 3 | 8 | 0 | 1 |
| translateTypeExpr(CommonTree, SimpleScope) | | 56% | | 33% | 2 | 3 | 2 | 6 | 0 | 1 |
| translateCharacterConstant(Source, CommonTree) | | 0% | | n/a | 1 | 1 | 3 | 3 | 1 | 1 |
| translateStringLiteral(Source, CommonTree) | | 0% | | n/a | 1 | 1 | 3 | 3 | 1 | 1 |
| processDirectDeclarator(CommonTree, TypeNode, SimpleScope) | | 80% | | 71% | 2 | 5 | 2 | 11 | 0 | 1 |
| translateLoopClause(CommonTree, SimpleScope) | | 70% | | 33% | 2 | 3 | 2 | 8 | 0 | 1 |
| translateLogicFunctions(CommonTree, SimpleScope) | | 79% | | 66% | 2 | 4 | 1 | 10 | 0 | 1 |
| translateIdentifier(CommonTree) | | 73% | | 50% | 1 | 2 | 1 | 6 | 0 | 1 |
| error(String, CommonTree) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| translateMPIAbsentEventNode(CommonTree, SimpleScope) | | 92% | | 81% | 2 | 7 | 1 | 18 | 0 | 1 |
| translateFloatingConstant(Source, CommonTree) | | 0% | | n/a | 1 | 1 | 2 | 2 | 1 | 1 |
| processDeclarator(CommonTree, TypeNode, SimpleScope) | | 81% | | 50% | 1 | 2 | 1 | 6 | 0 | 1 |
| translateFalse(Source) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| translateMPICollectiveBlock(Source, CommonTree, SimpleScope) | | 92% | | 75% | 1 | 4 | 1 | 16 | 0 | 1 |
| translateMPIConstantNode(CommonTree, Source) | | 87% | | 66% | 1 | 3 | 1 | 9 | 0 | 1 |
| translateDeclaratorSuffix(CommonTree, TypeNode, SimpleScope) | | 70% | | 50% | 1 | 2 | 1 | 4 | 0 | 1 |
| translateLambda(Source, CommonTree, SimpleScope) | | 91% | | 50% | 1 | 2 | 0 | 9 | 0 | 1 |
| translateWriteEvent(Source, CommonTree, SimpleScope) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| translateArraySuffix(CommonTree, TypeNode, SimpleScope) | | 97% | | 50% | 1 | 2 | 1 | 9 | 0 | 1 |
| translateMPIAbsentExpressionNode(CommonTree, Source, SimpleScope) | | 100% | | n/a | 0 | 1 | 0 | 12 | 0 | 1 |
| translateCall(Source, CommonTree, SimpleScope) | | 100% | | 100% | 0 | 2 | 0 | 10 | 0 | 1 |
| translateACSLAssertion(CommonTree, SimpleScope) | | 100% | | n/a | 0 | 1 | 0 | 7 | 0 | 1 |
| translateBinder(CommonTree, SimpleScope) | | 100% | | 100% | 0 | 2 | 0 | 9 | 0 | 1 |
| translateDotOrArrow(Source, CommonTree, SimpleScope) | | 100% | | 100% | 0 | 2 | 0 | 8 | 0 | 1 |
| translateBehaviorBody(CommonTree, SimpleScope) | | 100% | | 100% | 0 | 2 | 0 | 7 | 0 | 1 |
| translateDependsEventList(CommonTree, SimpleScope) | | 100% | | 100% | 0 | 2 | 0 | 7 | 0 | 1 |
| translateArgumentList(CommonTree, SimpleScope) | | 100% | | 100% | 0 | 2 | 0 | 6 | 0 | 1 |
| AcslContractWorker(NodeFactory, TokenFactory, CParseTree, Configuration) | | 100% | | n/a | 0 | 1 | 0 | 11 | 0 | 1 |
| translatePointers(CommonTree, TypeNode, SimpleScope) | | 100% | | 100% | 0 | 2 | 0 | 7 | 0 | 1 |
| translateOperatorEvent(CommonTree, CompositeEventNode.EventOperator, SimpleScope) | | 100% | | n/a | 0 | 1 | 0 | 6 | 0 | 1 |
| translateBinders(CommonTree, Source, SimpleScope) | | 100% | | 100% | 0 | 2 | 0 | 6 | 0 | 1 |
| translateLogicFunctionClause(CommonTree, SimpleScope) | | 100% | | n/a | 0 | 1 | 0 | 9 | 0 | 1 |
| translateRemoteExpression(CommonTree, Source, SimpleScope) | | 100% | | n/a | 0 | 1 | 0 | 6 | 0 | 1 |
| translateBehavior(CommonTree, SimpleScope) | | 100% | | n/a | 0 | 1 | 0 | 5 | 0 | 1 |
| translateReadsOrAssigns(CommonTree, SimpleScope, boolean) | | 100% | | 100% | 0 | 2 | 0 | 6 | 0 | 1 |
| translateDepends(CommonTree, SimpleScope) | | 100% | | n/a | 0 | 1 | 0 | 5 | 0 | 1 |
| translateAssumes(CommonTree, SimpleScope) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| translateRequires(CommonTree, SimpleScope) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| translateEnsures(CommonTree, SimpleScope) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| translateValidNode(CommonTree, Source, SimpleScope) | | 100% | | n/a | 0 | 1 | 0 | 3 | 0 | 1 |
| translateGuards(CommonTree, SimpleScope) | | 100% | | n/a | 0 | 1 | 0 | 3 | 0 | 1 |
| translateEnumerationConstant(IdentifierNode, SimpleScope) | | 100% | | 100% | 0 | 2 | 0 | 4 | 0 | 1 |
| translateIntegerConstant(Source, CommonTree) | | 100% | | n/a | 0 | 1 | 0 | 2 | 0 | 1 |
| newSource(CommonTree) | | 100% | | n/a | 0 | 1 | 0 | 2 | 0 | 1 |
| translateTrue(Source) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| static {...} | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |