| conditionalExpressionToIf(ConditionalExpression, Statement) |  | 0% | | 0% | 3 | 3 | 41 | 41 | 1 | 1 |
| setImpactScopeOfLocation(Location) |  | 4% | | 4% | 25 | 26 | 43 | 45 | 0 | 1 |
| atomicFragment(boolean, Fragment, Location, Location) | | 0% | | 0% | 5 | 5 | 20 | 20 | 1 | 1 |
| conditionalExpressionToIf(Expression, VariableExpression, ConditionalExpression) | | 0% | | 0% | 3 | 3 | 20 | 20 | 1 | 1 |
| refineConditionalExpressionOfStatement(Statement, Location) | | 0% | | 0% | 3 | 3 | 15 | 15 | 1 | 1 |
| tempVariable(CommonModelFactory.TempVariableKind, Scope, CIVLSource, CIVLType) | | 0% | | 0% | 2 | 2 | 11 | 11 | 1 | 1 |
| booleanExpression(Expression) | | 16% | | 12% | 4 | 5 | 9 | 12 | 0 | 1 |
| processValue(int) | | 15% | | 25% | 4 | 5 | 8 | 11 | 0 | 1 |
| refineConditionalExpression(Scope, Expression, ExpressionNode) | | 26% | | 33% | 3 | 4 | 8 | 12 | 0 | 1 |
| callOrSpawnStatement(CIVLSource, Location, boolean, Expression, List, Expression) | | 0% | | 0% | 3 | 3 | 10 | 10 | 1 | 1 |
| conditionalExpression(CIVLSource, Expression, Expression, Expression) | | 0% | | 0% | 3 | 3 | 5 | 5 | 1 | 1 |
| assertStatement(CIVLSource, Location, Expression, ArrayList) | | 0% | | 0% | 2 | 2 | 8 | 8 | 1 | 1 |
| chooseStatement(CIVLSource, Location, LHSExpression, Expression) | | 0% | | 0% | 2 | 2 | 6 | 6 | 1 | 1 |
| newAnonymousVariableForArrayLiteral(CIVLSource, Scope, CIVLArrayType) | | 0% | | n/a | 1 | 1 | 5 | 5 | 1 | 1 |
| binaryExpression(CIVLSource, BinaryExpression.BINARY_OPERATOR, Expression, Expression) | | 66% | | 40% | 8 | 11 | 4 | 17 | 0 | 1 |
| dotExpression(CIVLSource, Expression, int) | | 0% | | 0% | 3 | 3 | 6 | 6 | 1 | 1 |
| joinFragment(CIVLSource, Location, Expression) | | 0% | | n/a | 1 | 1 | 5 | 5 | 1 | 1 |
| joinScope(Expression[]) | | 0% | | 0% | 2 | 2 | 4 | 4 | 1 | 1 |
| quantifiedExpression(CIVLSource, QuantifiedExpression.Quantifier, Identifier, CIVLType, Expression, Expression) | | 0% | | n/a | 1 | 1 | 4 | 4 | 1 | 1 |
| ifElseBranchStatement(CIVLSource, Location, Expression, boolean) | | 0% | | 0% | 2 | 2 | 6 | 6 | 1 | 1 |
| switchBranchStatement(CIVLSource, Location, Expression, Expression) | | 0% | | 0% | 2 | 2 | 6 | 6 | 1 | 1 |
| noopStatement(CIVLSource, Location, Expression) | | 0% | | 0% | 2 | 2 | 6 | 6 | 1 | 1 |
| assignAtomicLockVariable(Integer, Location) | | 0% | | n/a | 1 | 1 | 3 | 3 | 1 | 1 |
| unaryExpression(CIVLSource, UnaryExpression.UNARY_OPERATOR, Expression) | | 70% | | 60% | 2 | 4 | 2 | 13 | 0 | 1 |
| subscriptExpression(CIVLSource, LHSExpression, Expression) | | 58% | | 25% | 2 | 3 | 3 | 9 | 0 | 1 |
| arrayLiteralExpression(CIVLSource, CIVLType, ArrayList) | | 0% | | 0% | 3 | 3 | 7 | 7 | 1 | 1 |
| structOrUnionLiteralExpression(CIVLSource, CIVLType, ArrayList) | | 0% | | 0% | 3 | 3 | 7 | 7 | 1 | 1 |
| switchBranchStatement(CIVLSource, Location, Expression) | | 0% | | 0% | 2 | 2 | 5 | 5 | 1 | 1 |
| isProcessDefined(CIVLSource, SymbolicExpression) | | 0% | | 0% | 2 | 2 | 4 | 4 | 1 | 1 |
| isScopeDefined(CIVLSource, SymbolicExpression) | | 0% | | 0% | 2 | 2 | 4 | 4 | 1 | 1 |
| sizeofExpressionExpression(CIVLSource, Expression) | | 0% | | n/a | 1 | 1 | 4 | 4 | 1 | 1 |
| noopStatement(CIVLSource, Location) | | 0% | | n/a | 1 | 1 | 3 | 3 | 1 | 1 |
| extractInt(CIVLSource, NumericExpression) | | 46% | | 50% | 1 | 2 | 1 | 4 | 0 | 1 |
| nullPointerExpression(CIVLPointerType, CIVLSource) | | 0% | | n/a | 1 | 1 | 3 | 3 | 1 | 1 |
| scopeofExpression(CIVLSource, LHSExpression) | | 0% | | n/a | 1 | 1 | 3 | 3 | 1 | 1 |
| booleanLiteralExpression(CIVLSource, boolean) | | 0% | | n/a | 1 | 1 | 3 | 3 | 1 | 1 |
| dynamicTypeOfExpression(CIVLSource, CIVLType) | | 0% | | n/a | 1 | 1 | 3 | 3 | 1 | 1 |
| selfExpression(CIVLSource) | | 0% | | n/a | 1 | 1 | 3 | 3 | 1 | 1 |
| procnullExpression(CIVLSource) | | 0% | | n/a | 1 | 1 | 3 | 3 | 1 | 1 |
| sizeofTopConditionalExpressionQueue() | | 0% | | 0% | 2 | 2 | 3 | 3 | 1 | 1 |
| functionGuardExpression(CIVLSource, Expression, List) | | 0% | | n/a | 1 | 1 | 2 | 2 | 1 | 1 |
| systemGuardExpression(CallOrSpawnStatement) | | 71% | | 50% | 1 | 2 | 1 | 4 | 0 | 1 |
| enumType(String, Map) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| gotoBranchStatement(CIVLSource, Location, String) | | 0% | | n/a | 1 | 1 | 2 | 2 | 1 | 1 |
| sourceOfSpan(CIVLSource, CIVLSource) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| addConditionalExpression(ConditionalExpression) | | 0% | | n/a | 1 | 1 | 2 | 2 | 1 | 1 |
| charLiteralExpression(CIVLSource, char) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| pollConditionaExpression() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| function(CIVLSource, Identifier, List, CIVLType, Scope, Location) | | 81% | | 75% | 1 | 3 | 1 | 5 | 0 | 1 |
| functionType(CIVLType, CIVLType[]) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| resetAnonFragment() | | 0% | | n/a | 1 | 1 | 2 | 2 | 1 | 1 |
| sizeofTypeExpression(CIVLSource, CIVLType) | | 80% | | 50% | 1 | 2 | 1 | 7 | 0 | 1 |
| resultExpression(CIVLSource) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| addAnonStatement(Statement) | | 0% | | n/a | 1 | 1 | 2 | 2 | 1 | 1 |
| returnFragment(CIVLSource, Location, Expression, CIVLFunction) | | 84% | | 50% | 1 | 2 | 1 | 5 | 0 | 1 |
| scopeValue(int) | | 95% | | 88% | 1 | 5 | 1 | 11 | 0 | 1 |
| callOrSpawnStatement(CIVLSource, Location, boolean, List, Expression) | | 93% | | 75% | 1 | 3 | 1 | 10 | 0 | 1 |
| mallocStatement(CIVLSource, Location, LHSExpression, CIVLType, Expression, Expression, int, Expression) | | 92% | | 50% | 1 | 2 | 1 | 7 | 0 | 1 |
| dynamicType() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| stringType() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| processSymbolicType() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| scopeSymbolicType() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| stringSymbolicType() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| atomicLockVariableExpression() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| undefinedProcessValue() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| nullProcessValue() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| undefinedScopeValue() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| nullScopeValue() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| currentScope() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| bundleType() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| getHeapFieldId(CIVLType) | | 86% | | 50% | 1 | 2 | 1 | 3 | 0 | 1 |
| hasConditionalExpressions() | | 80% | | 50% | 1 | 2 | 1 | 3 | 0 | 1 |
| static {...} | | 75% | | 50% | 1 | 2 | 0 | 1 | 0 | 1 |
| isTrue(Expression) | | 91% | | 50% | 2 | 3 | 0 | 1 | 0 | 1 |
| CommonModelFactory(SymbolicUniverse) | | 100% | | 100% | 0 | 2 | 0 | 46 | 0 | 1 |
| primitiveType(CIVLPrimitiveType.PrimitiveTypeKind, SymbolicType) | | 100% | | 100% | 0 | 4 | 0 | 12 | 0 | 1 |
| completeBundleType(CIVLBundleType, List, Collection) | | 100% | | 100% | 0 | 2 | 0 | 9 | 0 | 1 |
| scope(CIVLSource, Scope, Set, CIVLFunction) | | 100% | | 100% | 0 | 3 | 0 | 10 | 0 | 1 |
| computeInitialHeapValue(SymbolicTupleType) | | 100% | | 100% | 0 | 2 | 0 | 10 | 0 | 1 |
| computeDynamicHeapType(Iterable) | | 100% | | 100% | 0 | 2 | 0 | 8 | 0 | 1 |
| join(Scope, Scope) | | 100% | | 100% | 0 | 5 | 0 | 14 | 0 | 1 |
| derivativeCallExpression(CIVLSource, AbstractFunction, List, List) | | 100% | | 100% | 0 | 2 | 0 | 8 | 0 | 1 |
| completeHeapType(CIVLHeapType, Collection) | | 100% | | n/a | 0 | 1 | 0 | 8 | 0 | 1 |
| identifier(CIVLSource, String) | | 100% | | 100% | 0 | 2 | 0 | 6 | 0 | 1 |
| quantifiedExpression(CIVLSource, QuantifiedExpression.Quantifier, Identifier, CIVLType, Expression, Expression, Expression) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| assignStatement(CIVLSource, Location, LHSExpression, Expression, boolean) | | 100% | | n/a | 0 | 1 | 0 | 5 | 0 | 1 |
| sizeofExpression(CIVLPrimitiveType.PrimitiveTypeKind) | | 100% | | n/a | 0 | 1 | 0 | 3 | 0 | 1 |
| systemFunction(CIVLSource, Identifier, List, CIVLType, Scope, String) | | 100% | | 100% | 0 | 2 | 0 | 3 | 0 | 1 |
| loopBranchStatement(CIVLSource, Location, Expression, boolean) | | 100% | | 50% | 1 | 2 | 0 | 6 | 0 | 1 |
| createAtomicLockVariable(Scope) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| abstractFunctionCallExpression(CIVLSource, AbstractFunction, List) | | 100% | | n/a | 0 | 1 | 0 | 6 | 0 | 1 |
| assumeFragment(CIVLSource, Location, Expression) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| dereferenceExpression(CIVLSource, Expression) | | 100% | | n/a | 0 | 1 | 0 | 5 | 0 | 1 |
| joinScope(List) | | 100% | | 100% | 0 | 2 | 0 | 5 | 0 | 1 |
| variableExpression(CIVLSource, Variable) | | 100% | | 50% | 1 | 2 | 0 | 5 | 0 | 1 |
| addressOfExpression(CIVLSource, LHSExpression) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| assertStatement(CIVLSource, Location, Expression) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| castExpression(CIVLSource, CIVLType, Expression) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| undefinedValue(SymbolicType) | | 100% | | n/a | 0 | 1 | 0 | 3 | 0 | 1 |
| integerLiteralExpression(CIVLSource, BigInteger) | | 100% | | n/a | 0 | 1 | 0 | 3 | 0 | 1 |
| realLiteralExpression(CIVLSource, BigDecimal) | | 100% | | n/a | 0 | 1 | 0 | 3 | 0 | 1 |
| location(CIVLSource, Scope) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| hereOrRootExpression(CIVLSource, boolean) | | 100% | | n/a | 0 | 1 | 0 | 3 | 0 | 1 |
| initialValueExpression(CIVLSource, Variable) | | 100% | | n/a | 0 | 1 | 0 | 3 | 0 | 1 |
| extractIntField(CIVLSource, SymbolicExpression, IntObject) | | 100% | | n/a | 0 | 1 | 0 | 2 | 0 | 1 |
| boundVariableExpression(CIVLSource, Identifier, CIVLType) | | 100% | | n/a | 0 | 1 | 0 | 3 | 0 | 1 |
| abstractFunction(CIVLSource, Identifier, List, CIVLType, Scope, int) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| functionPointerExpression(CIVLSource, CIVLFunction) | | 100% | | n/a | 0 | 1 | 0 | 2 | 0 | 1 |
| addHeapFieldType(CIVLType, int) | | 100% | | n/a | 0 | 1 | 0 | 2 | 0 | 1 |
| sourceOfSpan(Source, Source) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| addConditionalExpressionQueue() | | 100% | | n/a | 0 | 1 | 0 | 2 | 0 | 1 |
| variable(CIVLSource, CIVLType, Identifier, int) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| pointerType(CIVLType) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| sourceOfSpan(ASTNode, ASTNode) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| sourceOfToken(CToken) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| model(CIVLSource, CIVLFunction) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| getProcessId(CIVLSource, SymbolicExpression) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| getScopeId(CIVLSource, SymbolicExpression) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| completeArrayType(CIVLType, Expression) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| structOrUnionType(Identifier, boolean) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| systemFunctionCallExpression(CallOrSpawnStatement) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| sourceOfBeginning(ASTNode) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| sourceOfEnd(ASTNode) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| structField(Identifier, CIVLType) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| heapType(String) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| incompleteArrayType(CIVLType) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| sourceOf(ASTNode) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| sourceOf(Source) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| popConditionaExpressionStack() | | 100% | | n/a | 0 | 1 | 0 | 2 | 0 | 1 |
| newBundleType() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| setTokenFactory(TokenFactory) | | 100% | | n/a | 0 | 1 | 0 | 2 | 0 | 1 |
| setSystemScope(Scope) | | 100% | | n/a | 0 | 1 | 0 | 2 | 0 | 1 |
| setCurrentScope(Scope) | | 100% | | n/a | 0 | 1 | 0 | 2 | 0 | 1 |
| model() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| booleanType() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| charType() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| integerType() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| processType() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| realType() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| scopeType() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| voidType() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| dynamicSymbolicType() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| functionPointerSymbolicType() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| pointerSymbolicType() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| universe() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| systemSource() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| anonFragment() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| heapType() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| heapSymbolicType() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| bundleSymbolicType() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |