summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGuillaume Boisseau2024-04-11 11:19:02 +0200
committerGitHub2024-04-11 11:19:02 +0200
commit87f3f68df0ae7ec010a7364762a1b852f0cac619 (patch)
tree722d3fad1c0cef926e40df16bd8645ce3b4abd20
parentdabbffde83e640aabc634d0a8917108decf9a5e7 (diff)
parent2f43c95253de73fce3207a7e6895f257b857f566 (diff)
Merge pull request #119 from AeneasVerif/generic-copy
Diffstat (limited to '')
-rw-r--r--compiler/InterpreterExpressions.ml10
-rw-r--r--compiler/Invariants.ml4
-rw-r--r--compiler/ValuesUtils.ml2
-rw-r--r--flake.lock6
4 files changed, 11 insertions, 11 deletions
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 48a1cce6..444e5788 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -146,7 +146,7 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
"Can't copy an assumed value other than Option"
| TAdt (TAdtId _, _) as ty ->
sanity_check __FILE__ __LINE__
- (allow_adt_copy || ty_is_primitively_copyable ty)
+ (allow_adt_copy || ty_is_copyable ty)
meta
| TAdt (TTuple, _) -> () (* Ok *)
| TAdt
@@ -158,7 +158,7 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
trait_refs = [];
} ) ->
exec_assert __FILE__ __LINE__
- (ty_is_primitively_copyable ty)
+ (ty_is_copyable ty)
meta "The type is not primitively copyable"
| _ -> exec_raise __FILE__ __LINE__ meta "Unreachable");
let ctx, fields =
@@ -195,7 +195,7 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
* thus requires calling the proper function. Here, we copy values
* for very simple types such as integers, shared borrows, etc. *)
cassert __FILE__ __LINE__
- (ty_is_primitively_copyable (Substitute.erase_regions sp.sv_ty))
+ (ty_is_copyable (Substitute.erase_regions sp.sv_ty))
meta "Not primitively copyable";
(* If the type is copyable, we simply return the current value. Side
* remark: what is important to look at when copying symbolic values
@@ -529,7 +529,7 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop)
"The arguments given to the binop don't have the same type";
(* Equality/inequality check is primitive only for a subset of types *)
exec_assert __FILE__ __LINE__
- (ty_is_primitively_copyable v1.ty)
+ (ty_is_copyable v1.ty)
meta "Type is not primitively copyable";
let b = v1 = v2 in
Ok { value = VLiteral (VBool b); ty = TLiteral TBool })
@@ -622,7 +622,7 @@ let eval_binary_op_symbolic (config : config) (meta : Meta.meta) (binop : binop)
sanity_check __FILE__ __LINE__ (v1.ty = v2.ty) meta;
(* Equality/inequality check is primitive only for a subset of types *)
exec_assert __FILE__ __LINE__
- (ty_is_primitively_copyable v1.ty)
+ (ty_is_copyable v1.ty)
meta "The type is not primitively copyable";
TLiteral TBool)
else
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 2ccf3ad4..689db0c4 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -825,9 +825,9 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit =
* it must be expanded first *)
if ty_has_borrows ctx.type_ctx.type_infos info.ty then
sanity_check __FILE__ __LINE__ (info.env_count <= 1) meta;
- (* A duplicated symbolic value is necessarily primitively copyable *)
+ (* A duplicated symbolic value is necessarily copyable *)
sanity_check __FILE__ __LINE__
- (info.env_count <= 1 || ty_is_primitively_copyable info.ty)
+ (info.env_count <= 1 || ty_is_copyable info.ty)
meta;
sanity_check __FILE__ __LINE__
diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml
index 91010e07..b6ee66f5 100644
--- a/compiler/ValuesUtils.ml
+++ b/compiler/ValuesUtils.ml
@@ -160,7 +160,7 @@ let find_first_primitively_copyable_sv_with_borrows
method! visit_VSymbolic _ sv =
let ty = sv.sv_ty in
- if ty_is_primitively_copyable ty && ty_has_borrows type_infos ty then
+ if ty_is_copyable ty && ty_has_borrows type_infos ty then
raise (FoundSymbolicValue sv)
else ()
end
diff --git a/flake.lock b/flake.lock
index 27a555ad..1eaf1375 100644
--- a/flake.lock
+++ b/flake.lock
@@ -8,11 +8,11 @@
"rust-overlay": "rust-overlay"
},
"locked": {
- "lastModified": 1712233083,
- "narHash": "sha256-KR4UwlgUzLWObSzQ1LIKITjRrYe4AuZXdvCK78qrip8=",
+ "lastModified": 1712825631,
+ "narHash": "sha256-YC0QArtso4Z9iBgd63FXHsSopMtWof0kC7ZrYpE6yzg=",
"owner": "aeneasverif",
"repo": "charon",
- "rev": "6e31313fdfd4830aa0fc795f6ab8b27600fcbbfb",
+ "rev": "657de2521c285401d706ec69d588bb5778b18109",
"type": "github"
},
"original": {