./esbmc-wrapper.py -p /mnt/goblint-svcomp/goblint-bench/bench/concrat/properties/no-data-race.prp -s kinduction --arch 64 /mnt/goblint-svcomp/goblint-bench/bench/concrat/the_silver_searcher/main.c


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


Verifying with ESBMC
Command: ./esbmc --no-div-by-zero-check --force-malloc-success --state-hashing --add-symex-value-sets --no-align-check --k-step 2 --floatbv --unlimited-k-steps --no-vla-size-check /mnt/goblint-svcomp/goblint-bench/bench/concrat/the_silver_searcher/main.c --64  --no-por --context-bound 2 --witness-output witness.graphml --no-pointer-check --no-bounds-check --data-races-check --no-assertions --incremental-bmc 
ESBMC version 7.4.0 64-bit x86_64 linux
Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc
Parsing /mnt/goblint-svcomp/goblint-bench/bench/concrat/the_silver_searcher/main.c
/mnt/goblint-svcomp/goblint-bench/bench/concrat/the_silver_searcher/main.c:5640:40: warning: '__no_sanitize__' attribute ignored when parsing type [-Wignored-attributes]
    return ((char const __attribute__((__no_sanitize__("alignment")))  *)((void *)0));
                                       ^~~~~~~~~~~~~~~~~~~~~~~~~~~~
/mnt/goblint-svcomp/goblint-bench/bench/concrat/the_silver_searcher/main.c:5666:42: warning: '__no_sanitize__' attribute ignored when parsing type [-Wignored-attributes]
      return ((char const __attribute__((__no_sanitize__("alignment")))  *)R);
                                         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~
/mnt/goblint-svcomp/goblint-bench/bench/concrat/the_silver_searcher/main.c:5694:40: warning: '__no_sanitize__' attribute ignored when parsing type [-Wignored-attributes]
    return ((char const __attribute__((__no_sanitize__("alignment")))  *)R___0);
                                       ^~~~~~~~~~~~~~~~~~~~~~~~~~~~
/mnt/goblint-svcomp/goblint-bench/bench/concrat/the_silver_searcher/main.c:5698:38: warning: '__no_sanitize__' attribute ignored when parsing type [-Wignored-attributes]
  return ((char const __attribute__((__no_sanitize__("alignment")))  *)((void *)0));
                                     ^~~~~~~~~~~~~~~~~~~~~~~~~~~~
/mnt/goblint-svcomp/goblint-bench/bench/concrat/the_silver_searcher/main.c:590:21: warning: inline function 'getc_unlocked' is not defined [-Wundefined-inline]
__inline extern int getc_unlocked(FILE *__fp ) ;
                    ^
/mnt/goblint-svcomp/goblint-bench/bench/concrat/the_silver_searcher/main.c:6180:9: note: used here
    c = getc_unlocked(fp);
        ^
Converting
WARNING: function `tolower' in module `main' is shadowed by a definition in module `ctype'
Generating GOTO Program
GOTO program creation time: 0.545s
Adding Data Race Checks
ERROR: Unexpected side-effect: sideeffect
* operand : symbol
    * name : c:main.c@189207@F@ag_realloc@ptr
    * renamelev : Level 0
    * level1_num : 0
    * level2_num : 0
    * thread_num : 0
    * node_num : 0
    * type : pointer
      * subtype : empty
* size : symbol
    * name : c:main.c@189219@F@ag_realloc@size
    * renamelev : Level 0
    * level1_num : 0
    * level2_num : 0
    * thread_num : 0
    * node_num : 0
    * type : unsignedbv
      * width : 64
* arguments : 

* alloctype : realloc
* type : pointer
  * subtype : empty

Unknown
