From 0f1389808ff3a848a9d6e6484df3f381860c7ddc Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Wed, 1 Nov 2023 17:14:03 +0200 Subject: [PATCH] Fix indentation --- src/analyses/apron/relationPriv.apron.ml | 22 +++++++++++----------- src/analyses/basePriv.ml | 22 +++++++++++----------- 2 files changed, 22 insertions(+), 22 deletions(-) diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index 3adfa272bb..2baf4cdca8 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -1011,17 +1011,17 @@ struct ) ) else ( - if ConcDomain.ThreadSet.is_top tids - then st - else - match ConcDomain.ThreadSet.elements tids with - | [tid] -> - let lmust',l' = G.thread (getg (V.thread tid)) in - {st with priv = (w, LMust.union lmust' lmust, L.join l l')} - | _ -> - (* To match the paper more closely, one would have to join in the non-definite case too *) - (* Given how we handle lmust (for initialization), doing this might actually be beneficial given that it grows lmust *) - st + if ConcDomain.ThreadSet.is_top tids then + st + else + match ConcDomain.ThreadSet.elements tids with + | [tid] -> + let lmust',l' = G.thread (getg (V.thread tid)) in + {st with priv = (w, LMust.union lmust' lmust, L.join l l')} + | _ -> + (* To match the paper more closely, one would have to join in the non-definite case too *) + (* Given how we handle lmust (for initialization), doing this might actually be beneficial given that it grows lmust *) + st ) let thread_return ask getg sideg tid (st: relation_components_t) = diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index ed6439a847..013a48a2d6 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -544,17 +544,17 @@ struct ) ) else ( - if (ConcDomain.ThreadSet.is_top tids) - then st - else - match ConcDomain.ThreadSet.elements tids with - | [tid] -> - let lmust',l' = G.thread (getg (V.thread tid)) in - {st with priv = (w, LMust.union lmust' lmust, L.join l l')} - | _ -> - (* To match the paper more closely, one would have to join in the non-definite case too *) - (* Given how we handle lmust (for initialization), doing this might actually be beneficial given that it grows lmust *) - st + if ConcDomain.ThreadSet.is_top tids then + st + else + match ConcDomain.ThreadSet.elements tids with + | [tid] -> + let lmust',l' = G.thread (getg (V.thread tid)) in + {st with priv = (w, LMust.union lmust' lmust, L.join l l')} + | _ -> + (* To match the paper more closely, one would have to join in the non-definite case too *) + (* Given how we handle lmust (for initialization), doing this might actually be beneficial given that it grows lmust *) + st ) let thread_return ask getg sideg tid (st: BaseComponents (D).t) =