Matches in value-assignements (V): {{numOfValueMatches}}
Matches in edge-description: {{numOfDescriptionMatches}}
-V- |
{{line.desc}}
|
1 | extern void __VERIFIER_error() __attribute__ ((__noreturn__)); |
2 | extern unsigned int __VERIFIER_nondet_uint(void); |
3 | |
4 | void __VERIFIER_assert(int cond) { |
5 | if (!(cond)) { |
6 | ERROR: __VERIFIER_error(); |
7 | } |
8 | return; |
9 | } |
10 | |
11 | int main(void) { |
12 | unsigned int x = __VERIFIER_nondet_uint(); |
13 | unsigned int y = x + 1; |
14 | |
15 | while (x < 1024) { |
16 | x++; |
17 | y++; |
18 | } |
19 | |
20 | __VERIFIER_assert(x == y); |
21 | } |
2018-05-19 17:32:54:104 INFO ResourceLimitChecker.fromConfiguration Using the following resource limits: CPU-time limit of 900s
2018-05-19 17:32:54:146 INFO CPAchecker.run CPAchecker 1.7-svn (Java HotSpot(TM) 64-Bit Server VM 1.8.0_171) started
2018-05-19 17:32:55:038 WARNING PredicateCPA:JavaSMT:Mathsat5SolverContext.<init> MathSAT5 is available for research and evaluation purposes only. It can not be used in a commercial environment, particularly as part of a commercial product, without written permission. MathSAT5 is provided as is, without any warranty. Please write to mathsat@fbk.eu for additional questions regarding licensing MathSAT5 or obtaining more up-to-date versions.
2018-05-19 17:32:55:106 INFO PredicateCPA:PredicateCPA.<init> Using predicate analysis with MathSAT5 version 5.5.0 (59014c8d54e1) (Dec 5 2017 11:43:02, gmp 6.1.0, gcc 4.8.5, 64-bit, reentrant) and JFactory 1.21.
2018-05-19 17:32:55:161 WARNING ARGCPA:JavaSMT:Mathsat5SolverContext.<init> MathSAT5 is available for research and evaluation purposes only. It can not be used in a commercial environment, particularly as part of a commercial product, without written permission. MathSAT5 is provided as is, without any warranty. Please write to mathsat@fbk.eu for additional questions regarding licensing MathSAT5 or obtaining more up-to-date versions.
2018-05-19 17:32:55:166 WARNING ARGCPA:JavaSMT:Mathsat5SolverContext.<init> MathSAT5 is available for research and evaluation purposes only. It can not be used in a commercial environment, particularly as part of a commercial product, without written permission. MathSAT5 is provided as is, without any warranty. Please write to mathsat@fbk.eu for additional questions regarding licensing MathSAT5 or obtaining more up-to-date versions.
2018-05-19 17:32:55:248 INFO PredicateCPA:PredicateCPARefiner.<init> Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy.
2018-05-19 17:32:55:258 INFO CPAchecker.runAlgorithm Starting analysis ...
2018-05-19 17:32:55:378 INFO CPAchecker.runAlgorithm Stopping analysis ...
PredicateCPA statistics
-----------------------
Number of abstractions: 2 (11% of all post computations)
Times abstraction was reused: 0
Because of function entry/exit: 0 (0%)
Because of loop head: 1 (50%)
Because of join nodes: 0 (0%)
Because of threshold: 0 (0%)
Because of target state: 1 (50%)
Times precision was empty: 2 (100%)
Times precision was {false}: 0 (0%)
Times result was cached: 0 (0%)
Times cartesian abs was used: 0 (0%)
Times boolean abs was used: 0 (0%)
Times result was 'false': 0 (0%)
Number of strengthen sat checks: 0
Number of coverage checks: 0
BDD entailment checks: 0
Number of SMT sat checks: 0
trivial: 0
cached: 0
Max ABE block size: 3
Number of predicates discovered: 0
Time for post operator: 0.060s
Time for path formula creation: 0.060s
Time for strengthen operator: 0.000s
Time for prec operator: 0.004s
Time for abstraction: 0.001s (Max: 0.001s, Count: 2)
Solving time: 0.000s (Max: 0.000s)
Model enumeration time: 0.000s
Time for BDD construction: 0.000s (Max: 0.000s)
Time for merge operator: 0.000s
Time for coverage check: 0.000s
Total time for SMT solver (w/o itp): 0.000s
Number of path formula cache hits: 10 (29%)
Inside post operator:
Inside path formula creation:
Time for path formula computation: 0.060s
Total number of created targets for pointer analysis: 0
Number of BDD nodes: 202
Size of BDD node table: 55949
Size of BDD cache: 5623
Size of BDD node cleanup queue: 0.00 (sum: 0, count: 13, min: 0, max: 0)
Time for BDD node cleanup: 0.000s
Time for BDD garbage collection: 0.000s (in 0 runs)
PrecisionBootstrap statistics
-----------------------------
Init. function predicates: 0
Init. global predicates: 0
Init. location predicates: 0
Invariant Generation statistics
-------------------------------
AutomatonAnalysis (SVCOMP) statistics
-------------------------------------
Number of states: 1
Total time for successor computation: 0.001s
Automaton transfers with branching: 0
Automaton transfer successors: 1.00 (sum: 18, count: 18, min: 1, max: 1) [1 x 18]
CPA algorithm statistics
------------------------
Number of iterations: 9
Max size of waitlist: 3
Average size of waitlist: 1
ReversePostorderSortedWaitlist: 0.00 (sum: 0, count: 6, min: 0, max: 0)
CallstackSortedWaitlist: 3.00 (sum: 3, count: 1, min: 3, max: 3)
Number of computed successors: 11
Max successors for one state: 2
Number of times merged: 0
Number of times stopped: 0
Number of times breaked: 1
Total time for CPA algorithm: 0.077s (Max: 0.077s)
Time for choose from waitlist: 0.002s
Time for precision adjustment: 0.006s
Time for transfer relation: 0.064s
Time for stop operator: 0.000s
Time for adding to reached set: 0.004s
Static Predicate Refiner statistics
-----------------------------------
Number of predicates found statically: 0 (count: 0, min: 0, max: 0, avg: 0.00)
Total time for static refinement: 0.034s
Time for path feasibility check: 0.007s
PredicateCPARefiner statistics
------------------------------
Number of predicate refinements: 0
Predicate-Abstraction Refiner statistics
----------------------------------------
Predicate creation: 0.000s
Precision update: 0.000s
ARG update: 0.000s
Length of refined path (in blocks): 0.00 (sum: 0, count: 0, min: 0, max: 0)
Number of affected states: 0 (count: 0, min: 0, max: 0, avg: 0.00)
Length (states) of path with itp 'true': 0 (count: 0, min: 0, max: 0, avg: 0.00)
Length (states) of path with itp non-trivial itp: 0 (count: 0, min: 0, max: 0, avg: 0.00)
Length (states) of path with itp 'false': 0 (count: 0, min: 0, max: 0, avg: 0.00)
Different non-trivial interpolants along paths: 0 (count: 0, min: 0, max: 0, avg: 0.00)
Equal non-trivial interpolants along paths: 0 (count: 0, min: 0, max: 0, avg: 0.00)
Number of refs with location-based cutoff: 0
CEGAR algorithm statistics
--------------------------
Number of refinements: 1
Number of successful refinements: 0
Number of failed refinements: 0
Max. size of reached set before ref.: 12
Max. size of reached set after ref.: 0
Avg. size of reached set before ref.: 12.00
Avg. size of reached set after ref.: NaN
Total time for CEGAR algorithm: 0.118s
Time for refinements: 0.041s
Average time for refinement: 0.041s
Max time for refinement: 0.041s
Code Coverage
-----------------------------
Function coverage: 1.000
Visited lines: 6
Total lines: 9
Line coverage: 0.667
Visited conditions: 4
Total conditions: 4
Condition coverage: 1.000
CPAchecker general statistics
-----------------------------
Number of program locations: 28
Number of CFA edges (per node): 29 (count: 28, min: 0, max: 2, avg: 1.04)
Number of relevant variables: 3
Number of functions: 2
Number of loops (and loop nodes): 1 (sum: 8, min: 8, max: 8, avg: 8.00)
Size of reached set: 12
Number of reached locations: 12 (43%)
Avg states per location: 1
Max states per location: 1 (at node N1)
Number of reached functions: 2 (100%)
Number of partitions: 12
Avg size of partitions: 1
Max size of partitions: 1
Number of target states: 1
Size of final wait list 3
Time for analysis setup: 1.102s
Time for loading CPAs: 0.364s
Time for loading parser: 0.221s
Time for CFA construction: 0.421s
Time for parsing file(s): 0.235s
Time for AST to CFA: 0.078s
Time for CFA sanity check: 0.006s
Time for post-processing: 0.070s
Time for CFA export: 0.503s
Time for function pointers resolving: 0.003s
Function calls via function pointers: 0 (count: 1, min: 0, max: 0, avg: 0.00)
Instrumented function pointer calls: 0 (count: 1, min: 0, max: 0, avg: 0.00)
Function calls with function pointer arguments: 0 (count: 1, min: 0, max: 0, avg: 0.00)
Instrumented function pointer arguments: 0 (count: 1, min: 0, max: 0, avg: 0.00)
Time for var class.: 0.036s
Time for collecting variables: 0.012s
Time for solving dependencies: 0.001s
Time for building hierarchy: 0.000s
Time for building classification: 0.022s
Time for exporting data: 0.001s
Time for Analysis: 0.118s
CPU time for analysis: 0.330s
Time for analyzing result: 0.000s
Total time for CPAchecker: 1.223s
Total CPU time for CPAchecker: 3.510s
Time for statistics: 0.181s
Time for Garbage Collector: 0.046s (in 3 runs)
Garbage Collector(s) used: PS MarkSweep, PS Scavenge
Used heap memory: 61MB ( 58 MiB) max; 41MB ( 39 MiB) avg; 93MB ( 89 MiB) peak
Used non-heap memory: 36MB ( 34 MiB) max; 25MB ( 23 MiB) avg; 40MB ( 38 MiB) peak
Used in PS Old Gen pool: 17MB ( 16 MiB) max; 6MB ( 6 MiB) avg; 17MB ( 16 MiB) peak
Allocated heap memory: 251MB ( 240 MiB) max; 235MB ( 224 MiB) avg
Allocated non-heap memory: 37MB ( 35 MiB) max; 26MB ( 24 MiB) avg
Total process virtual memory: 4122MB ( 3931 MiB) max; 3963MB ( 3779 MiB) avg
analysis.algorithm.CEGAR = true
analysis.entryFunction = main
analysis.programNames = multivar_false-unreach-call1_true-termination.c
analysis.traversal.order = bfs
analysis.traversal.useCallstack = true
analysis.traversal.useReversePostorder = true
ARGCPA.cpa = cpa.composite.CompositeCPA
cegar.refiner = cpa.predicate.PredicateRefiner
CompositeCPA.cpas = cpa.location.LocationCPA, cpa.callstack.CallstackCPA, cpa.functionpointer.FunctionPointerCPA, cpa.predicate.PredicateCPA
cpa = cpa.arg.ARGCPA
cpa.arg.proofWitness = witness.graphml
cpa.composite.aggregateBasicBlocks = true
cpa.predicate.blk.alwaysAtFunctions = false
cpa.predicate.blk.alwaysAtLoops = true
cpa.predicate.refinement.performInitialStaticRefinement = true
limits.time.cpu = 900s
log.level = INFO
specification = config/specification/sv-comp-reachability.spc