scripts/cpa.sh -svcomp24 -heap 10000M -benchmark -timelimit '900 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 10000M.
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 900s (ResourceLimitChecker.fromConfiguration, INFO)

CPAchecker 2.3 (OpenJDK 64-Bit Server VM 17.0.9) 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.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant) and JFactory 1.21. (PredicateCPA:PredicateCPA.<init>, INFO)

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

lines 795-798: Ignoring assignment to array type (char)[56] from other type unsigned int (PredicateCPA:AssignmentHandler.generatePartialAssignmentsForArrayType, WARNING)

lines 795-798: Ignoring assignment to array type (char)[56] from other type signed int (PredicateCPA:AssignmentHandler.generatePartialAssignmentsForArrayType, WARNING)

lines 795-798: Ignoring assignment to array type (char)[56] from other type signed char (PredicateCPA:AssignmentHandler.generatePartialAssignmentsForArrayType, WARNING)

lines 795-798: Ignoring assignment to array type (char)[56] from other type unsigned long int (PredicateCPA:AssignmentHandler.generatePartialAssignmentsForArrayType, WARNING)

lines 1944-1947: Ignoring assignment to array type (char)[56] from other type unsigned int (PredicateCPA:AssignmentHandler.generatePartialAssignmentsForArrayType, WARNING)

lines 1944-1947: Ignoring assignment to array type (char)[56] from other type signed int (PredicateCPA:AssignmentHandler.generatePartialAssignmentsForArrayType, WARNING)

lines 1944-1947: Ignoring assignment to array type (char)[56] from other type signed char (PredicateCPA:AssignmentHandler.generatePartialAssignmentsForArrayType, WARNING)

lines 1944-1947: Ignoring assignment to array type (char)[56] from other type unsigned long int (PredicateCPA:AssignmentHandler.generatePartialAssignmentsForArrayType, WARNING)

lines 5228-5232: Ignoring assignment to array type (char)[56] from other type unsigned int (PredicateCPA:AssignmentHandler.generatePartialAssignmentsForArrayType, WARNING)

lines 5228-5232: Ignoring assignment to array type (char)[56] from other type signed int (PredicateCPA:AssignmentHandler.generatePartialAssignmentsForArrayType, WARNING)

lines 5228-5232: Ignoring assignment to array type (char)[56] from other type signed char (PredicateCPA:AssignmentHandler.generatePartialAssignmentsForArrayType, WARNING)

lines 5228-5232: Ignoring assignment to array type (char)[56] from other type unsigned long int (PredicateCPA:AssignmentHandler.generatePartialAssignmentsForArrayType, WARNING)

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: Unrecognized C code (Memory assignment function called but their handling is disabled. Set cpa.predicate.enableMemoryAssignmentFunctions=true to enable.): memset((void *)(&ifr), 0, 40UL) (CExpressionVisitorWithPointerAliasing.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.209s
  Time for path formula creation:                      0.205s
Time for strengthen operator:                          0.006s
Time for prec operator:                                0.005s
  Time for abstraction:                  0.001s (Max:     0.001s, 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.004s
  Time for BDD entailment checks:                      0.004s
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.199s

Total number of created targets for pointer analysis: 0


Number of BDD nodes:                               202
Size of BDD node table:                            524309
Size of BDD cache:                                 52433
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.001s
Total time for strengthen operator:                    0.086s
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.000s
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.439s (Max:     0.439s)
  Time for choose from waitlist:      0.001s
  Time for precision adjustment:      0.018s
  Time for transfer relation:         0.389s
  Time for merge operator:            0.006s
  Time for stop operator:             0.005s
  Time for adding to reached set:     0.009s

CPAchecker general statistics
-----------------------------
Number of program locations:                       24394
Number of CFA edges (per node):                       28444 (count: 24394, min: 0, max: 23, avg: 1.17)
Number of relevant variables:                      5580
Number of functions:                               1303
Number of loops (and loop nodes):                       228 (sum: 2856, min: 3, max: 36, avg: 12.53)
Size of reached set:             570
  Number of partitions:          562
    Avg size of partitions:      1
    Max size of partitions:      2 (with key [{main=N1492 (before line 2530) Function parse_opts called from node N1513, stack depth 3 [17f84bc5], stack [main, parse_cli, parse_opts] @@ 0}])
  Number of target states:       0
  Size of final wait list:       3

Time for analysis setup:          2.805s
  Time for loading CPAs:          0.637s
  Time for loading parser:        0.134s
  Time for CFA construction:      2.007s
    Time for parsing file(s):     0.295s
    Time for AST to CFA:          0.444s
    Time for CFA sanity check:    0.000s
    Time for post-processing:     1.187s
    Time for loop structure:      0.044s
    Time for AST structure:       0.000s
      Time for function pointers resolving:            0.014s
        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.648s
        Time for collecting variables:                 0.467s
        Time for solving dependencies:                 0.016s
        Time for building hierarchy:                   0.004s
        Time for building classification:              0.159s
        Time for exporting data:                       0.000s
Time for Analysis:                0.440s
CPU time for analysis:            1.440s
Total time for CPAchecker:        3.246s
Total CPU time for CPAchecker:   10.890s
Time for statistics:              0.044s

Time for Garbage Collector:       0.131s (in 10 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".
