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; |
14 | |
15 | while (x < 1024) { |
16 | x++; |
17 | y++; |
18 | } |
19 | |
20 | __VERIFIER_assert(x == y); |
21 | } |
2018-05-19 18:21:41:909 INFO ResourceLimitChecker.fromConfiguration Using the following resource limits: CPU-time limit of 900s
2018-05-19 18:21:41:946 INFO CPAchecker.run CPAchecker 1.7-svn (Java HotSpot(TM) 64-Bit Server VM 1.8.0_171) started
2018-05-19 18:21:42:824 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 18:21:42:900 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 18:21:42:944 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 18:21:42:950 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 18:21:43:017 INFO PredicateCPA:PredicateCPARefiner.<init> Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy.
2018-05-19 18:21:43:028 INFO CPAchecker.runAlgorithm Starting analysis ...
2018-05-19 18:21:43:154 INFO CPAchecker.runAlgorithm Stopping analysis ...
PredicateCPA statistics
-----------------------
Number of abstractions: 7 (13% of all post computations)
Times abstraction was reused: 0
Because of function entry/exit: 0 (0%)
Because of loop head: 4 (57%)
Because of join nodes: 0 (0%)
Because of threshold: 0 (0%)
Because of target state: 3 (43%)
Times precision was empty: 3 (43%)
Times precision was {false}: 0 (0%)
Times result was cached: 0 (0%)
Times cartesian abs was used: 0 (0%)
Times boolean abs was used: 4 (57%)
Times result was 'false': 1 (14%)
Number of strengthen sat checks: 0
Number of coverage checks: 1
BDD entailment checks: 1
Number of SMT sat checks: 0
trivial: 0
cached: 0
Max ABE block size: 3
Number of predicates discovered: 3
Number of abstraction locations: 2
Max number of predicates per location: 2
Avg number of predicates per location: 1
Total predicates per abstraction: 5
Max number of predicates per abstraction: 2
Avg number of predicates per abstraction: 1.25
Number of irrelevant predicates: 1 (20%)
Number of preds handled by boolean abs: 4 (80%)
Total number of models for allsat: 3
Max number of models for allsat: 1
Avg number of models for allsat: 0.75
Time for post operator: 0.029s
Time for path formula creation: 0.029s
Time for strengthen operator: 0.001s
Time for prec operator: 0.022s
Time for abstraction: 0.020s (Max: 0.012s, Count: 7)
Boolean abstraction: 0.008s
Solving time: 0.003s (Max: 0.002s)
Model enumeration time: 0.000s
Time for BDD construction: 0.004s (Max: 0.004s)
Time for merge operator: 0.000s
Time for coverage check: 0.000s
Time for BDD entailment checks: 0.000s
Total time for SMT solver (w/o itp): 0.003s
Number of path formula cache hits: 30 (51%)
Inside post operator:
Inside path formula creation:
Time for path formula computation: 0.030s
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: 44, 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.006s
Automaton transfers with branching: 0
Automaton transfer successors: 1.00 (sum: 55, count: 55, min: 1, max: 1) [1 x 55]
CPA algorithm statistics
------------------------
Number of iterations: 31
Max size of waitlist: 3
Average size of waitlist: 1
ReversePostorderSortedWaitlist: 0.00 (sum: 0, count: 64, min: 0, max: 0)
CallstackSortedWaitlist: 6.67 (sum: 20, count: 3, min: 3, max: 11)
Number of computed successors: 36
Max successors for one state: 2
Number of times merged: 0
Number of times stopped: 1
Number of times breaked: 2
Total time for CPA algorithm: 0.076s (Max: 0.040s)
Time for choose from waitlist: 0.000s
Time for precision adjustment: 0.025s
Time for transfer relation: 0.046s
Time for merge operator: 0.000s
Time for stop operator: 0.001s
Time for adding to reached set: 0.004s
Static Predicate Refiner statistics
-----------------------------------
Number of predicates found statically: 1 (count: 1, min: 1, max: 1, avg: 1.00)
Total time for static refinement: 0.030s
Time for path feasibility check: 0.004s
Time for predicate extraction from CFA: 0.009s
Time for ARG update: 0.011s
PredicateCPARefiner statistics
------------------------------
Number of predicate refinements: 1
Avg. length of target path (in blocks): 2.00 (sum: 2, count: 1, min: 2, max: 2)
Number of infeasible sliced prefixes: 0 (count: 0, min: 0, max: 0, avg: 0.00)
Time for refinement: 0.012s
Counterexample analysis: 0.011s (Max: 0.007s, Calls: 2)
Refinement sat check: 0.003s
Interpolant computation: 0.000s
Path-formulas extraction: 0.000s
Error path post-processing: 0.000s
Predicate-Abstraction Refiner statistics
----------------------------------------
Predicate creation: 0.002s
Precision update: 0.001s
ARG update: 0.001s
Length of refined path (in blocks): 2.00 (sum: 2, count: 1, min: 2, max: 2)
Number of affected states: 1 (count: 1, min: 1, max: 1, avg: 1.00)
Length (states) of path with itp 'true': 0 (count: 1, min: 0, max: 0, avg: 0.00)
Length (states) of path with itp non-trivial itp: 1 (count: 1, min: 1, max: 1, avg: 1.00)
Length (states) of path with itp 'false': 0 (count: 1, min: 0, max: 0, avg: 0.00)
Different non-trivial interpolants along paths: 0 (count: 1, min: 0, max: 0, avg: 0.00)
Equal non-trivial interpolants along paths: 0 (count: 1, min: 0, max: 0, avg: 0.00)
Number of refs with location-based cutoff: 0
CEGAR algorithm statistics
--------------------------
Number of refinements: 2
Number of successful refinements: 2
Number of failed refinements: 0
Max. size of reached set before ref.: 12
Max. size of reached set after ref.: 3
Avg. size of reached set before ref.: 12.00
Avg. size of reached set after ref.: 2.00
Total time for CEGAR algorithm: 0.125s
Time for refinements: 0.049s
Average time for refinement: 0.024s
Max time for refinement: 0.037s
Code Coverage
-----------------------------
Function coverage: 1.000
Visited lines: 9
Total lines: 9
Line coverage: 1.000
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: 15
Number of reached locations: 15 (54%)
Avg states per location: 1
Max states per location: 1 (at node N0)
Number of reached functions: 2 (100%)
Number of partitions: 15
Avg size of partitions: 1
Max size of partitions: 1
Number of target states: 0
Time for analysis setup: 1.073s
Time for loading CPAs: 0.358s
Time for loading parser: 0.225s
Time for CFA construction: 0.408s
Time for parsing file(s): 0.231s
Time for AST to CFA: 0.074s
Time for CFA sanity check: 0.006s
Time for post-processing: 0.066s
Time for CFA export: 0.525s
Time for function pointers resolving: 0.002s
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.034s
Time for collecting variables: 0.012s
Time for solving dependencies: 0.000s
Time for building hierarchy: 0.000s
Time for building classification: 0.021s
Time for exporting data: 0.001s
Time for Analysis: 0.125s
CPU time for analysis: 0.470s
Time for analyzing result: 0.001s
Total time for CPAchecker: 1.199s
Total CPU time for CPAchecker: 3.550s
Time for statistics: 0.182s
Time for Garbage Collector: 0.045s (in 3 runs)
Garbage Collector(s) used: PS MarkSweep, PS Scavenge
Used heap memory: 64MB ( 61 MiB) max; 39MB ( 37 MiB) avg; 93MB ( 89 MiB) peak
Used non-heap memory: 35MB ( 33 MiB) max; 24MB ( 23 MiB) avg; 40MB ( 38 MiB) peak
Used in PS Old Gen pool: 17MB ( 16 MiB) max; 5MB ( 5 MiB) avg; 17MB ( 16 MiB) peak
Allocated heap memory: 251MB ( 240 MiB) max; 237MB ( 226 MiB) avg
Allocated non-heap memory: 36MB ( 34 MiB) max; 25MB ( 23 MiB) avg
Total process virtual memory: 4119MB ( 3928 MiB) max; 3950MB ( 3767 MiB) avg
analysis.algorithm.CEGAR = true
analysis.entryFunction = main
analysis.programNames = multivar_true-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.compressWitness = false
cpa.arg.proofWitness = proofWitness.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