C-2PO: Thesis About a Weakly-Relational Pointer Analysis

conf/svcomp-c2po-no-maypointto.json

@@ -0,0 +1,152 @@
+{
+    "ana": {
+      "sv-comp": {
+        "enabled": true,
+        "functions": true
+      },
+      "int": {
+        "def_exc": true,
+        "enums": false,
+        "interval": true
+      },
+      "float": {
+        "interval": true
+      },
+      "activated": [
+        "base",
+        "threadid",
+        "threadflag",
+        "threadreturn",
+        "mallocWrapper",
+        "mutexEvents",
+        "mutex",
+        "access",
+        "race",
+        "escape",
+        "expRelation",
+        "mhp",
+        "assert",
+        "symb_locks",
+        "region",
+        "thread",
+        "threadJoins",
+        "c2po",
+        "startState",
+        "taintPartialContexts"
+      ],
+      "path_sens": [
+        "mutex",
+        "malloc_null",
+        "uninit",
+        "expsplit",
+        "activeSetjmp",
+        "memLeak",
+        "threadflag"
+      ],
+      "context": {
+        "widen": false
+      },
+      "malloc": {
+        "wrappers": [
+          "kmalloc",
+          "__kmalloc",
+          "usb_alloc_urb",
+          "__builtin_alloca",
+          "kzalloc",
+
+          "ldv_malloc",
+
+          "kzalloc_node",
+          "ldv_zalloc",
+          "kmalloc_array",
+          "kcalloc",
+
+          "ldv_xmalloc",
+          "ldv_xzalloc",
+          "ldv_calloc",
+          "ldv_kzalloc"
+        ]
+      },
+      "base": {
+        "arrays": {
+          "domain": "partitioned"
+        }
+      },
+      "race": {
+        "free": false,
+        "call": false
+      },
+      "c2po": {
+        "askbase": false
+      },
+      "autotune": {
+        "enabled": true,
+        "activated": [
+          "singleThreaded",
+          "mallocWrappers",
+          "noRecursiveIntervals",
+          "enums",
+          "congruence",
+          "octagon",
+          "wideningThresholds",
+          "loopUnrollHeuristic",
+          "memsafetySpecification",
+          "termination",
+          "tmpSpecialAnalysis"
+        ]
+      }
+    },
+    "exp": {
+      "region-offsets": true
+    },
+    "solver": "td3",
+    "sem": {
+      "unknown_function": {
+        "spawn": false,
+        "call": false
+      },
+      "int": {
+        "signed_overflow": "assume_none"
+      },
+      "null-pointer": {
+        "dereference": "assume_none"
+      }
+    },
+    "witness": {
+      "graphml": {
+        "enabled": true,
+        "id": "enumerate",
+        "unknown": false
+      },
+      "yaml": {
+        "enabled": true,
+        "format-version": "2.0",
+        "entry-types": [
+          "invariant_set"
+        ],
+        "invariant-types": [
+          "loop_invariant"
+        ]
+      },
+      "invariant": {
+        "loop-head": true,
+        "after-lock": false,
+        "other": false,
+        "accessed": false,
+        "exact": true,
+        "exclude-vars": [
+          "tmp\\(___[0-9]+\\)?",
+          "cond",
+          "RETURN",
+          "__\\(cil_\\)?tmp_?[0-9]*\\(_[0-9]+\\)?",
+          ".*____CPAchecker_TMP_[0-9]+",
+          "__VERIFIER_assert__cond",
+          "__ksymtab_.*",
+          "\\(ldv_state_variable\\|ldv_timer_state\\|ldv_timer_list\\|ldv_irq_\\(line_\\|data_\\)?[0-9]+\\|ldv_retval\\)_[0-9]+"
+        ]
+      }
+    },
+    "pre": {
+      "enabled": false
+    }
+  }

conf/svcomp-c2po1_join_nform.json

@@ -0,0 +1,154 @@
+{
+    "ana": {
+      "sv-comp": {
+        "enabled": true,
+        "functions": true
+      },
+      "int": {
+        "def_exc": true,
+        "enums": false,
+        "interval": true
+      },
+      "float": {
+        "interval": true
+      },
+      "activated": [
+        "base",
+        "threadid",
+        "threadflag",
+        "threadreturn",
+        "mallocWrapper",
+        "mutexEvents",
+        "mutex",
+        "access",
+        "race",
+        "escape",
+        "expRelation",
+        "mhp",
+        "assert",
+        "symb_locks",
+        "region",
+        "thread",
+        "threadJoins",
+        "c2po",
+        "startState",
+        "taintPartialContexts"
+      ],
+      "path_sens": [
+        "mutex",
+        "malloc_null",
+        "uninit",
+        "expsplit",
+        "activeSetjmp",
+        "memLeak",
+        "threadflag"
+      ],
+      "context": {
+        "widen": false
+      },
+      "malloc": {
+        "wrappers": [
+          "kmalloc",
+          "__kmalloc",
+          "usb_alloc_urb",
+          "__builtin_alloca",
+          "kzalloc",
+
+          "ldv_malloc",
+
+          "kzalloc_node",
+          "ldv_zalloc",
+          "kmalloc_array",
+          "kcalloc",
+
+          "ldv_xmalloc",
+          "ldv_xzalloc",
+          "ldv_calloc",
+          "ldv_kzalloc"
+        ]
+      },
+      "base": {
+        "arrays": {
+          "domain": "partitioned"
+        }
+      },
+      "race": {
+        "free": false,
+        "call": false
+      },
+      "autotune": {
+        "enabled": true,
+        "activated": [
+          "singleThreaded",
+          "mallocWrappers",
+          "noRecursiveIntervals",
+          "enums",
+          "congruence",
+          "octagon",
+          "wideningThresholds",
+          "loopUnrollHeuristic",
+          "memsafetySpecification",
+          "termination",
+          "tmpSpecialAnalysis"
+        ]
+      },
+      "c2po": {
+        "askbase": true,
+        "precise_join": true,
+        "normal_form": true
+      }
+    },
+    "exp": {
+      "region-offsets": true
+    },
+    "solver": "td3",
+    "sem": {
+      "unknown_function": {
+        "spawn": false,
+        "call": false
+      },
+      "int": {
+        "signed_overflow": "assume_none"
+      },
+      "null-pointer": {
+        "dereference": "assume_none"
+      }
+    },
+    "witness": {
+      "graphml": {
+        "enabled": true,
+        "id": "enumerate",
+        "unknown": false
+      },
+      "yaml": {
+        "enabled": true,
+        "format-version": "2.0",
+        "entry-types": [
+          "invariant_set"
+        ],
+        "invariant-types": [
+          "loop_invariant"
+        ]
+      },
+      "invariant": {
+        "loop-head": true,
+        "after-lock": false,
+        "other": false,
+        "accessed": false,
+        "exact": true,
+        "exclude-vars": [
+          "tmp\\(___[0-9]+\\)?",
+          "cond",
+          "RETURN",
+          "__\\(cil_\\)?tmp_?[0-9]*\\(_[0-9]+\\)?",
+          ".*____CPAchecker_TMP_[0-9]+",
+          "__VERIFIER_assert__cond",
+          "__ksymtab_.*",
+          "\\(ldv_state_variable\\|ldv_timer_state\\|ldv_timer_list\\|ldv_irq_\\(line_\\|data_\\)?[0-9]+\\|ldv_retval\\)_[0-9]+"
+        ]
+      }
+    },
+    "pre": {
+      "enabled": false
+    }
+  }