[CCBM] Add semantics of assigning marker to local variable

Reviewed By: ezgicicek

Differential Revision: D22524050

fbshipit-source-id: f5f5e3895

infer/src/checkers/ConfigChecksBetweenMarkers.ml

@@ -132,15 +132,21 @@ module Mem = struct
       ~f:(fun v -> add (Loc.of_pvar pvar) v mem)
 
 
-  let store_constant id fn marker mem =
+  let store_constant e marker mem =
-    let marker = Marker.of_int_lit marker in
+    let marker = Marker.of_int_lit marker |> Val.of_marker in
-    let add_marker loc acc =
+    match (e : Exp.t) with
-      if Loc.is_this loc then add (Loc.of_this_field fn) (Val.of_marker marker) acc else acc
+    | Lfield (Var id, fn, _) ->
-    in
+        let add_marker loc acc =
-    let locs =
+          if Loc.is_this loc then add (Loc.of_this_field fn) marker acc else acc
-      find_opt (Loc.of_id id) mem |> Option.value_map ~default:Locs.bottom ~f:Val.get_locs
+        in
-    in
+        let locs =
-    Locs.fold add_marker locs mem
+          find_opt (Loc.of_id id) mem |> Option.value_map ~default:Locs.bottom ~f:Val.get_locs
+        in
+        Locs.fold add_marker locs mem
+    | Lvar pvar ->
+        add (Loc.of_pvar pvar) marker mem
+    | _ ->
+        mem
 end
 
 module Trace = struct
@@ -419,9 +425,7 @@ module Dom = struct
 
   let store_config pvar id ({mem} as astate) = {astate with mem= Mem.store pvar id mem}
 
-  let store_constant id fn marker ({mem} as astate) =
+  let store_constant e marker ({mem} as astate) = {astate with mem= Mem.store_constant e marker mem}
-    {astate with mem= Mem.store_constant id fn marker mem}
-
 
   let call_marker_start marker location ({context} as astate) =
     {astate with context= Context.call_marker_start marker location context}
@@ -566,8 +570,8 @@ module TransferFunctions = struct
             Dom.load_constant_config (Loc.of_pvar pvar) config astate )
     | Store {e1= Lvar pvar; e2= Exp.Var id} ->
         Dom.store_config pvar id astate
-    | Store {e1= Lfield (Var id, fn, _); e2= Const (Const.Cint marker)} ->
+    | Store {e1; e2= Const (Const.Cint marker)} ->
-        Dom.store_constant id fn marker astate
+        Dom.store_constant e1 marker astate
     | Call (_, Const (Cfun callee), _ :: (e, _) :: _, location, _)
       when FbGKInteraction.is_marker_start_java tenv callee ->
         get_marker_from_java_param e mem