Merge remote-tracking branch 'upstream/master'

Author: Philip Feniuk

goblint.opam

@@ -102,7 +102,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
   # published goblint-cil 2.0.6 is currently up-to-date, but pinned for reproducibility
-  [ "goblint-cil.2.0.6" "git+https://github.com/goblint/cil.git#c0b10d1848223a67de45ef608f4e05c082977ac1" ]
+  [ "goblint-cil.2.0.6" "git+https://github.com/goblint/cil.git#4b8b06eb39801a87d195f81d830a686578bd8b8b" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
   [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
 ]

goblint.opam.locked

@@ -143,7 +143,7 @@ post-messages: [
 pin-depends: [
   [
     "goblint-cil.2.0.6"
-    "git+https://github.com/goblint/cil.git#c0b10d1848223a67de45ef608f4e05c082977ac1"
+    "git+https://github.com/goblint/cil.git#4b8b06eb39801a87d195f81d830a686578bd8b8b"
   ]
   [
     "apron.v0.9.15"

goblint.opam.template

@@ -2,8 +2,7 @@
 # also remember to generate/adjust goblint.opam.locked!
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
-  # published goblint-cil 2.0.6 is currently up-to-date, but pinned for reproducibility
-  [ "goblint-cil.2.0.6" "git+https://github.com/goblint/cil.git#c0b10d1848223a67de45ef608f4e05c082977ac1" ]
+  [ "goblint-cil.2.0.6" "git+https://github.com/goblint/cil.git#4b8b06eb39801a87d195f81d830a686578bd8b8b" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
   [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
 ]

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

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/framework/analyses.ml

@@ -322,6 +322,12 @@ struct
   let should_print _ = false
 end
 
+module EmptyP =
+struct
+  include Printable.Empty
+  let of_elt _ = failwith "EmptyP.of_elt: analysis cannot be path-sensitive"
+end
+
 module UnitP =
 struct
   include Printable.Unit
@@ -339,7 +345,7 @@ module DefaultSpec =
 struct
   module G = Lattice.Unit
   module V = EmptyV
-  module P = UnitP
+  module P = EmptyP
 
   type marshal = unit
   let init _ = ()

src/goblint_lib.ml

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

src/solver/sideWPointSelect.ml

@@ -20,7 +20,7 @@ module type S =
     *)
     val create_data: (S.v -> bool) -> (S.v -> S.v -> unit) -> data
 
-    (** Notifies this strategy that a side-effect has occured.
+    (** Notifies this strategy that a side-effect has occurred.
         This allows the strategy to adapt its internal data structure.
         @param data The internal state of this strategy
         @param x    The optional source of the side-effect

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;
+}