From 125672acdb181f3fe26cdeec91f45ad110cc557d Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 18 Feb 2025 17:47:50 +0100 Subject: [PATCH] Use `Option.map_default` in a few cases --- src/analyses/apron/relationAnalysis.apron.ml | 22 +++++++------------- 1 file changed, 7 insertions(+), 15 deletions(-) diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index dec9a691c4..841fe15d6c 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -518,14 +518,10 @@ struct match desc.special args, f.vname with | Assert { exp; refine; _ }, _ -> assert_fn man exp refine | ThreadJoin { thread = id; ret_var = retvar }, _ -> - ( - (* Forget value that thread return is assigned to *) - let st' = forget_reachable man st [retvar] in - let st' = Priv.thread_join ask man.global id st' in - match r with - | Some lv -> invalidate_one ask man st' lv - | None -> st' - ) + (* Forget value that thread return is assigned to *) + let st' = forget_reachable man st [retvar] in + let st' = Priv.thread_join ask man.global id st' in + Option.map_default (invalidate_one ask man st') st' r | ThreadExit _, _ -> begin match ThreadId.get_current ask with | `Lifted tid -> @@ -540,11 +536,10 @@ struct let id = List.hd args in Priv.thread_join ~force:true ask man.global id st | Rand, _ -> - (match r with - | Some lv -> + Option.map_default (fun lv -> let st = invalidate_one ask man st lv in assert_fn {man with local = st} (BinOp (Ge, Lval lv, zero, intType)) true - | None -> st) + ) st r | _, _ -> let lvallist e = match ask.f (Queries.MayPointTo e) with @@ -572,10 +567,7 @@ struct let shallow_lvals = List.concat_map lvallist shallow_addrs in let st' = List.fold_left (invalidate_one ask man) st' shallow_lvals in (* invalidate lval if present *) - match r with - | Some lv -> invalidate_one ask man st' lv - | None -> st' - + Option.map_default (invalidate_one ask man st') st' r let query_invariant man context = let keep_local = GobConfig.get_bool "ana.relation.invariant.local" in