Incompatible ikinds exception on svcomp22 reachsafety tests

[MartinWehking]

The following tests fail:

• sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.yml
• (sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.yml

with the following exception (the same for both):
Fatal error: exception IntDomain.IncompatibleIKinds("ikinds unsigned long long and unsigned int are incompatible. Values: (Unknown int([0,64]),[0,18446744073709551615]) and (Unknown int([0,32]),[0,4294967295])")

My settings:

{
  "ana": {
    "sv-comp": {
      "enabled": true,
      "functions": true
    },
    "int": {
      "def_exc": true,
      "enums": false,
      "interval": true
    },
    "activated": [
      "base",
      "threadid",
      "threadflag",
      "mallocWrapper",
      "mutex",
      "access",
      "escape",
      "expRelation",
      "apron",
      "mutexEvents",
      "symb_locks",
      "region",
      "thread"
    ],
    "context": {
      "widen": false
    },
    "malloc": {
      "wrappers": [
        "kmalloc",
        "__kmalloc",
        "usb_alloc_urb",
        "__builtin_alloca",
        "kzalloc",

        "ldv_malloc",

        "kzalloc_node",
        "ldv_zalloc",
        "kmalloc_array",
        "kcalloc"
      ]
    },
    "base": {
      "arrays": {
        "domain": "partitioned"
      }
    },
    "apron":{
    "domain": "octagon"
    }
  },
  "exp": {
    "region-offsets": true
  },
  "solver": "td3",
  "sem": {
    "unknown_function": {
      "spawn": false
    },
    "int": {
      "signed_overflow": "assume_none"
    }
  },
  "witness": {
    "id": "enumerate",
    "unknown": false
  }
}

This issue seems to only occur when Apron is activated

[michael-schwarz]

Thanks for flagging this!

[michael-schwarz]

We will not have time to address this for this year's SVCOMP, moving to 2024.

[jerhard]

Goblint also crashes with an IncompatibleIkinds exception on the sqlite-amalgamation in some configuration.

[michael-schwarz]

Do you have a line number here? I think debugging the amalgamation makes more sense than these LDV programs that are dubious anyway.

[jerhard]

Do you have a line number here?

No, not yet, this was run on a version of Goblint that did not print the lint number. I now started a run with the current master merged, so that hopefullly yields a line number.

[jerhard]

Now with #931 merged, there is a whole stack of line numbers:

Stack trace

Fatal error: exception Goblint_lib.IntDomain.IncompatibleIKinds("ikinds int and unsigned long are incompatible. Values: (0) and (0)")
Marked with transfer function at sqlite/sqlite3.c:107022:17-107022:91
Marked with transfer function at sqlite/sqlite3.c:106307:11-106307:77
Marked with transfer function at sqlite/sqlite3.c:106361:5-106361:55
Marked with transfer function at sqlite/sqlite3.c:105823:9-105823:60
Marked with transfer function at sqlite/sqlite3.c:106364:5-106364:50
Marked with transfer function at sqlite/sqlite3.c:106888:9-106888:59
Marked with transfer function at sqlite/sqlite3.c:106782:9-106782:59
Marked with transfer function at sqlite/sqlite3.c:148220:5-148220:55
Marked with transfer function at sqlite/sqlite3.c:155242:5-155242:80
Marked with transfer function at sqlite/sqlite3.c:139473:5-139474:69
Marked with transfer function at sqlite/sqlite3.c:139331:7-139331:41
Marked with transfer function at sqlite/sqlite3.c:135184:3-135184:49
Marked with transfer function at sqlite/sqlite3.c:135379:5-135379:49
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:135559:9-135559:59
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:135478:9-135478:55
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:135407:9-135407:50
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:136085:3-136085:40
Marked with transfer function at sqlite/sqlite3.c:135386:5-135386:48
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:104840:7-104840:42
Marked with transfer function at sqlite/sqlite3.c:105390:7-105390:48
Marked with transfer function at sqlite/sqlite3.c:106550:5-106550:66
Marked with transfer function at sqlite/sqlite3.c:106692:7-106692:74
Marked with transfer function at sqlite/sqlite3.c:106609:9-106609:58
Marked with transfer function at sqlite/sqlite3.c:106790:9-106791:43
Marked with transfer function at sqlite/sqlite3.c:106782:9-106782:59
Marked with transfer function at sqlite/sqlite3.c:106227:9-106227:58
Marked with transfer function at sqlite/sqlite3.c:105454:7-105454:62
Marked with transfer function at sqlite/sqlite3.c:105920:9-105921:57
Marked with transfer function at sqlite/sqlite3.c:106387:3-106387:55
Marked with transfer function at sqlite/sqlite3.c:106321:7-106321:46
Marked with transfer function at sqlite/sqlite3.c:105899:9-105899:61
Marked with transfer function at sqlite/sqlite3.c:106387:3-106387:55
Marked with transfer function at sqlite/sqlite3.c:158491:5-158491:53
Marked with transfer function at sqlite/sqlite3.c:139507:7-139507:68
Marked with transfer function at sqlite/sqlite3.c:139331:7-139331:41
Marked with transfer function at sqlite/sqlite3.c:135184:3-135184:49
Marked with transfer function at sqlite/sqlite3.c:135379:5-135379:49
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:135559:9-135559:59
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:135478:9-135478:55
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:135407:9-135407:50
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:136085:3-136085:40
Marked with transfer function at sqlite/sqlite3.c:135386:5-135386:48
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:104653:7-104653:77
Marked with transfer function at sqlite/sqlite3.c:104445:5-104445:41
Marked with transfer function at sqlite/sqlite3.c:104951:3-104954:43
Marked with transfer function at sqlite/sqlite3.c:106699:7-106699:64
Marked with transfer function at sqlite/sqlite3.c:106609:9-106609:58
Marked with transfer function at sqlite/sqlite3.c:106790:9-106791:43
Marked with transfer function at sqlite/sqlite3.c:106782:9-106782:59
Marked with transfer function at sqlite/sqlite3.c:106227:9-106227:58
Marked with transfer function at sqlite/sqlite3.c:105454:7-105454:62
Marked with transfer function at sqlite/sqlite3.c:105920:9-105921:57
Marked with transfer function at sqlite/sqlite3.c:106387:3-106387:55
Marked with transfer function at sqlite/sqlite3.c:106321:7-106321:46
Marked with transfer function at sqlite/sqlite3.c:105899:9-105899:61
Marked with transfer function at sqlite/sqlite3.c:106481:11-106481:65
Marked with transfer function at sqlite/sqlite3.c:133206:3-133207:47
Marked with transfer function at sqlite/sqlite3.c:133786:7-133786:49
Marked with transfer function at sqlite/sqlite3.c:135279:5-135279:54
Marked with transfer function at sqlite/sqlite3.c:135366:5-135366:45
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:104840:7-104840:42
Marked with transfer function at sqlite/sqlite3.c:146855:7-146855:48
Marked with transfer function at sqlite/sqlite3.c:147152:9-147152:53
Marked with transfer function at sqlite/sqlite3.c:155242:5-155242:80
Marked with transfer function at sqlite/sqlite3.c:139473:5-139474:69
Marked with transfer function at sqlite/sqlite3.c:135184:3-135184:49
Marked with transfer function at sqlite/sqlite3.c:135379:5-135379:49
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:135559:9-135559:59
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:135478:9-135478:55
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:135407:9-135407:50
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:136085:3-136085:40
Marked with transfer function at sqlite/sqlite3.c:135386:5-135386:48
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:139331:7-139331:41
Marked with transfer function at sqlite/sqlite3.c:104840:7-104840:42
Marked with transfer function at sqlite/sqlite3.c:105390:7-105390:48
Marked with transfer function at sqlite/sqlite3.c:106550:5-106550:66
Marked with transfer function at sqlite/sqlite3.c:106692:7-106692:74
Marked with transfer function at sqlite/sqlite3.c:106609:9-106609:58
Marked with transfer function at sqlite/sqlite3.c:106790:9-106791:43
Marked with transfer function at sqlite/sqlite3.c:106782:9-106782:59
Marked with transfer function at sqlite/sqlite3.c:106227:9-106227:58
Marked with transfer function at sqlite/sqlite3.c:105454:7-105454:62
Marked with transfer function at sqlite/sqlite3.c:105920:9-105921:57
Marked with transfer function at sqlite/sqlite3.c:106387:3-106387:55
Marked with transfer function at sqlite/sqlite3.c:106321:7-106321:46
Marked with transfer function at sqlite/sqlite3.c:105899:9-105899:61
Marked with transfer function at sqlite/sqlite3.c:106481:11-106481:65
Marked with transfer function at sqlite/sqlite3.c:133206:3-133207:47
Marked with transfer function at sqlite/sqlite3.c:133786:7-133786:49
Marked with transfer function at sqlite/sqlite3.c:135279:5-135279:54
Marked with transfer function at sqlite/sqlite3.c:135366:5-135366:45
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:104840:7-104840:42
Marked with transfer function at sqlite/sqlite3.c:105390:7-105390:48
Marked with transfer function at sqlite/sqlite3.c:106550:5-106550:66
Marked with transfer function at sqlite/sqlite3.c:106692:7-106692:74
Marked with transfer function at sqlite/sqlite3.c:106609:9-106609:58
Marked with transfer function at sqlite/sqlite3.c:106790:9-106791:43
Marked with transfer function at sqlite/sqlite3.c:106782:9-106782:59
Marked with transfer function at sqlite/sqlite3.c:106227:9-106227:58
Marked with transfer function at sqlite/sqlite3.c:105454:7-105454:62
Marked with transfer function at sqlite/sqlite3.c:105920:9-105921:57
Marked with transfer function at sqlite/sqlite3.c:105593:9-105593:66
Marked with transfer function at sqlite/sqlite3.c:106387:3-106387:55
Marked with transfer function at sqlite/sqlite3.c:106321:7-106321:46
Marked with transfer function at sqlite/sqlite3.c:106361:5-106361:55
Marked with transfer function at sqlite/sqlite3.c:106661:7-106661:64
Marked with transfer function at sqlite/sqlite3.c:106609:9-106609:58
Marked with transfer function at sqlite/sqlite3.c:106790:9-106791:43
Marked with transfer function at sqlite/sqlite3.c:106782:9-106782:59
Marked with transfer function at sqlite/sqlite3.c:106910:5-106910:56
Marked with transfer function at sqlite/sqlite3.c:119822:7-119823:34
Marked with transfer function at sqlite/sqlite3.c:130754:13-130755:53
Marked with transfer function at sqlite/sqlite3.c:163234:2-163234:68
Marked with transfer function at sqlite/sqlite3.c:163869:7-163869:68
Marked with transfer function at sqlite/sqlite3.c:165165:5-165165:58
Marked with transfer function at sqlite/sqlite3.c:132359:5-132359:46
Marked with transfer function at sqlite/sqlite3.c:131770:5-131770:59
Marked with transfer function at sqlite/sqlite3.c:131864:3-131864:55
Marked with transfer function at sqlite/sqlite3.c:132073:5-132073:44
Marked with transfer function at sqlite/sqlite3.c:132099:5-132099:43
Marked with transfer function at sqlite/sqlite3.c:113312:8-113314:3
Marked with transfer function at sqlite/sqlite3.c:113377:3-113377:58
Marked with transfer function at sqlite/sqlite3.c:138121:7-138121:68
Marked with transfer function at sqlite/sqlite3.c:99520:5-99520:46
Marked with transfer function at sqlite/sqlite3.c:138391:3-138391:33
Marked with transfer function at sqlite/sqlite3.c:138476:3-138476:33
Marked with transfer function at sqlite/sqlite3.c:138953:3-138953:34
Marked with transfer function at sqlite/sqlite3.c:104840:7-104840:42
Marked with transfer function at sqlite/sqlite3.c:105390:7-105390:48
Marked with transfer function at sqlite/sqlite3.c:106550:5-106550:66
Marked with transfer function at sqlite/sqlite3.c:106692:7-106692:74
Marked with transfer function at sqlite/sqlite3.c:106609:9-106609:58
Marked with transfer function at sqlite/sqlite3.c:106790:9-106791:43
Marked with transfer function at sqlite/sqlite3.c:106782:9-106782:59
Marked with transfer function at sqlite/sqlite3.c:106227:9-106227:58
Marked with transfer function at sqlite/sqlite3.c:105454:7-105454:62
Marked with transfer function at sqlite/sqlite3.c:105920:9-105921:57
Marked with transfer function at sqlite/sqlite3.c:106387:3-106387:55
Marked with transfer function at sqlite/sqlite3.c:106321:7-106321:46
Marked with transfer function at sqlite/sqlite3.c:105899:9-105899:61
Marked with transfer function at sqlite/sqlite3.c:106481:11-106481:65
Marked with transfer function at sqlite/sqlite3.c:133206:3-133207:47
Marked with transfer function at sqlite/sqlite3.c:133786:7-133786:49
Marked with transfer function at sqlite/sqlite3.c:135279:5-135279:54
Marked with transfer function at sqlite/sqlite3.c:135366:5-135366:45
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:135559:9-135559:59
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:135478:9-135478:55
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:135407:9-135407:50
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:136085:3-136085:40
Marked with transfer function at sqlite/sqlite3.c:135386:5-135386:48
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:104840:7-104840:42
Marked with transfer function at sqlite/sqlite3.c:105390:7-105390:48
Marked with transfer function at sqlite/sqlite3.c:106550:5-106550:66
Marked with transfer function at sqlite/sqlite3.c:106692:7-106692:74
Marked with transfer function at sqlite/sqlite3.c:106609:9-106609:58
Marked with transfer function at sqlite/sqlite3.c:106790:9-106791:43
Marked with transfer function at sqlite/sqlite3.c:106782:9-106782:59
Marked with transfer function at sqlite/sqlite3.c:106227:9-106227:58
Marked with transfer function at sqlite/sqlite3.c:105454:7-105454:62
Marked with transfer function at sqlite/sqlite3.c:105920:9-105921:57
Marked with transfer function at sqlite/sqlite3.c:106387:3-106387:55
Marked with transfer function at sqlite/sqlite3.c:106321:7-106321:46
Marked with transfer function at sqlite/sqlite3.c:105899:9-105899:61
Marked with transfer function at sqlite/sqlite3.c:106481:11-106481:65
Marked with transfer function at sqlite/sqlite3.c:133206:3-133207:47
Marked with transfer function at sqlite/sqlite3.c:133786:7-133786:49
Marked with transfer function at sqlite/sqlite3.c:135279:5-135279:54
Marked with transfer function at sqlite/sqlite3.c:135366:5-135366:45
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:115576:7-115576:44
Marked with transfer function at sqlite/sqlite3.c:162284:3-162284:52
Marked with transfer function at sqlite/sqlite3.c:163869:7-163869:68
Marked with transfer function at sqlite/sqlite3.c:165165:5-165165:58
Marked with transfer function at sqlite/sqlite3.c:132359:5-132359:46
Marked with transfer function at sqlite/sqlite3.c:131770:5-131770:59
Marked with transfer function at sqlite/sqlite3.c:131864:3-131864:55
Marked with transfer function at sqlite/sqlite3.c:132073:5-132073:44
Marked with transfer function at sqlite/sqlite3.c:132099:5-132099:43
Marked with transfer function at sqlite/sqlite3.c:113312:8-113314:3
Marked with transfer function at sqlite/sqlite3.c:113377:3-113377:58
Marked with transfer function at sqlite/sqlite3.c:138121:7-138121:68
Marked with transfer function at sqlite/sqlite3.c:99520:5-99520:46
Marked with transfer function at sqlite/sqlite3.c:138391:3-138391:33
Marked with transfer function at sqlite/sqlite3.c:138476:3-138476:33
Marked with transfer function at sqlite/sqlite3.c:138953:3-138953:34
Marked with transfer function at sqlite/sqlite3.c:104840:7-104840:42
Marked with transfer function at sqlite/sqlite3.c:105390:7-105390:48
Marked with transfer function at sqlite/sqlite3.c:106550:5-106550:66
Marked with transfer function at sqlite/sqlite3.c:106692:7-106692:74
Marked with transfer function at sqlite/sqlite3.c:106609:9-106609:58
Marked with transfer function at sqlite/sqlite3.c:106790:9-106791:43
Marked with transfer function at sqlite/sqlite3.c:106782:9-106782:59
Marked with transfer function at sqlite/sqlite3.c:106227:9-106227:58
Marked with transfer function at sqlite/sqlite3.c:105454:7-105454:62
Marked with transfer function at sqlite/sqlite3.c:105920:9-105921:57
Marked with transfer function at sqlite/sqlite3.c:106387:3-106387:55
Marked with transfer function at sqlite/sqlite3.c:106321:7-106321:46
Marked with transfer function at sqlite/sqlite3.c:105899:9-105899:61
Marked with transfer function at sqlite/sqlite3.c:106481:11-106481:65
Marked with transfer function at sqlite/sqlite3.c:133206:3-133207:47
Marked with transfer function at sqlite/sqlite3.c:133786:7-133786:49
Marked with transfer function at sqlite/sqlite3.c:135279:5-135279:54
Marked with transfer function at sqlite/sqlite3.c:135366:5-135366:45
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:135478:9-135478:55
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:135407:9-135407:50
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:136085:3-136085:40
Marked with transfer function at sqlite/sqlite3.c:135386:5-135386:48
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:139331:7-139331:41
Marked with transfer function at sqlite/sqlite3.c:104840:7-104840:42
Marked with transfer function at sqlite/sqlite3.c:105390:7-105390:48
Marked with transfer function at sqlite/sqlite3.c:106550:5-106550:66
Marked with transfer function at sqlite/sqlite3.c:106692:7-106692:74
Marked with transfer function at sqlite/sqlite3.c:106609:9-106609:58
Marked with transfer function at sqlite/sqlite3.c:106790:9-106791:43
Marked with transfer function at sqlite/sqlite3.c:106782:9-106782:59
Marked with transfer function at sqlite/sqlite3.c:106227:9-106227:58
Marked with transfer function at sqlite/sqlite3.c:105454:7-105454:62
Marked with transfer function at sqlite/sqlite3.c:105920:9-105921:57
Marked with transfer function at sqlite/sqlite3.c:106387:3-106387:55
Marked with transfer function at sqlite/sqlite3.c:106321:7-106321:46
Marked with transfer function at sqlite/sqlite3.c:105899:9-105899:61
Marked with transfer function at sqlite/sqlite3.c:106481:11-106481:65
Marked with transfer function at sqlite/sqlite3.c:133206:3-133207:47
Marked with transfer function at sqlite/sqlite3.c:133786:7-133786:49
Marked with transfer function at sqlite/sqlite3.c:135279:5-135279:54
Marked with transfer function at sqlite/sqlite3.c:135366:5-135366:45
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:104840:7-104840:42
Marked with transfer function at sqlite/sqlite3.c:105390:7-105390:48
Marked with transfer function at sqlite/sqlite3.c:106550:5-106550:66
Marked with transfer function at sqlite/sqlite3.c:106692:7-106692:74
Marked with transfer function at sqlite/sqlite3.c:106609:9-106609:58
Marked with transfer function at sqlite/sqlite3.c:106790:9-106791:43
Marked with transfer function at sqlite/sqlite3.c:106782:9-106782:59
Marked with transfer function at sqlite/sqlite3.c:106227:9-106227:58
Marked with transfer function at sqlite/sqlite3.c:105454:7-105454:62
Marked with transfer function at sqlite/sqlite3.c:105920:9-105921:57
Marked with transfer function at sqlite/sqlite3.c:105593:9-105593:66
Marked with transfer function at sqlite/sqlite3.c:106387:3-106387:55
Marked with transfer function at sqlite/sqlite3.c:106321:7-106321:46
Marked with transfer function at sqlite/sqlite3.c:106361:5-106361:55
Marked with transfer function at sqlite/sqlite3.c:106661:7-106661:64
Marked with transfer function at sqlite/sqlite3.c:106609:9-106609:58
Marked with transfer function at sqlite/sqlite3.c:106790:9-106791:43
Marked with transfer function at sqlite/sqlite3.c:106782:9-106782:59
Marked with transfer function at sqlite/sqlite3.c:106910:5-106910:56
Marked with transfer function at sqlite/sqlite3.c:119822:7-119823:34
Marked with transfer function at sqlite/sqlite3.c:130754:13-130755:53
Marked with transfer function at sqlite/sqlite3.c:163234:2-163234:68
Marked with transfer function at sqlite/sqlite3.c:163869:7-163869:68
Marked with transfer function at sqlite/sqlite3.c:165165:5-165165:58
Marked with transfer function at sqlite/sqlite3.c:132359:5-132359:46
Marked with transfer function at sqlite/sqlite3.c:131770:5-131770:59
Marked with transfer function at sqlite/sqlite3.c:131864:3-131864:55
Marked with transfer function at sqlite/sqlite3.c:132073:5-132073:44
Marked with transfer function at sqlite/sqlite3.c:132099:5-132099:43
Marked with transfer function at sqlite/sqlite3.c:113312:8-113314:3
Marked with transfer function at sqlite/sqlite3.c:113377:3-113377:58
Marked with transfer function at sqlite/sqlite3.c:138121:7-138121:68
Marked with transfer function at sqlite/sqlite3.c:99520:5-99520:46
Marked with transfer function at sqlite/sqlite3.c:138391:3-138391:33
Marked with transfer function at sqlite/sqlite3.c:138476:3-138476:33
Marked with transfer function at sqlite/sqlite3.c:138953:3-138953:34
Marked with transfer function at sqlite/sqlite3.c:104840:7-104840:42
Marked with transfer function at sqlite/sqlite3.c:105390:7-105390:48
Marked with transfer function at sqlite/sqlite3.c:106550:5-106550:66
Marked with transfer function at sqlite/sqlite3.c:106692:7-106692:74
Marked with transfer function at sqlite/sqlite3.c:106609:9-106609:58
Marked with transfer function at sqlite/sqlite3.c:106790:9-106791:43
Marked with transfer function at sqlite/sqlite3.c:106782:9-106782:59
Marked with transfer function at sqlite/sqlite3.c:106227:9-106227:58
Marked with transfer function at sqlite/sqlite3.c:105454:7-105454:62
Marked with transfer function at sqlite/sqlite3.c:105920:9-105921:57
Marked with transfer function at sqlite/sqlite3.c:106387:3-106387:55
Marked with transfer function at sqlite/sqlite3.c:106321:7-106321:46
Marked with transfer function at sqlite/sqlite3.c:105899:9-105899:61
Marked with transfer function at sqlite/sqlite3.c:106481:11-106481:65
Marked with transfer function at sqlite/sqlite3.c:133206:3-133207:47
Marked with transfer function at sqlite/sqlite3.c:133786:7-133786:49
Marked with transfer function at sqlite/sqlite3.c:135279:5-135279:54
Marked with transfer function at sqlite/sqlite3.c:135366:5-135366:45
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:135407:9-135407:50
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:136085:3-136085:40
Marked with transfer function at sqlite/sqlite3.c:135386:5-135386:48
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:104840:7-104840:42
Marked with transfer function at sqlite/sqlite3.c:105390:7-105390:48
Marked with transfer function at sqlite/sqlite3.c:106550:5-106550:66
Marked with transfer function at sqlite/sqlite3.c:106692:7-106692:74
Marked with transfer function at sqlite/sqlite3.c:106609:9-106609:58
Marked with transfer function at sqlite/sqlite3.c:106790:9-106791:43
Marked with transfer function at sqlite/sqlite3.c:106782:9-106782:59
Marked with transfer function at sqlite/sqlite3.c:106227:9-106227:58
Marked with transfer function at sqlite/sqlite3.c:105454:7-105454:62
Marked with transfer function at sqlite/sqlite3.c:105920:9-105921:57
Marked with transfer function at sqlite/sqlite3.c:106387:3-106387:55
Marked with transfer function at sqlite/sqlite3.c:106321:7-106321:46
Marked with transfer function at sqlite/sqlite3.c:105899:9-105899:61
Marked with transfer function at sqlite/sqlite3.c:106481:11-106481:65
Marked with transfer function at sqlite/sqlite3.c:133206:3-133207:47
Marked with transfer function at sqlite/sqlite3.c:133786:7-133786:49
Marked with transfer function at sqlite/sqlite3.c:135279:5-135279:54
Marked with transfer function at sqlite/sqlite3.c:135366:5-135366:45
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:115576:7-115576:44
Marked with transfer function at sqlite/sqlite3.c:162284:3-162284:52
Marked with transfer function at sqlite/sqlite3.c:163869:7-163869:68
Marked with transfer function at sqlite/sqlite3.c:165165:5-165165:58
Marked with transfer function at sqlite/sqlite3.c:132359:5-132359:46
Marked with transfer function at sqlite/sqlite3.c:131770:5-131770:59
Marked with transfer function at sqlite/sqlite3.c:131864:3-131864:55
Marked with transfer function at sqlite/sqlite3.c:132073:5-132073:44
Marked with transfer function at sqlite/sqlite3.c:132099:5-132099:43
Marked with transfer function at sqlite/sqlite3.c:113312:8-113314:3
Marked with transfer function at sqlite/sqlite3.c:113377:3-113377:58
Marked with transfer function at sqlite/sqlite3.c:138121:7-138121:68
Marked with transfer function at sqlite/sqlite3.c:99520:5-99520:46
Marked with transfer function at sqlite/sqlite3.c:138391:3-138391:33
Marked with transfer function at sqlite/sqlite3.c:138476:3-138476:33
Marked with transfer function at sqlite/sqlite3.c:138953:3-138953:34
Marked with transfer function at sqlite/sqlite3.c:139331:7-139331:41
Marked with transfer function at sqlite/sqlite3.c:104840:7-104840:42
Marked with transfer function at sqlite/sqlite3.c:105390:7-105390:48
Marked with transfer function at sqlite/sqlite3.c:106550:5-106550:66
Marked with transfer function at sqlite/sqlite3.c:106692:7-106692:74
Marked with transfer function at sqlite/sqlite3.c:106609:9-106609:58
Marked with transfer function at sqlite/sqlite3.c:106790:9-106791:43
Marked with transfer function at sqlite/sqlite3.c:106782:9-106782:59
Marked with transfer function at sqlite/sqlite3.c:106227:9-106227:58
Marked with transfer function at sqlite/sqlite3.c:105454:7-105454:62
Marked with transfer function at sqlite/sqlite3.c:105920:9-105921:57
Marked with transfer function at sqlite/sqlite3.c:106387:3-106387:55
Marked with transfer function at sqlite/sqlite3.c:106321:7-106321:46
Marked with transfer function at sqlite/sqlite3.c:105899:9-105899:61
Marked with transfer function at sqlite/sqlite3.c:106481:11-106481:65
Marked with transfer function at sqlite/sqlite3.c:133206:3-133207:47
Marked with transfer function at sqlite/sqlite3.c:133786:7-133786:49
Marked with transfer function at sqlite/sqlite3.c:135279:5-135279:54
Marked with transfer function at sqlite/sqlite3.c:135366:5-135366:45
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:104840:7-104840:42
Marked with transfer function at sqlite/sqlite3.c:105390:7-105390:48
Marked with transfer function at sqlite/sqlite3.c:106550:5-106550:66
Marked with transfer function at sqlite/sqlite3.c:106692:7-106692:74
Marked with transfer function at sqlite/sqlite3.c:106609:9-106609:58
Marked with transfer function at sqlite/sqlite3.c:106790:9-106791:43
Marked with transfer function at sqlite/sqlite3.c:106782:9-106782:59
Marked with transfer function at sqlite/sqlite3.c:106227:9-106227:58
Marked with transfer function at sqlite/sqlite3.c:105454:7-105454:62
Marked with transfer function at sqlite/sqlite3.c:105920:9-105921:57
Marked with transfer function at sqlite/sqlite3.c:105593:9-105593:66
Marked with transfer function at sqlite/sqlite3.c:106387:3-106387:55
Marked with transfer function at sqlite/sqlite3.c:106321:7-106321:46
Marked with transfer function at sqlite/sqlite3.c:106361:5-106361:55
Marked with transfer function at sqlite/sqlite3.c:106661:7-106661:64
Marked with transfer function at sqlite/sqlite3.c:106609:9-106609:58
Marked with transfer function at sqlite/sqlite3.c:106790:9-106791:43
Marked with transfer function at sqlite/sqlite3.c:106782:9-106782:59
Marked with transfer function at sqlite/sqlite3.c:106910:5-106910:56
Marked with transfer function at sqlite/sqlite3.c:119822:7-119823:34
Marked with transfer function at sqlite/sqlite3.c:130754:13-130755:53
Marked with transfer function at sqlite/sqlite3.c:163234:2-163234:68
Marked with transfer function at sqlite/sqlite3.c:163869:7-163869:68
Marked with transfer function at sqlite/sqlite3.c:165165:5-165165:58
Marked with transfer function at sqlite/sqlite3.c:132359:5-132359:46
Marked with transfer function at sqlite/sqlite3.c:131770:5-131770:59
Marked with transfer function at sqlite/sqlite3.c:131864:3-131864:55
Marked with transfer function at sqlite/sqlite3.c:132073:5-132073:44
Marked with transfer function at sqlite/sqlite3.c:132099:5-132099:43
Marked with transfer function at sqlite/sqlite3.c:113312:8-113314:3
Marked with transfer function at sqlite/sqlite3.c:113377:3-113377:58
Marked with transfer function at sqlite/sqlite3.c:138121:7-138121:68
Marked with transfer function at sqlite/sqlite3.c:99520:5-99520:46
Marked with transfer function at sqlite/sqlite3.c:138391:3-138391:33
Marked with transfer function at sqlite/sqlite3.c:138476:3-138476:33
Marked with transfer function at sqlite/sqlite3.c:138953:3-138953:34
Marked with transfer function at sqlite/sqlite3.c:104840:7-104840:42
Marked with transfer function at sqlite/sqlite3.c:105390:7-105390:48
Marked with transfer function at sqlite/sqlite3.c:106550:5-106550:66
Marked with transfer function at sqlite/sqlite3.c:106692:7-106692:74
Marked with transfer function at sqlite/sqlite3.c:106609:9-106609:58
Marked with transfer function at sqlite/sqlite3.c:106790:9-106791:43
Marked with transfer function at sqlite/sqlite3.c:106782:9-106782:59
Marked with transfer function at sqlite/sqlite3.c:106227:9-106227:58
Marked with transfer function at sqlite/sqlite3.c:105454:7-105454:62
Marked with transfer function at sqlite/sqlite3.c:105920:9-105921:57
Marked with transfer function at sqlite/sqlite3.c:106387:3-106387:55
Marked with transfer function at sqlite/sqlite3.c:106321:7-106321:46
Marked with transfer function at sqlite/sqlite3.c:105899:9-105899:61
Marked with transfer function at sqlite/sqlite3.c:106387:3-106387:55
Marked with transfer function at sqlite/sqlite3.c:134960:7-134960:53
Marked with transfer function at sqlite/sqlite3.c:136055:3-136055:45
Marked with transfer function at sqlite/sqlite3.c:135386:5-135386:48
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:136085:3-136085:40
Marked with transfer function at sqlite/sqlite3.c:135386:5-135386:48
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:104840:7-104840:42
Marked with transfer function at sqlite/sqlite3.c:105390:7-105390:48
Marked with transfer function at sqlite/sqlite3.c:106550:5-106550:66
Marked with transfer function at sqlite/sqlite3.c:106692:7-106692:74
Marked with transfer function at sqlite/sqlite3.c:106609:9-106609:58
Marked with transfer function at sqlite/sqlite3.c:106790:9-106791:43
Marked with transfer function at sqlite/sqlite3.c:106782:9-106782:59
Marked with transfer function at sqlite/sqlite3.c:106227:9-106227:58
Marked with transfer function at sqlite/sqlite3.c:105454:7-105454:62
Marked with transfer function at sqlite/sqlite3.c:105920:9-105921:57
Marked with transfer function at sqlite/sqlite3.c:106387:3-106387:55
Marked with transfer function at sqlite/sqlite3.c:106321:7-106321:46
Marked with transfer function at sqlite/sqlite3.c:105899:9-105899:61
Marked with transfer function at sqlite/sqlite3.c:106481:11-106481:65
Marked with transfer function at sqlite/sqlite3.c:133206:3-133207:47
Marked with transfer function at sqlite/sqlite3.c:133786:7-133786:49
Marked with transfer function at sqlite/sqlite3.c:135279:5-135279:54
Marked with transfer function at sqlite/sqlite3.c:135366:5-135366:45
Marked with transfer function at sqlite/sqlite3.c:139141:5-139141:39
Marked with transfer function at sqlite/sqlite3.c:115576:7-115576:44
Marked with transfer function at sqlite/sqlite3.c:162284:3-162284:52
Marked with transfer function at sqlite/sqlite3.c:163869:7-163869:68
Marked with transfer function at sqlite/sqlite3.c:165165:5-165165:58
Marked with transfer function at sqlite/sqlite3.c:132359:5-132359:46
Marked with transfer function at sqlite/sqlite3.c:131770:5-131770:59
Marked with transfer function at sqlite/sqlite3.c:131864:3-131864:55
Marked with transfer function at sqlite/sqlite3.c:132073:5-132073:44
Marked with transfer function at sqlite/sqlite3.c:132099:5-132099:43
Marked with transfer function at sqlite/sqlite3.c:113312:8-113314:3
Marked with transfer function at sqlite/sqlite3.c:113377:3-113377:58
Marked with transfer function at sqlite/sqlite3.c:138121:7-138121:68
Marked with transfer function at sqlite/sqlite3.c:99520:5-99520:46
Marked with transfer function at sqlite/sqlite3.c:138391:3-138391:33
Marked with transfer function at sqlite/sqlite3.c:138476:3-138476:33
Marked with transfer function at sqlite/sqlite3.c:101178:5-101178:43
Marked with transfer function at sqlite/sqlite3.c:99520:5-99520:46
Marked with transfer function at sqlite/sqlite3.c:100697:9-100697:53
Marked with transfer function at sqlite/sqlite3.c:99382:5-99382:48
Marked with transfer function at sqlite/sqlite3.c:99410:3-99410:45
Marked with transfer function at sqlite/sqlite3.c:101457:3-101457:29
Marked with transfer function at sqlite/sqlite3.c:101198:9-101198:50
Marked with transfer function at sqlite/sqlite3.c:99520:5-99520:46
Marked with transfer function at sqlite/sqlite3.c:101544:3-101544:27
Marked with transfer function at sqlite/sqlite3.c:138478:3-138478:49
Marked with transfer function at sqlite/sqlite3.c:134868:3-134868:40
Marked with transfer function at sqlite/sqlite3.c:115849:5-115849:59
Marked with transfer function at sqlite/sqlite3.c:138137:13-138137:53
Marked with transfer function at sqlite/sqlite3.c:99520:5-99520:46
Marked with transfer function at sqlite/sqlite3.c:99485:11-99485:72
Marked with transfer function at sqlite/sqlite3.c:99522:9-99524:5
Marked with transfer function at sqlite/sqlite3.c:99393:13-99393:58
Marked with transfer function at sqlite/sqlite3.c:99386:11-99386:59
Marked with transfer function at sqlite/sqlite3.c:99410:3-99410:45
Marked with transfer function at sqlite/sqlite3.c:99422:11-99422:50
Marked with transfer function at sqlite/sqlite3.c:99445:7-99445:47
Marked with transfer function at sqlite/sqlite3.c:99522:9-99524:5
Marked with transfer function at sqlite/sqlite3.c:138391:3-138391:33
Marked with transfer function at sqlite/sqlite3.c:138476:3-138476:33
Marked with transfer function at sqlite/sqlite3.c:101178:5-101178:43
Marked with transfer function at sqlite/sqlite3.c:99520:5-99520:46
Marked with transfer function at sqlite/sqlite3.c:100697:9-100697:53
Marked with transfer function at sqlite/sqlite3.c:99382:5-99382:48
Marked with transfer function at sqlite/sqlite3.c:99410:3-99410:45
Marked with transfer function at sqlite/sqlite3.c:101457:3-101457:29
Marked with transfer function at sqlite/sqlite3.c:101595:8-101595:54
Marked with transfer function at sqlite/sqlite3.c:116897:5-116897:77
Marked with transfer function at sqlite/sqlite3.c:115193:5-115194:26
Marked with transfer function at sqlite/sqlite3.c:115444:5-115444:42
Marked with transfer function at sqlite/sqlite3.c:162279:3-162279:91
Marked with transfer function at sqlite/sqlite3.c:163869:7-163869:68
Marked with transfer function at sqlite/sqlite3.c:165165:5-165165:58
Marked with transfer function at sqlite/sqlite3.c:132359:5-132359:46
Marked with transfer function at sqlite/sqlite3.c:132434:5-132434:75
Marked with transfer function at sqlite/sqlite3.c:132519:3-132520:44
Marked with transfer function at sqlite/sqlite3.c:126746:5-126746:62
Marked with transfer function at sqlite/sqlite3.c:93194:3-93194:44
Marked with transfer function at sqlite/sqlite3.c:85219:5-85219:28
Marked with transfer function at sqlite/sqlite3.c:85276:11-85277:24
Marked with transfer function at sqlite/sqlite3.c:126760:7-126760:31
Marked with transfer function at sqlite/sqlite3.c:131998:7-131998:69
Marked with transfer function at sqlite/sqlite3.c:132073:5-132073:44
Marked with transfer function at sqlite/sqlite3.c:132099:5-132099:43
Marked with transfer function at sqlite/sqlite3.c:114095:9-114095:38
Marked with transfer function at sqlite/sqlite3.c:162254:4-162254:118
Marked with transfer function at sqlite/sqlite3.c:163869:7-163869:68
Marked with transfer function at sqlite/sqlite3.c:165165:5-165165:58
Marked with transfer function at sqlite/sqlite3.c:132359:5-132359:46
Marked with transfer function at sqlite/sqlite3.c:132434:5-132434:75
Marked with transfer function at sqlite/sqlite3.c:132519:3-132520:44
Marked with transfer function at sqlite/sqlite3.c:126746:5-126746:62
Marked with transfer function at sqlite/shell.c:15632:7-15632:41
Marked with transfer function at sqlite/shell.c:22203:5-22203:22
Raised at Goblint_lib__IntDomain.IntDomLifter.check_ikinds in file "src/cdomains/intDomain.ml", line 291, characters 52-292
Called from Goblint_lib__IntDomain.IntDomLifter.lift2 in file "src/cdomains/intDomain.ml", line 295, characters 21-37
Called from Goblint_lib__ValueDomain.Compound.meet in file "src/cdomains/valueDomain.ml", line 622, characters 31-44
Called from Goblint_lib__Lattice.ProdConf.op_scheme in file "src/domains/lattice.ml", line 427, characters 57-66
Called from Goblint_lib__ValueDomain.Compound.meet in file "src/cdomains/valueDomain.ml", line 628, characters 37-54
Called from Goblint_lib__MapDomain.PMap.long_map2.f in file "src/domains/mapDomain.ml", line 154, characters 33-43
Called from Stdlib__Map.Make.merge in file "map.ml", line 395, characters 44-63
Called from Stdlib__Map.Make.merge in file "map.ml", line 395, characters 64-79
Called from Goblint_lib__Lattice.LiftBot.meet in file "src/domains/lattice.ml", line 498, characters 40-55
Called from Goblint_lib__FlagHelper.FlagHelper.binop_to_t in file "src/domains/flagHelper.ml", line 27, characters 48-59
Called from Goblint_lib__ValueDomain.Compound.meet in file "src/cdomains/valueDomain.ml", line 627, characters 40-58
Called from Goblint_lib__Base.MainFunctor.set.(fun).update_one_addr in file "src/analyses/base.ml", line 1430, characters 24-57
Called from Stdlib__Map.Make.fold in file "map.ml", line 321, characters 19-42
Called from Goblint_lib__Base.MainFunctor.set.(fun) in file "src/analyses/base.ml", line 1508, characters 16-42
Called from Goblint_lib__Base.MainFunctor.invariant_fallback in file "src/analyses/base.ml", line 1696, characters 34-84
Called from Goblint_lib__Base.MainFunctor.invariant in file "src/analyses/base.ml", line 2121, characters 8-33
Called from Goblint_lib__Base.MainFunctor.branch.refine in file "src/analyses/base.ml", line 2236, characters 16-83
Called from Goblint_lib__MCP.MCP2.branch.f in file "src/analyses/mCP.ml", line 225, characters 17-35
Called from Goblint_lib__MCP.MCP2.map_deadcode.one_el in file "src/analyses/mCP.ml", line 100, characters 49-78
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from Goblint_lib__MCP.MCP2.map_deadcode in file "src/analyses/mCP.ml", line 101, characters 13-35
Called from Goblint_lib__MCP.MCP2.branch in file "src/analyses/mCP.ml", line 227, characters 15-52
Called from Goblint_lib__Constraints.WidenContextLifterSide.lift_fun in file "src/framework/constraints.ml", line 340, characters 25-41
Called from Goblint_lib__Constraints.PathSensitive2.map.h in file "src/framework/constraints.ml", line 1021, characters 16-36
Called from BatSet.Concrete.fold in file "src/batSet.ml", line 310, characters 35-56
Called from Goblint_lib__Constraints.PathSensitive2.map in file "src/framework/constraints.ml", line 1024, characters 12-43
Called from Goblint_lib__Constraints.DeadCodeLifter.lift_fun in file "src/framework/constraints.ml", line 410, characters 13-29
Called from Goblint_lib__Constraints.HashconsLifter.branch in file "src/framework/constraints.ml", line 55, characters 14-38
Called from Goblint_lib__Constraints.FromSpec.tf_test in file "src/framework/constraints.ml", line 586, characters 20-39
Called from Goblint_backtrace.protect in file "src/util/backtrace/goblint_backtrace.ml", line 29, characters 8-15
Re-raised at Goblint_backtrace.protect in file "src/util/backtrace/goblint_backtrace.ml", line 37, characters 4-50
Called from BatList.fold_left2 in file "src/batList.mlv", line 660, characters 39-54
Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15
Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52
Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28
Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 748, characters 27-47
Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 886, characters 4-105
Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15
Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52
Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 277, characters 14-39
Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 331, characters 46-59
Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 359, characters 18-36
Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25
Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 712, characters 15-25
Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15
Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52
Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28
Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 748, characters 27-47
Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 886, characters 4-105
Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15
Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52
Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 277, characters 14-39
Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 331, characters 46-59
Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 359, characters 18-36
Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25
Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 712, characters 15-25
Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15
Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52
Called from BatList.map.loop in file "src/batList.mlv", line 237, characters 28-33
Called from BatList.map in file "src/batList.mlv", line 240, characters 4-12
Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 748, characters 27-47
Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 886, characters 4-105
Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15
Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52
Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 277, characters 14-39
Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 331, characters 46-59
Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 359, characters 18-36

(abbreviated stack trace)

Goblint command:

./analyzer/goblint --conf ./analyzer/conf/custom/sqlite-ctx-sens-no-priv.json ./bench/scripts/incremental/benchmarking/result_efficiency/process0/sqlite/sqlite3.c ./bench/scripts/incremental/benchmarking/result_efficiency/process0/sqlite/sqlite3.h ./bench/scripts/incremental/benchmarking/result_efficiency/process0/sqlite/sqlite3ext.h ./bench/scripts/incremental/benchmarking/result_efficiency/process0/sqlite/shell.c -v --disable incremental.load --enable incremental.save

This is at sqlite commit cf9d36d1b3a84fb68d2e13acb790c449bff51c15.

[karoliineh]

analyzer/src/cdomain/value/cdomains/valueDomain.ml

Lines 502 to 507 in 5cd8650

	| TArray (ta, l, _) -> (* TODO, why is the length exp option? *)
	(* TODO handle casts between different sizes? *)
	Array (match v with
	| Array x -> x
	| _ -> log_top __POS__; CArrays.top ()
	)

By tracing a smaller example extracted from sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.i, it seems that this issue is caused by this todo about handling casts between different sizes.

[sim642]

Actually the TODO sounds like it's just about casts between different array sizes (e.g. int[2] and int[4]), but the incompatibility here is even worse: the array contents aren't being cast at all! In the benchmark, there's a cast (as part of union field access) from unsigned long long[1] to unsigned int[2]. And the IntDomain values in the array are never cast to the correct type.