diff options
| -rw-r--r-- | src/InterpreterExpressions.ml | 4 | ||||
| -rw-r--r-- | src/InterpreterPaths.ml | 2 | ||||
| -rw-r--r-- | src/Invariants.ml | 2 | ||||
| -rw-r--r-- | src/TypesUtils.ml | 4 | ||||
| -rw-r--r-- | src/ValuesUtils.ml | 2 |
5 files changed, 7 insertions, 7 deletions
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml index 2390aa48..f15c7558 100644 --- a/src/InterpreterExpressions.ml +++ b/src/InterpreterExpressions.ml @@ -267,7 +267,7 @@ let eval_binary_op_concrete (config : C.config) (ctx : C.eval_ctx) (* Equality operations *) assert (v1.ty = v2.ty); (* Equality/inequality check is primitive only for a subset of types *) - assert (type_is_primitively_copyable v1.ty); + assert (ty_is_primitively_copyable v1.ty); let b = v1 = v2 in Ok (ctx, { V.value = V.Concrete (Bool b); ty = T.Bool })) else @@ -344,7 +344,7 @@ let eval_binary_op_symbolic (config : C.config) (ctx : C.eval_ctx) (* Equality operations *) assert (v1.ty = v2.ty); (* Equality/inequality check is primitive only for a subset of types *) - assert (type_is_primitively_copyable v1.ty); + assert (ty_is_primitively_copyable v1.ty); T.Bool) else (* Other operations: input types are integers *) diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml index cf02fc23..c0d1c528 100644 --- a/src/InterpreterPaths.ml +++ b/src/InterpreterPaths.ml @@ -716,7 +716,7 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config) * Note that in the general case, copy is a trait: copying values * thus requires calling the proper function. Here, we copy values * for very simple types such as integers, shared borrows, etc. *) - assert (type_is_primitively_copyable (Subst.erase_regions sp.V.sv_ty)); + assert (ty_is_primitively_copyable (Subst.erase_regions sp.V.sv_ty)); (* If the type is copyable, we simply return the current value. Side * remark: what is important to look at when copying symbolic values * is symbolic expansion. The important subcase is the expansion of shared diff --git a/src/Invariants.ml b/src/Invariants.ml index 77b11136..5b77e13c 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -708,7 +708,7 @@ let check_symbolic_values (_config : C.config) (ctx : C.eval_ctx) : unit = let check_info _id info = assert (info.env_count = 0 || info.aproj_borrows = []); if ty_has_regions info.ty then assert (info.env_count <= 1); - assert (info.env_count <= 1 || type_is_primitively_copyable info.ty) + assert (info.env_count <= 1 || ty_is_primitively_copyable info.ty) in M.iter check_info !infos diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml index b0cd57c5..431ae8d8 100644 --- a/src/TypesUtils.ml +++ b/src/TypesUtils.ml @@ -140,10 +140,10 @@ let ty_has_regions_in_set (rset : RegionId.Set.t) (ty : rty) : bool = * require calling dedicated functions defined through the Copy trait. It * is the case for types like integers, shared borrows, etc. *) -let rec type_is_primitively_copyable (ty : 'r ty) : bool = +let rec ty_is_primitively_copyable (ty : 'r ty) : bool = match ty with | Adt ((AdtId _ | Assumed _), _, _) -> false - | Adt (Tuple, _, tys) -> List.for_all type_is_primitively_copyable tys + | Adt (Tuple, _, tys) -> List.for_all ty_is_primitively_copyable tys | TypeVar _ | Never | Str | Array _ | Slice _ -> false | Bool | Char | Integer _ -> true | Ref (_, _, Mut) -> false diff --git a/src/ValuesUtils.ml b/src/ValuesUtils.ml index 2d380ca9..4555fd50 100644 --- a/src/ValuesUtils.ml +++ b/src/ValuesUtils.ml @@ -97,7 +97,7 @@ let find_first_primitively_copyable_sv (v : typed_value) : symbolic_value option method! visit_Symbolic _ sv = let ty = sv.sv_ty in - if type_is_primitively_copyable ty && ty_has_regions ty then + if ty_is_primitively_copyable ty && ty_has_regions ty then raise (FoundSymbolicValue sv) else () end |