scripts/cpa.sh -svcomp23 -heap 20000M -benchmark -timelimit '7200 s' -stats -spec /mnt/goblint-svcomp/goblint-bench/bench/concrat/properties/no-data-race.prp -64 /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c


--------------------------------------------------------------------------------


Running CPAchecker with Java heap of size 20000M.
Running CPAchecker with default stack size (1024k). Specify a larger value with -stack if needed.
Language C detected and set for analysis (CPAMain.detectFrontendLanguageIfNecessary, INFO)

Using the following resource limits: CPU-time limit of 7200s (ResourceLimitChecker.fromConfiguration, INFO)

CPAchecker 2.2 (OpenJDK 64-Bit Server VM 17.0.8.1) started (CPAchecker.run, INFO)

Parsing CFA from file(s) "/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c" (CPAchecker.parse, INFO)

line 1193: Dead code detected: return (-11); (CFACreationUtils.addEdgeToCFA, INFO)

line 3753: Dead code detected: rp = rp->ai_next; (CFACreationUtils.addEdgeToCFA, INFO)

line 4293: Dead code detected: break; (CFACreationUtils.addEdgeToCFA, INFO)

line 4297: Dead code detected: break; (CFACreationUtils.addEdgeToCFA, INFO)

line 4301: Dead code detected: break; (CFACreationUtils.addEdgeToCFA, INFO)

line 4305: Dead code detected: break; (CFACreationUtils.addEdgeToCFA, INFO)

line 4309: Dead code detected: break; (CFACreationUtils.addEdgeToCFA, INFO)

line 4313: Dead code detected: break; (CFACreationUtils.addEdgeToCFA, INFO)

line 4317: Dead code detected: break; (CFACreationUtils.addEdgeToCFA, INFO)

line 4427: Dead code detected: close(fd___0); (CFACreationUtils.addEdgeToCFA, INFO)

line 2564: Function pointer *(ops->alloc_sock) with type struct sock *(*)(int protocol) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

program contains concurrency, cloning functions... (CFACreator.postProcessingOnMutableCFAs, INFO)

Using predicate analysis with MathSAT5 version 5.6.8 (27814677e16f) (Jun 28 2022 17:03:19, gmp 6.1.2, gcc 6.3.0, 64-bit, reentrant) and JFactory 1.21. (PredicateCPA:PredicateCPA.<init>, INFO)

Starting analysis ... (CPAchecker.runAlgorithm, INFO)

Assuming external function getopt to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO)

Assuming external function sigemptyset to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO)

Assuming external function sigaddset to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO)

Assuming external function pthread_sigmask to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO)

Assuming external function open to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO)

Assuming external function perror to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO)

Error: line 1445: Unsupported feature (memset): memset((void *)(&ifr), 0, 40UL) (line was originally memset((void *)(& ifr), 0, sizeof(ifr));) (ExpressionToFormulaVisitor.visit, SEVERE)


PredicateCPA statistics
-----------------------
Number of abstractions:            20 (4% of all post computations)
  Times abstraction was reused:    0
  Because of function entry/exit:  17 (85%)
  Because of loop head:            3 (15%)
  Because of join nodes:           0 (0%)
  Because of threshold:            0 (0%)
  Because of target state:         0 (0%)
  Times precision was empty:       20 (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:         20
  BDD entailment checks:           20
Number of SMT sat checks:          0
  trivial:                         0
  cached:                          0

Max ABE block size:                       37
Avg ABE block size:                                3.90 (sum: 78, count: 20, min: 0, max: 37)
Number of predicates discovered:          0

Time for post operator:                                0.147s
  Time for path formula creation:                      0.142s
Time for strengthen operator:                          0.003s
Time for prec operator:                                0.006s
  Time for abstraction:                  0.000s (Max:     0.000s, Count: 20)
    Solving time:                        0.000s (Max:     0.000s)
    Model enumeration time:              0.000s
    Time for BDD construction:           0.000s (Max:     0.000s)
Time for coverage checks:                              0.006s
  Time for BDD entailment checks:                      0.006s
Total time for SMT solver (w/o itp):     0.000s

Number of path formula cache hits:   4 (1%)

Inside post operator:                  
  Inside path formula creation:        
    Time for path formula computation:     0.129s

Total number of created targets for pointer analysis: 0


Number of BDD nodes:                               202
Size of BDD node table:                            1048583
Size of BDD cache:                                 104869
Size of BDD node cleanup queue:                    0.00 (sum: 0, count: 41, min: 0, max: 0)
Time for BDD node cleanup:                             0.000s
Time for BDD garbage collection:                       0.000s (in 0 runs)

KeyValue statistics
-------------------
Init. function predicates:                         0
Init. global predicates:                           0
Init. location predicates:                         0

Invariant Generation statistics
-------------------------------

ValueAnalysisCPA statistics
---------------------------
Number of variables per state:                     5.72 (sum: 3262, count: 570, min: 0, max: 13)
Number of global variables per state:              5.68 (sum: 3240, count: 570, min: 0, max: 12)
Number of assumptions:                                   14
Number of deterministic assumptions:                      0
Level of Determinism:                              0%

ValueAnalysisPrecisionAdjustment statistics
-------------------------------------------
Number of abstraction computations:                     570
Total time for liveness abstraction:                   0.000s
Total time for abstraction computation:                0.003s
Total time for path thresholds:                        0.000s

ConstraintsStrengthenOperator statistics
----------------------------------------
Total time for strengthening by ConstraintsCPA:     0.000s
Replaced symbolic expressions: 0

AutomatonAnalysis (DataRace) statistics
---------------------------------------
Number of states:                                  1
Total time for successor computation:                  0.003s
Total time for strengthen operator:                    0.078s
Automaton transfers with branching:                0
Automaton transfer successors:                     1.00 (sum: 570, count: 570, min: 1, max: 1) [1 x 570]
Number of states with assumption transitions:      0

AutomatonAnalysis (svcompTerminatingFunctions) statistics
---------------------------------------------------------
Number of states:                                  1
Total time for successor computation:                  0.003s
Automaton transfers with branching:                0
Automaton transfer successors:                     1.00 (sum: 570, count: 570, min: 1, max: 1) [1 x 570]
Number of states with assumption transitions:      0

CPA algorithm statistics
------------------------
Number of iterations:            568
Max size of waitlist:            5
Average size of waitlist:        1
Number of computed successors:   570
Max successors for one state:    2
Number of times merged:          0
Number of times stopped:         1
Number of times breaked:         0

Total time for CPA algorithm:         0.363s (Max:     0.363s)
  Time for choose from waitlist:      0.000s
  Time for precision adjustment:      0.021s
  Time for transfer relation:         0.320s
  Time for merge operator:            0.006s
  Time for stop operator:             0.005s
  Time for adding to reached set:     0.004s

CPAchecker general statistics
-----------------------------
Number of program locations:                       24976
Number of CFA edges (per node):                       29026 (count: 24976, min: 0, max: 23, avg: 1.16)
Number of relevant variables:                      6170
Number of functions:                               1303
Number of loops (and loop nodes):                       228 (sum: 3000, min: 3, max: 36, avg: 13.16)
Size of reached set:             570
  Number of partitions:          562
    Avg size of partitions:      1
    Max size of partitions:      2 (with key [{main=N1537 (before line 2530) Function parse_opts called from node N1558, stack depth 3 [68544dba], stack [main, parse_cli, parse_opts] @@ 0}])
  Number of target states:       0
  Size of final wait list:       3

Time for analysis setup:          2.526s
  Time for loading CPAs:          0.463s
  Time for loading parser:        0.126s
  Time for CFA construction:      1.901s
    Time for parsing file(s):     0.303s
    Time for AST to CFA:          0.446s
    Time for CFA sanity check:    0.000s
    Time for post-processing:     1.083s
      Time for function pointers resolving:            0.012s
        Function calls via function pointers:            20 (count: 1, min: 20, max: 20, avg: 20.00)
        Instrumented function pointer calls:             19 (count: 1, min: 19, max: 19, avg: 19.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 classifying variables:                  0.567s
        Time for collecting variables:                 0.355s
        Time for solving dependencies:                 0.018s
        Time for building hierarchy:                   0.006s
        Time for building classification:              0.185s
        Time for exporting data:                       0.000s
Time for Analysis:                0.363s
CPU time for analysis:            1.470s
Total time for CPAchecker:        2.890s
Total CPU time for CPAchecker:   11.980s
Time for statistics:              0.047s

Time for Garbage Collector:       0.105s (in 8 runs)
Garbage Collector(s) used:    G1 Old Generation, G1 Young Generation

Verification result: UNKNOWN, incomplete analysis.
More details about the verification run can be found in the directory "./output".
