./Dartagnan-SVCOMP.sh /mnt/goblint-svcomp/goblint-bench/bench/concrat/properties/no-data-race.prp /mnt/goblint-svcomp/goblint-bench/bench/concrat/kona/main.c


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


13:32:37 [INFO ] Compilation.compileWithClang - Compiling with clang
Exception in thread "main" java.lang.Exception: /mnt/goblint-svcomp/benchexec/tools-pldi/dartagnan/output/main_tmp.c:5714:62: warning: integer literal is too large to be represented in a signed integer type, interpreting as unsigned [-Wimplicitly-unsigned-literal]
  return ((__uint64_t )((((((((((unsigned long long )__bsx & 18374686479671623680) >> 56) | (((unsigned long long )__bsx & 71776119061217280ULL) >> 40)) | (((unsigned long long )__bsx & 280375465082880ULL) >> 24)) | (((unsigned long long )__bsx & 1095216660480ULL) >> 8)) | (((unsigned long long )__bsx & 4278190080ULL) << 8)) | (((unsigned long long )__bsx & 16711680ULL) << 24)) | (((unsigned long long )__bsx & 65280ULL) << 40)) | (((unsigned long long )__bsx & 255ULL) << 56)));
                                                             ^
/mnt/goblint-svcomp/benchexec/tools-pldi/dartagnan/output/main_tmp.c:6908:57: warning: integer literal is too large to be represented in a signed integer type, interpreting as unsigned [-Wimplicitly-unsigned-literal]
static unsigned long long mag01[2]  = {      0ULL,      13043109905998158313};
                                                        ^
/mnt/goblint-svcomp/benchexec/tools-pldi/dartagnan/output/main_tmp.c:6922:24: warning: integer literal is too large to be represented in a signed integer type, interpreting as unsigned [-Wimplicitly-unsigned-literal]
      x___0 = (mt[i] & 18446744071562067968) | (mt[i + 1] & 2147483647ULL);
                       ^
/mnt/goblint-svcomp/benchexec/tools-pldi/dartagnan/output/main_tmp.c:6927:24: warning: integer literal is too large to be represented in a signed integer type, interpreting as unsigned [-Wimplicitly-unsigned-literal]
      x___0 = (mt[i] & 18446744071562067968) | (mt[i + 1] & 2147483647ULL);
                       ^
/mnt/goblint-svcomp/benchexec/tools-pldi/dartagnan/output/main_tmp.c:6931:24: warning: integer literal is too large to be represented in a signed integer type, interpreting as unsigned [-Wimplicitly-unsigned-literal]
    x___0 = (mt[311] & 18446744071562067968) | (mt[0] & 2147483647ULL);
                       ^
/mnt/goblint-svcomp/benchexec/tools-pldi/dartagnan/output/main_tmp.c:6940:28: warning: integer literal is too large to be represented in a signed integer type, interpreting as unsigned [-Wimplicitly-unsigned-literal]
  x___0 ^= (x___0 << 37) & 18444473444759240704;
                           ^
/mnt/goblint-svcomp/benchexec/tools-pldi/dartagnan/output/main_tmp.c:14921:35: error: cannot redeclare builtin function '__builtin_isnan'
extern int ( /* missing proto */  __builtin_isnan)() ;
                                  ^
/mnt/goblint-svcomp/benchexec/tools-pldi/dartagnan/output/main_tmp.c:14921:35: note: '__builtin_isnan' is a builtin with type 'int ()'
/mnt/goblint-svcomp/benchexec/tools-pldi/dartagnan/output/main_tmp.c:20415:82: warning: adding 'int' to a string does not append to the string [-Wstring-plus-int]
            tmp___35 = strchr((char const   *)((C *)((z->k[2])->k)), (int )*("z" + 0));
                                                                             ~~~~^~~
/mnt/goblint-svcomp/benchexec/tools-pldi/dartagnan/output/main_tmp.c:20415:82: note: use array indexing to silence this warning
            tmp___35 = strchr((char const   *)((C *)((z->k[2])->k)), (int )*("z" + 0));
                                                                                 ^
                                                                             &   [  ]
/mnt/goblint-svcomp/benchexec/tools-pldi/dartagnan/output/main_tmp.c:20480:82: warning: adding 'int' to a string does not append to the string [-Wstring-plus-int]
            tmp___42 = strchr((char const   *)((C *)((z->k[2])->k)), (int )*("y" + 0));
                                                                             ~~~~^~~
/mnt/goblint-svcomp/benchexec/tools-pldi/dartagnan/output/main_tmp.c:20480:82: note: use array indexing to silence this warning
            tmp___42 = strchr((char const   *)((C *)((z->k[2])->k)), (int )*("y" + 0));
                                                                                 ^
                                                                             &   [  ]
/mnt/goblint-svcomp/benchexec/tools-pldi/dartagnan/output/main_tmp.c:20560:82: warning: adding 'int' to a string does not append to the string [-Wstring-plus-int]
            tmp___50 = strchr((char const   *)((C *)((z->k[2])->k)), (int )*("x" + 0));
                                                                             ~~~~^~~
/mnt/goblint-svcomp/benchexec/tools-pldi/dartagnan/output/main_tmp.c:20560:82: note: use array indexing to silence this warning
            tmp___50 = strchr((char const   *)((C *)((z->k[2])->k)), (int )*("x" + 0));
                                                                                 ^
                                                                             &   [  ]
/mnt/goblint-svcomp/benchexec/tools-pldi/dartagnan/output/main_tmp.c:22060:98: warning: adding 'int' to a string does not append to the string [-Wstring-plus-int]
                    if ((int )*((C *)((prnt->k[2])->k) + ((prnt->k[2])->n - 1LL)) == (int )*("}" + 0)) {
                                                                                             ~~~~^~~
/mnt/goblint-svcomp/benchexec/tools-pldi/dartagnan/output/main_tmp.c:22060:98: note: use array indexing to silence this warning
                    if ((int )*((C *)((prnt->k[2])->k) + ((prnt->k[2])->n - 1LL)) == (int )*("}" + 0)) {
                                                                                                 ^
                                                                                             &   [  ]
/mnt/goblint-svcomp/benchexec/tools-pldi/dartagnan/output/main_tmp.c:22062:53: warning: adding 'int' to a string does not append to the string [-Wstring-plus-int]
                                        (int )*("y" + 0));
                                                ~~~~^~~
/mnt/goblint-svcomp/benchexec/tools-pldi/dartagnan/output/main_tmp.c:22062:53: note: use array indexing to silence this warning
                                        (int )*("y" + 0));
                                                    ^
                                                &   [  ]
/mnt/goblint-svcomp/benchexec/tools-pldi/dartagnan/output/main_tmp.c:23956:53: warning: integer literal is too large to be represented in a signed integer type, interpreting as unsigned [-Wimplicitly-unsigned-literal]
  x___0->_c = (I )((unsigned long long )x___0->_c & 18446744073709551360);
                                                    ^
/mnt/goblint-svcomp/benchexec/tools-pldi/dartagnan/output/main_tmp.c:31650:35: error: cannot redeclare builtin function '__builtin_isinf_sign'
extern int ( /* missing proto */  __builtin_isinf_sign)() ;
                                  ^
/mnt/goblint-svcomp/benchexec/tools-pldi/dartagnan/output/main_tmp.c:31650:35: note: '__builtin_isinf_sign' is a builtin with type 'int ()'
/mnt/goblint-svcomp/benchexec/tools-pldi/dartagnan/output/main_tmp.c:34754:35: error: cannot redeclare builtin function '__builtin_signbit'
extern int ( /* missing proto */  __builtin_signbit)() ;
                                  ^
/mnt/goblint-svcomp/benchexec/tools-pldi/dartagnan/output/main_tmp.c:34754:35: note: '__builtin_signbit' is a builtin with type 'int ()'
/mnt/goblint-svcomp/benchexec/tools-pldi/dartagnan/output/main_tmp.c:35065:11: warning: integer literal is too large to be represented in a signed integer type, interpreting as unsigned [-Wimplicitly-unsigned-literal]
  return (9223372036854775808 ^ (uI )a);
          ^
13 warnings and 3 errors generated.

	at com.dat3m.dartagnan.parsers.program.utils.Compilation.compileWithClang(Compilation.java:74)
	at com.dat3m.svcomp.SVCOMPRunner.main(SVCOMPRunner.java:116)
