Merge pull request #1791 from goblint/base_path_sens

Allow for path-sensitive base analysis

Author: michael-schwarz

src/analyses/base.ml

@@ -38,6 +38,7 @@ struct
   type t = Dom.t
   module D      = Dom
   include Analyses.ValueContexts(D)
+  module P = IdentityP(Dom)
 
   (* Two global invariants:
      1. Priv.V -> Priv.G  --  used for Priv

tests/regression/01-cpa/80-path.c

@@ -0,0 +1,20 @@
+//PARAM: --enable ana.int.interval --set ana.path_sens[+] base
+#include <stdio.h>
+#include <stdlib.h>
+#include <goblint.h>
+
+int main () {
+  int a;
+  int b;
+
+  int top;
+
+  if(top) {
+    a = 5; b = 5;
+  } else {
+    a = 10; b = 10;
+  }
+
+  __goblint_check(a == b); 
+  return 0;
+}