search

goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
184 stars 75 forks source link

Incompatible ikinds exception on svcomp22 reachsafety tests #751

Open MartinWehking opened 2 years ago

MartinWehking commented 2 years ago

The following tests fail:

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 commented 2 years ago

Thanks for flagging this!

michael-schwarz commented 2 years ago

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

jerhard commented 2 years ago

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

michael-schwarz commented 2 years ago

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

jerhard commented 2 years ago

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 commented 1 year ago

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 commented 6 months ago

https://github.com/goblint/analyzer/blob/5cd8650a2872341152f48a7d1cd20ac9fa0de994/src/cdomain/value/cdomains/valueDomain.ml#L502-L507

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 commented 6 months ago

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.

michael-schwarz commented 6 months ago

I don't think we should change the representation of the array here (there may be other pointers to the same array). Rather, when we read we need to check that the type we're using to read matches the one we expect the elements to have (c.f. https://github.com/goblint/analyzer/issues/582)

sim642 commented 6 months ago

Other pointers to the array are irrelevant at this point: nothing is being changed here, this logic already is part of reading in eval_offset. This is when you are reading from u32 when u64 was written (and the local state still does contain that):

union u {
  unsigned long long u64[1];
  unsigned int u32[2];
}