Skip to content

Commit 2812ce7

Browse files
Simplify some things in relationAnalysis
1 parent 0dd89ad commit 2812ce7

File tree

1 file changed

+9
-13
lines changed

1 file changed

+9
-13
lines changed

src/analyses/apron/relationAnalysis.apron.ml

Lines changed: 9 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -356,16 +356,14 @@ struct
356356
let st = man.local in
357357
let ask = Analyses.ask_of_man man in
358358
let new_rel =
359-
if RD.Tracked.type_tracked (Cilfacade.fundec_return_type f) then (
359+
if RD.Tracked.type_tracked (Cilfacade.fundec_return_type f) then
360360
let rel' = RD.add_vars st.rel [RV.return] in
361-
match e with
362-
| Some e ->
361+
Option.map_default (fun e ->
363362
assign_from_globals_wrapper ask man.global {st with rel = rel'} e (fun rel' e' ->
364363
RD.assign_exp ask rel' RV.return e' (no_overflow ask e)
365-
)
366-
| None ->
367-
rel' (* leaves V.return unconstrained *)
368-
)
364+
)
365+
) rel' e
366+
(* default value rel' leaves V.return unconstrained *)
369367
else
370368
RD.copy st.rel
371369
in
@@ -436,20 +434,18 @@ struct
436434

437435
let combine_assign man r fe f args fc fun_st (f_ask : Queries.ask) =
438436
let unify_st = man.local in
439-
if RD.Tracked.type_tracked (Cilfacade.fundec_return_type f) then (
440-
let unify_st' = match r with
441-
| Some lv ->
437+
if RD.Tracked.type_tracked (Cilfacade.fundec_return_type f) then
438+
let unify_st' = Option.map_default (fun lv ->
442439
let ask = Analyses.ask_of_man man in
443440
assign_to_global_wrapper ask man.global man.sideg unify_st lv (fun st v ->
444441
let rel = RD.assign_var st.rel (RV.local v) RV.return in
445442
assert_type_bounds ask rel v (* TODO: should be done in return instead *)
446443
)
447-
| None ->
448-
unify_st
444+
)
445+
unify_st r
449446
in
450447
RD.remove_vars_with unify_st'.rel [RV.return]; (* mutates! *)
451448
unify_st'
452-
)
453449
else
454450
unify_st
455451

0 commit comments

Comments
 (0)