diff --git a/src/analyses/branchSet.ml b/src/analyses/branchSet.ml new file mode 100644 index 0000000000..a730c16221 --- /dev/null +++ b/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) diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 23a85e7045..74dfcd88cd 100644 --- a/src/config/options.schema.json +++ b/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", diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml index 5c83be6e3c..60dd07f68d 100644 --- a/src/goblint_lib.ml +++ b/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} diff --git a/tests/regression/88-branchset/01-set.c b/tests/regression/88-branchset/01-set.c new file mode 100644 index 0000000000..3b48af7805 --- /dev/null +++ b/tests/regression/88-branchset/01-set.c @@ -0,0 +1,25 @@ +//PARAM: --enable ana.int.interval --set ana.activated[+] branchSet +#include +#include +#include + +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; +}