diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/nl_flow.ml | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/nl_flow.ml b/src/nl_flow.ml index 6196f23b..24ef73fa 100644 --- a/src/nl_flow.ml +++ b/src/nl_flow.ml @@ -60,6 +60,13 @@ let rec escapes (E_aux (aux, _)) = | E_block exps -> escapes (List.hd (List.rev exps)) | _ -> false +let rec returns (E_aux (aux, _)) = + match aux with + | E_return _ -> true + | E_block [] -> false + | E_block exps -> returns (List.hd (List.rev exps)) + | _ -> false + let is_bitvector_literal (L_aux (aux, _)) = match aux with | L_bin _ | L_hex _ -> true @@ -112,6 +119,12 @@ let analyze' exps = List.map (modify_unsigned id value) exps | _ -> exps end + | (E_aux (E_if (cond, then_exp, _), (l, _)) as exp) :: next :: rest + when returns then_exp -> + let msg = mk_lit_exp (L_string "") in + let not_cond = locate (fun _ -> gen_loc l) (mk_exp (E_app (mk_id "not_bool", [cond]))) in + let assertion = locate (fun _ -> gen_loc l) (mk_exp (E_assert (not_cond, msg))) in + exp :: assertion :: next :: rest | _ -> exps let analyze exps = |