diff --git a/src/plugins/eva/domains/cvalue/builtins_memory.ml b/src/plugins/eva/domains/cvalue/builtins_memory.ml index dc8645d225f1c589193e248a2f98772f4f28e95d..9815b35bd4fb161d1d392d41d416ebd1c8377a17 100644 --- a/src/plugins/eva/domains/cvalue/builtins_memory.ml +++ b/src/plugins/eva/domains/cvalue/builtins_memory.ml @@ -34,7 +34,7 @@ let dkey = Self.register_category "imprecision" let rec lval_of_address exp = match exp.node with | AddrOf lval -> lval - | CastE (_typ, exp) -> lval_of_address exp + | CastE (_typ, exp) when Cil.isPointerType exp.typ -> lval_of_address exp | _ -> Eva_ast.Build.mem exp let plevel = Parameters.ArrayPrecisionLevel.get