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

line 3760: Function pointer *fnstrstr with type char *(*)(const char *haystack, const char *needle) 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)

line 857: Ignoring assignment to (g_ctx[0]).c_cfg.timeorder because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[0]).c_cfg.sizeorder because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[0]).c_cfg.apparentsz because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[0]).c_cfg.blkorder because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[0]).c_cfg.extnorder because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[0]).c_cfg.showhidden because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[0]).c_cfg.ctxactive because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[0]).c_cfg.reverse because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[0]).c_cfg.version because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[0]).c_cfg.curctx because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[0]).c_cfg.fileinfo because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[0]).c_cfg.nonavopen because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[0]).c_cfg.autoenter because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[0]).c_cfg.useeditor because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[0]).c_cfg.regex because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[0]).c_cfg.timetype because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[0]).c_cfg.cliopener because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[0]).c_cfg.waitedit because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[0]).c_cfg.rollover because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[1]).c_cfg.timeorder because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[1]).c_cfg.sizeorder because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[1]).c_cfg.apparentsz because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[1]).c_cfg.blkorder because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[1]).c_cfg.extnorder because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[1]).c_cfg.showhidden because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[1]).c_cfg.ctxactive because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[1]).c_cfg.reverse because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[1]).c_cfg.version because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[1]).c_cfg.curctx because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[1]).c_cfg.fileinfo because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[1]).c_cfg.nonavopen because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[1]).c_cfg.autoenter because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[1]).c_cfg.useeditor because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[1]).c_cfg.regex because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[1]).c_cfg.timetype because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[1]).c_cfg.cliopener because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[1]).c_cfg.waitedit because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[1]).c_cfg.rollover because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[2]).c_cfg.timeorder because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[2]).c_cfg.sizeorder because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[2]).c_cfg.apparentsz because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[2]).c_cfg.blkorder because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[2]).c_cfg.extnorder because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[2]).c_cfg.showhidden because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[2]).c_cfg.ctxactive because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[2]).c_cfg.reverse because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[2]).c_cfg.version because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[2]).c_cfg.curctx because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[2]).c_cfg.fileinfo because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[2]).c_cfg.nonavopen because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[2]).c_cfg.autoenter because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[2]).c_cfg.useeditor because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[2]).c_cfg.regex because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[2]).c_cfg.timetype because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[2]).c_cfg.cliopener because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[2]).c_cfg.waitedit because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[2]).c_cfg.rollover because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[3]).c_cfg.timeorder because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[3]).c_cfg.sizeorder because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[3]).c_cfg.apparentsz because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[3]).c_cfg.blkorder because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[3]).c_cfg.extnorder because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[3]).c_cfg.showhidden because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[3]).c_cfg.ctxactive because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[3]).c_cfg.reverse because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[3]).c_cfg.version because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[3]).c_cfg.curctx because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[3]).c_cfg.fileinfo because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[3]).c_cfg.nonavopen because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[3]).c_cfg.autoenter because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[3]).c_cfg.useeditor because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[3]).c_cfg.regex because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[3]).c_cfg.timetype because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[3]).c_cfg.cliopener because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[3]).c_cfg.waitedit because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

line 857: Ignoring assignment to (g_ctx[3]).c_cfg.rollover because bit fields are currently not fully supported (PredicateCPA:AssignmentHandler.handleAssignment, WARNING)

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

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

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

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

Assuming external function __errno_location to be a constant function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO)

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

Assuming external function strerror 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 wattr_on to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Assuming external function read 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 realloc to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO)

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

