Skip to content

Commit

Permalink
Fix indentation (PR #1040)
Browse files Browse the repository at this point in the history
  • Loading branch information
sim642 committed May 8, 2023
1 parent f9dc56a commit db4faa8
Showing 1 changed file with 9 additions and 9 deletions.
18 changes: 9 additions & 9 deletions src/analyses/basePriv.ml
Original file line number Diff line number Diff line change
Expand Up @@ -226,19 +226,19 @@ struct
else
CPA.find x st.cpa
(* let read_global ask getg cpa x =
let (cpa', v) as r = read_global ask getg cpa x in
ignore (Pretty.printf "READ GLOBAL %a (%a, %B) = %a\n" CilType.Varinfo.pretty x CilType.Location.pretty !Tracing.current_loc (is_unprotected ask x) VD.pretty v);
r *)
let (cpa', v) as r = read_global ask getg cpa x in
ignore (Pretty.printf "READ GLOBAL %a (%a, %B) = %a\n" CilType.Varinfo.pretty x CilType.Location.pretty !Tracing.current_loc (is_unprotected ask x) VD.pretty v);
r *)
let write_global ?(invariant=false) ask getg sideg (st: BaseComponents (D).t) x v =
let cpa' = CPA.add x v st.cpa in
if not invariant then
sideg (V.global x) (CPA.singleton x v);
(* Unlock after invariant will still side effect refined value from CPA, because cannot distinguish from non-invariant write. *)
{st with cpa = cpa'}
(* let write_global ask getg sideg cpa x v =
let cpa' = write_global ask getg sideg cpa x v in
ignore (Pretty.printf "WRITE GLOBAL %a %a = %a\n" CilType.Varinfo.pretty x VD.pretty v CPA.pretty cpa');
cpa' *)
let cpa' = write_global ask getg sideg cpa x v in
ignore (Pretty.printf "WRITE GLOBAL %a %a = %a\n" CilType.Varinfo.pretty x VD.pretty v CPA.pretty cpa');
cpa' *)

let lock ask getg (st: BaseComponents (D).t) m =
if Locksets.(not (Lockset.mem m (current_lockset ask))) then (
Expand Down Expand Up @@ -331,9 +331,9 @@ struct
);
{st with cpa = cpa'}
(* let write_global ask getg sideg cpa x v =
let cpa' = write_global ask getg sideg cpa x v in
ignore (Pretty.printf "WRITE GLOBAL %a %a = %a\n" CilType.Varinfo.pretty x VD.pretty v CPA.pretty cpa');
cpa' *)
let cpa' = write_global ask getg sideg cpa x v in
ignore (Pretty.printf "WRITE GLOBAL %a %a = %a\n" CilType.Varinfo.pretty x VD.pretty v CPA.pretty cpa');
cpa' *)

let lock (ask: Queries.ask) getg (st: BaseComponents (D).t) m =
if Locksets.(not (Lockset.mem m (current_lockset ask))) then (
Expand Down

0 comments on commit db4faa8

Please sign in to comment.