scripts/cpa.sh -svcomp23 -heap 4000M -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/siege/main.c


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


Running CPAchecker with Java heap of size 4000M.
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.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/siege/main.c" (CPAchecker.parse, INFO)

line 2588: Dead code detected: __res = toupper((int )*(password + i)); (CFACreationUtils.addEdgeToCFA, INFO)

line 6628: Dead code detected: return ((BOOLEAN )0); (CFACreationUtils.addEdgeToCFA, INFO)

line 7146: Dereferencing of non-pointer type CREW  in expression *this (ASTConverter.convert, WARNING)

line 7276: Dead code detected: return ((void *)0); (CFACreationUtils.addEdgeToCFA, INFO)

line 7533: Dereferencing of non-pointer type DATA  in expression *this (ASTConverter.convert, WARNING)

line 8752: Dead code detected: return ((BOOLEAN )1); (CFACreationUtils.addEdgeToCFA, INFO)

line 10507: Dead code detected: return (resp); (CFACreationUtils.addEdgeToCFA, INFO)

line 10559: Dead code detected: return (-1); (CFACreationUtils.addEdgeToCFA, INFO)

line 12637: Dead code detected: return ((BOOLEAN )0); (CFACreationUtils.addEdgeToCFA, INFO)

line 15028: Dead code detected: __res = tolower((int )((unsigned char )c)); (CFACreationUtils.addEdgeToCFA, INFO)

line 15044: Dead code detected: __res___0 = tolower((int )((unsigned char )sc)); (CFACreationUtils.addEdgeToCFA, INFO)

line 17479: Dead code detected: continue; (CFACreationUtils.addEdgeToCFA, INFO)

line 17484: Dead code detected: continue; (CFACreationUtils.addEdgeToCFA, INFO)

line 17488: Dead code detected: continue; (CFACreationUtils.addEdgeToCFA, INFO)

line 17492: Dead code detected: continue; (CFACreationUtils.addEdgeToCFA, INFO)

line 18419: Dead code detected: return; (CFACreationUtils.addEdgeToCFA, INFO)

line 19119: Dead code detected: __res = toupper((int )*(p + 1)); (CFACreationUtils.addEdgeToCFA, INFO)

line 19130: Dead code detected: __res___0 = toupper((int )*(p + 2)); (CFACreationUtils.addEdgeToCFA, INFO)

line 19291: Dead code detected: __res = toupper((int )*(p1 + 1)); (CFACreationUtils.addEdgeToCFA, INFO)

line 19302: Dead code detected: __res___0 = toupper((int )*(p1 + 2)); (CFACreationUtils.addEdgeToCFA, INFO)

line 19433: Dead code detected: __res = tolower((int )*(p + x)); (CFACreationUtils.addEdgeToCFA, INFO)

line 19622: Dead code detected: __res = toupper((int )*c); (CFACreationUtils.addEdgeToCFA, INFO)

line 19645: Dead code detected: __res = tolower((int )*c); (CFACreationUtils.addEdgeToCFA, INFO)

line 19672: Dead code detected: __res = tolower((int )((unsigned char )*h)); (CFACreationUtils.addEdgeToCFA, INFO)

line 19678: Dead code detected: __res___0 = tolower((int )((unsigned char )*n)); (CFACreationUtils.addEdgeToCFA, INFO)

Inline assembler ignored, analysis is probably unsound! (CFABuilder.createCFA, WARNING)

line 1073: Function pointer *__compar with type int (*)(const void *, const void *) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

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

Error: Parsing failed (line 7273: Method __signal_cleanup takes 0 parameter(s) but is called with 1 parameter(s): __signal_cleanup(workptr->arg); (line was originally pointer call(__signal_cleanup) (*(workptr->routine))(workptr->arg);)) (CFASecondPassBuilder.createCallAndReturnEdges, SEVERE)

Please make sure that the code can be compiled by a compiler.
If the code was not preprocessed, please use a C preprocessor
or specify the -preprocess command-line argument.
If the error still occurs, please send this error message
together with the input file to cpachecker-users@googlegroups.com.
 (CPAchecker.run, INFO)


CPAchecker general statistics
-----------------------------

Time for analysis setup:          6.664s
  Time for loading CPAs:          0.000s
  Time for loading parser:        0.281s
  Time for CFA construction:      6.337s
    Time for parsing file(s):     1.015s
    Time for AST to CFA:          2.300s
    Time for CFA sanity check:    0.001s
    Time for post-processing:     2.814s
      Time for function pointers resolving:            0.032s
        Function calls via function pointers:             6 (count: 1, min: 6, max: 6, avg: 6.00)
        Instrumented function pointer calls:              5 (count: 1, min: 5, max: 5, avg: 5.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 Analysis:                0.000s
CPU time for analysis:            0.000s
Total time for CPAchecker:        6.664s
Total CPU time for CPAchecker:    0.740s
Time for statistics:              0.007s

Time for Garbage Collector:       0.774s (in 19 runs)
Garbage Collector(s) used:    Copy, MarkSweepCompact

More details about the verification run can be found in the directory "./output".
