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/EasyLogger/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/EasyLogger/main.c" (CPAchecker.parse, INFO)

line 2011: Function pointer *elog_assert_hook with type void (*)(const char *expr, const char *func, size_t line) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 1999: Function pointer *elog_assert_hook with type void (*)(const char *expr, const char *func, size_t line) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 1646: Function pointer *elog_assert_hook with type void (*)(const char *expr, const char *func, size_t line) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 1611: Function pointer *elog_assert_hook with type void (*)(const char *expr, const char *func, size_t line) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 1599: Function pointer *elog_assert_hook with type void (*)(const char *expr, const char *func, size_t line) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 1050: Function pointer *elog_assert_hook with type void (*)(const char *expr, const char *func, size_t line) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 1037: Function pointer *elog_assert_hook with type void (*)(const char *expr, const char *func, size_t line) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 1024: Function pointer *elog_assert_hook with type void (*)(const char *expr, const char *func, size_t line) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 1011: Function pointer *elog_assert_hook with type void (*)(const char *expr, const char *func, size_t line) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 998: Function pointer *elog_assert_hook with type void (*)(const char *expr, const char *func, size_t line) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 985: Function pointer *elog_assert_hook with type void (*)(const char *expr, const char *func, size_t line) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 973: Function pointer *elog_assert_hook with type void (*)(const char *expr, const char *func, size_t line) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 1113: Function pointer *elog_assert_hook with type void (*)(const char *expr, const char *func, size_t line) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 1125: Function pointer *elog_assert_hook with type void (*)(const char *expr, const char *func, size_t line) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 1101: Function pointer *elog_assert_hook with type void (*)(const char *expr, const char *func, size_t line) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 1089: Function pointer *elog_assert_hook with type void (*)(const char *expr, const char *func, size_t line) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 599: Function pointer *elog_assert_hook with type void (*)(const char *expr, const char *func, size_t line) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 2068: Function pointer *elog_assert_hook with type void (*)(const char *expr, const char *func, size_t line) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 2056: Function pointer *elog_assert_hook with type void (*)(const char *expr, const char *func, size_t line) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 743: Function pointer *elog_assert_hook with type void (*)(const char *expr, const char *func, size_t line) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 417: Function pointer *elog_assert_hook with type void (*)(const char *expr, const char *func, size_t line) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 440: Function pointer *elog_assert_hook with type void (*)(const char *expr, const char *func, size_t line) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 526: Function pointer *elog_assert_hook with type void (*)(const char *expr, const char *func, size_t line) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 539: Function pointer *elog_assert_hook with type void (*)(const char *expr, const char *func, size_t line) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 396: Function pointer *elog_assert_hook with type void (*)(const char *expr, const char *func, size_t line) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 348: Function pointer *elog_assert_hook with type void (*)(const char *expr, const char *func, size_t line) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 1957: Function pointer *elog_assert_hook with type void (*)(const char *expr, const char *func, size_t line) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 1945: Function pointer *elog_assert_hook with type void (*)(const char *expr, const char *func, size_t line) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 912: Function pointer *elog_assert_hook with type void (*)(const char *expr, const char *func, size_t line) 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)

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

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

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

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

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

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

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

lines 313-314: Ignoring parameters passed as varargs to function elog_output: elog_output(3U, "elog", "../../../easylogger/src/elog.c", "elog_start", 244L, "EasyLogger V%s is initialize success.", "2.2.99") (PredicateCPA:CtoFormulaConverter.makeFunctionCall, WARNING)

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

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

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

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

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

Error: line 1460: Unrecognized C code (unsupported thread assignment): (pthread_t *)(&async_output_thread) (ThreadingTransferRelation.startNewThread, SEVERE)


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

Max ABE block size:                       27
Avg ABE block size:                                3.23 (sum: 381, count: 118, min: 0, max: 27)
Number of predicates discovered:          0

Time for post operator:                                1.820s
  Time for path formula creation:                      1.815s
Time for strengthen operator:                          0.009s
Time for prec operator:                                0.015s
  Time for abstraction:                  0.004s (Max:     0.001s, Count: 118)
    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.009s
Time for coverage checks:                              0.008s
  Time for BDD entailment checks:                      0.008s
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:     1.805s

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: 654, min: 0, max: 0)
Time for BDD node cleanup:                             0.001s
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:                     12.23 (sum: 8597, count: 703, min: 0, max: 26)
Number of global variables per state:              9.80 (sum: 6890, count: 703, min: 0, max: 20)
Number of assumptions:                                  216
Number of deterministic assumptions:                      0
Level of Determinism:                              0%

ValueAnalysisPrecisionAdjustment statistics
-------------------------------------------
Number of abstraction computations:                     735
Total time for liveness abstraction:                   0.000s
Total time for abstraction computation:                0.005s
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.004s
Total time for strengthen operator:                    0.096s
Automaton transfers with branching:                0
Automaton transfer successors:                     1.00 (sum: 735, count: 735, min: 1, max: 1) [1 x 735]
Number of states with assumption transitions:      0

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

CPA algorithm statistics
------------------------
Number of iterations:            704
Max size of waitlist:            17
Average size of waitlist:        7
Number of computed successors:   735
Max successors for one state:    2
Number of times merged:          11
Number of times stopped:         33
Number of times breaked:         0

Total time for CPA algorithm:         2.161s (Max:     2.161s)
  Time for choose from waitlist:      0.005s
  Time for precision adjustment:      0.033s
  Time for transfer relation:         2.067s
  Time for merge operator:            0.028s
  Time for stop operator:             0.009s
  Time for adding to reached set:     0.008s

CPAchecker general statistics
-----------------------------
Number of program locations:                       8227
Number of CFA edges (per node):                        9855 (count: 8227, min: 0, max: 37, avg: 1.20)
Number of relevant variables:                      1354
Number of functions:                               361
Number of loops (and loop nodes):                       300 (sum: 1890, min: 2, max: 54, avg: 6.30)
Size of reached set:             703
  Number of partitions:          624
    Avg size of partitions:      1
    Max size of partitions:      12 (with key [{main=N1174 (entry of function elog_file_port_unlock in lines 1717-1727) Function elog_file_port_unlock called from node N1146, stack depth 6 [72b4ecb2], stack [main, elog_init, elog_port_init, elog_file_init, elog_file_config, elog_file_port_unlock] @@ 0}])
  Number of target states:       0
  Size of final wait list:       11

Time for analysis setup:          1.816s
  Time for loading CPAs:          0.580s
  Time for loading parser:        0.141s
  Time for CFA construction:      1.065s
    Time for parsing file(s):     0.243s
    Time for AST to CFA:          0.278s
    Time for CFA sanity check:    0.001s
    Time for post-processing:     0.482s
    Time for loop structure:      0.050s
    Time for AST structure:       0.000s
      Time for function pointers resolving:            0.009s
        Function calls via function pointers:            29 (count: 1, min: 29, max: 29, avg: 29.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 classifying variables:                  0.289s
        Time for collecting variables:                 0.193s
        Time for solving dependencies:                 0.005s
        Time for building hierarchy:                   0.001s
        Time for building classification:              0.089s
        Time for exporting data:                       0.000s
Time for Analysis:                2.163s
CPU time for analysis:            6.410s
Total time for CPAchecker:        3.979s
Total CPU time for CPAchecker:   12.340s
Time for statistics:              0.050s

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