diff options
| author | Brian Campbell | 2019-01-25 15:48:57 +0000 |
|---|---|---|
| committer | Brian Campbell | 2019-01-25 15:49:52 +0000 |
| commit | e3266e1ce5463d57f3d35c89dc811348f76c9e41 (patch) | |
| tree | dc6c8a56f3b48023134a9364f72d70c0e4d475d3 /src | |
| parent | c1e0bc6530bcc18d2c3798894b58855ed1231719 (diff) | |
Monomorphisation: update a built-in name
Diffstat (limited to 'src')
| -rw-r--r-- | src/monomorphise.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 4bb1876c..76a48cd7 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -3418,7 +3418,7 @@ let rec sets_from_assert e = match e with | E_app (Id_aux (Id "or_bool",_),[e1;e2]) -> aux e1 @ aux e2 - | E_app (Id_aux (Id "eq_atom",_), + | E_app (Id_aux (Id "eq_int",_), [E_aux (E_sizeof (Nexp_aux (Nexp_var kid,_)),_); E_aux (E_lit (L_aux (L_num i,_)),_)]) -> (check_kid kid; [i]) @@ -4034,7 +4034,7 @@ let rec extract_value_from_guard var (E_aux (e,_)) = match e with | E_app (op, ([E_aux (E_id var',_); E_aux (E_lit (L_aux (L_num i,_)),_)] | [E_aux (E_lit (L_aux (L_num i,_)),_); E_aux (E_id var',_)])) - when string_of_id op = "eq_atom" && Id.compare var var' == 0 -> + when string_of_id op = "eq_int" && Id.compare var var' == 0 -> Some i | E_app (op, [e1;e2]) when string_of_id op = "and_bool" -> (match extract_value_from_guard var e1 with @@ -4047,7 +4047,8 @@ let fill_in_type env typ = let subst = KidSet.fold (fun kid subst -> match Env.get_typ_var kid env with | K_type - | K_order -> subst + | K_order + | K_bool -> subst | K_int -> (match solve env (nvar kid) with | None -> subst @@ -4102,7 +4103,7 @@ let add_bitvector_casts (Defs defs) = | E_app (op, ([E_aux (E_sizeof (Nexp_aux (Nexp_var kid,_)),_); y] | [y; E_aux (E_sizeof (Nexp_aux (Nexp_var kid,_)),_)])) - when string_of_id op = "eq_atom" -> + when string_of_id op = "eq_int" -> (match destruct_atom_nexp (env_of y) (typ_of y) with | Some (Nexp_aux (Nexp_constant i,_)) -> [(kid,i)] | _ -> []) |