diff options
| author | Thomas Bauereiss | 2020-02-21 21:01:50 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2020-02-24 20:43:10 +0000 |
| commit | f75f4b66028305d77205fe0f8ef0aa78c8660ada (patch) | |
| tree | 490694e2536a8ff4896d1e6931c34d84d40e7fe4 /src | |
| parent | e37855c0c43b8369aefa91cfd17889452011b137 (diff) | |
Avoid generating assertions multiple times during typechecking
Diffstat (limited to 'src')
| -rw-r--r-- | src/nl_flow.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/nl_flow.ml b/src/nl_flow.ml index 24ef73fa..bf99f869 100644 --- a/src/nl_flow.ml +++ b/src/nl_flow.ml @@ -67,6 +67,11 @@ let rec returns (E_aux (aux, _)) = | E_block exps -> returns (List.hd (List.rev exps)) | _ -> false +let is_assert (E_aux (aux, _)) = + match aux with + | E_assert _ -> true + | _ -> false + let is_bitvector_literal (L_aux (aux, _)) = match aux with | L_bin _ | L_hex _ -> true @@ -120,7 +125,7 @@ let analyze' exps = | _ -> exps end | (E_aux (E_if (cond, then_exp, _), (l, _)) as exp) :: next :: rest - when returns then_exp -> + when returns then_exp && not (is_assert next) -> 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 |