diff options
| author | Son HO | 2024-04-11 19:38:03 +0200 |
|---|---|---|
| committer | GitHub | 2024-04-11 19:38:03 +0200 |
| commit | 4fb9c9f655a9ffc3b4a1a717988311c057c9c599 (patch) | |
| tree | b44f8115822ac556b7023c114c8e893f22e5f552 /compiler | |
| parent | 87f3f68df0ae7ec010a7364762a1b852f0cac619 (diff) | |
| parent | 8894c310cd995f2f1f2abb1ca5232f98aa046274 (diff) | |
Merge pull request #121 from AeneasVerif/son/format
Reformat the code
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 15 |
1 files changed, 6 insertions, 9 deletions
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 444e5788..5f849230 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -157,9 +157,8 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config) const_generics = []; trait_refs = []; } ) -> - exec_assert __FILE__ __LINE__ - (ty_is_copyable ty) - meta "The type is not primitively copyable" + exec_assert __FILE__ __LINE__ (ty_is_copyable ty) meta + "The type is not primitively copyable" | _ -> exec_raise __FILE__ __LINE__ meta "Unreachable"); let ctx, fields = List.fold_left_map @@ -528,9 +527,8 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop) exec_assert __FILE__ __LINE__ (v1.ty = v2.ty) meta "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_copyable v1.ty) - meta "Type is not primitively copyable"; + exec_assert __FILE__ __LINE__ (ty_is_copyable v1.ty) meta + "Type is not primitively copyable"; let b = v1 = v2 in Ok { value = VLiteral (VBool b); ty = TLiteral TBool }) else @@ -621,9 +619,8 @@ let eval_binary_op_symbolic (config : config) (meta : Meta.meta) (binop : binop) (* Equality operations *) 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_copyable v1.ty) - meta "The type is not primitively copyable"; + exec_assert __FILE__ __LINE__ (ty_is_copyable v1.ty) meta + "The type is not primitively copyable"; TLiteral TBool) else (* Other operations: input types are integers *) |