diff options
| author | Son Ho | 2024-02-08 09:42:00 +0100 |
|---|---|---|
| committer | Son Ho | 2024-03-17 04:53:07 +0100 |
| commit | 91d62c6e73cd67236848c3efa85f85ae152d0d4e (patch) | |
| tree | a79a50daf9bc23070cd168c985930e3e99f75aa4 /compiler/InterpreterExpressions.ml | |
| parent | c33a9807cf6aa21b2364449ee756ebf93de19eca (diff) | |
Update following changes in Charon
Diffstat (limited to 'compiler/InterpreterExpressions.ml')
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 8536b4ab..dc100fe3 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -263,8 +263,7 @@ let eval_operand_no_reorganize (config : config) (op : operand) match cv.value with | CLiteral lit -> cf (literal_to_typed_value (ty_as_literal cv.ty) lit) ctx - | CTraitConst (trait_ref, generics, const_name) -> ( - assert (generics = empty_generic_args); + | CTraitConst (trait_ref, const_name) -> ( match trait_ref.trait_id with | TraitImpl _ -> (* This shouldn't happen: if we refer to a concrete implementation, we @@ -294,8 +293,7 @@ let eval_operand_no_reorganize (config : config) (op : operand) ( ctx0, None, value_as_symbolic v.value, - SymbolicAst.VaTraitConstValue - (trait_ref, generics, const_name), + SymbolicAst.VaTraitConstValue (trait_ref, const_name), e )))) | CVar vid -> ( let ctx0 = ctx in |