BranchSet analysis tracking set of taken branches

src/analyses/branchSet.ml

@@ -0,0 +1,40 @@
+(** Helper analysis to be path-sensitive in set of taken branches. *)
+
+open GoblintCil
+open Analyses
+
+module Spec =
+struct
+  include Analyses.IdentitySpec
+
+  module Branch = Printable.ProdSimple(BoolDomain.Bool)(Node)
+  module BranchSet = SetDomain.Make(Branch)
+
+  module D = BranchSet
+  include Analyses.ValueContexts(D)
+  module P = IdentityP (D)
+
+
+  let enter man (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
+    [man.local,man.local]
+
+  let combine_env man lval fexp f args fc au f_ask =
+    au
+
+  let combine_assign man (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
+    man.local
+
+
+  let branch man (exp:exp) (tv:bool) : D.t =
+    BranchSet.add (tv, man.node) man.local
+
+
+  let name () = "branchSet"
+
+  let startstate v = D.empty ()
+  let threadenter man ~multiple lval f args = [D.empty ()]
+  let exitstate  v = D.empty ()
+end
+
+let _ =
+  MCP.register_analysis (module Spec : MCPSpec)

src/config/options.schema.json

@@ -352,7 +352,7 @@
           "description": "List of path-sensitive analyses",
           "type": "array",
           "items": { "type": "string" },
-          "default": [ "mutex", "malloc_null", "uninit", "expsplit","activeSetjmp","memLeak" ]
+          "default": [ "mutex", "malloc_null", "uninit", "expsplit", "activeSetjmp", "memLeak", "branchSet"]
         },
         "ctx_insens": {
           "title": "ana.ctx_insens",

src/goblint_lib.ml

@@ -159,6 +159,7 @@ module Callstring = Callstring
 module LoopfreeCallstring = LoopfreeCallstring
 module Uninit = Uninit
 module Expsplit = Expsplit
+module BranchSet = BranchSet
 module StackTrace = StackTrace
 
 (** {2 Helper}

tests/regression/88-branchset/01-set.c

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