diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml
index 984f42275..4dfe9705d 100644
--- a/infer/src/pulse/PulseAbductiveDomain.ml
+++ b/infer/src/pulse/PulseAbductiveDomain.ml
@@ -232,8 +232,12 @@ module AddressAttributes = struct
     BaseAddressAttributes.is_std_vector_reserved addr (astate.post :> base_domain).attrs
 
 
-  let is_end_iterator addr astate =
-    BaseAddressAttributes.is_end_iterator addr (astate.post :> base_domain).attrs
+  let mark_as_end_of_collection addr astate =
+    map_post_attrs astate ~f:(BaseAddressAttributes.mark_as_end_of_collection addr)
+
+
+  let is_end_of_collection addr astate =
+    BaseAddressAttributes.is_end_of_collection addr (astate.post :> base_domain).attrs
 
 
   let abduce_and_add value attrs astate =
diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli
index 06a74e820..eba41e6b1 100644
--- a/infer/src/pulse/PulseAbductiveDomain.mli
+++ b/infer/src/pulse/PulseAbductiveDomain.mli
@@ -133,7 +133,9 @@ module AddressAttributes : sig
 
   val get_closure_proc_name : AbstractValue.t -> t -> Procname.t option
 
-  val is_end_iterator : AbstractValue.t -> t -> bool
+  val is_end_of_collection : AbstractValue.t -> t -> bool
+
+  val mark_as_end_of_collection : AbstractValue.t -> t -> t
 
   val is_std_vector_reserved : AbstractValue.t -> t -> bool
 
diff --git a/infer/src/pulse/PulseAttribute.ml b/infer/src/pulse/PulseAttribute.ml
index ab52549d7..14e384671 100644
--- a/infer/src/pulse/PulseAttribute.ml
+++ b/infer/src/pulse/PulseAttribute.ml
@@ -30,6 +30,7 @@ module Attribute = struct
     | Allocated of Procname.t * Trace.t
     | Closure of Procname.t
     | DynamicType of Typ.Name.t
+    | EndOfCollection
     | Invalid of Invalidation.t * Trace.t
     | MustBeValid of Trace.t
     | StdVectorReserve
@@ -67,6 +68,8 @@ module Attribute = struct
 
   let dynamic_type_rank = Variants.to_rank (DynamicType (Typ.Name.Objc.from_string ""))
 
+  let end_of_collection_rank = Variants.to_rank EndOfCollection
+
   let pp f attribute =
     let pp_string_if_debug string fmt =
       if Config.debug_level_analysis >= 3 then F.pp_print_string fmt string
@@ -85,6 +88,8 @@ module Attribute = struct
         Procname.pp f pname
     | DynamicType typ ->
         F.fprintf f "DynamicType %a" Typ.Name.pp typ
+    | EndOfCollection ->
+        F.pp_print_string f "EndOfCollection"
     | Invalid (invalidation, trace) ->
         F.fprintf f "Invalid %a"
           (Trace.pp ~pp_immediate:(fun fmt -> Invalidation.pp fmt invalidation))
@@ -135,6 +140,10 @@ module Attributes = struct
            (var, loc, history) )
 
 
+  let is_end_of_collection attrs =
+    Set.find_rank attrs Attribute.end_of_collection_rank |> Option.is_some
+
+
   let is_std_vector_reserved attrs =
     Set.find_rank attrs Attribute.std_vector_reserve_rank |> Option.is_some
 
@@ -171,6 +180,7 @@ let is_suitable_for_pre = function
   | Allocated _
   | Closure _
   | DynamicType _
+  | EndOfCollection
   | Invalid _
   | StdVectorReserve
   | WrittenTo _ ->
@@ -190,5 +200,6 @@ let map_trace ~f = function
     | AddressOfStackVariable _
     | Closure _
     | DynamicType _
+    | EndOfCollection
     | StdVectorReserve ) as attr ->
       attr
diff --git a/infer/src/pulse/PulseAttribute.mli b/infer/src/pulse/PulseAttribute.mli
index 817f60bc8..87998f2b6 100644
--- a/infer/src/pulse/PulseAttribute.mli
+++ b/infer/src/pulse/PulseAttribute.mli
@@ -17,6 +17,7 @@ type t =
       (** the {!Procname.t} is the function causing the allocation, eg [malloc] *)
   | Closure of Procname.t
   | DynamicType of Typ.Name.t
+  | EndOfCollection
   | Invalid of Invalidation.t * Trace.t
   | MustBeValid of Trace.t
   | StdVectorReserve
@@ -41,6 +42,8 @@ module Attributes : sig
 
   val get_dynamic_type : t -> Typ.Name.t option
 
+  val is_end_of_collection : t -> bool
+
   val get_invalid : t -> (Invalidation.t * Trace.t) option
 
   val get_must_be_valid : t -> Trace.t option
diff --git a/infer/src/pulse/PulseBaseAddressAttributes.ml b/infer/src/pulse/PulseBaseAddressAttributes.ml
index 7152cce9d..f45e79bcf 100644
--- a/infer/src/pulse/PulseBaseAddressAttributes.ml
+++ b/infer/src/pulse/PulseBaseAddressAttributes.ml
@@ -72,6 +72,8 @@ let allocate procname (address, history) location memory =
 
 let add_dynamic_type typ address memory = add_one address (Attribute.DynamicType typ) memory
 
+let mark_as_end_of_collection address memory = add_one address Attribute.EndOfCollection memory
+
 let check_valid address attrs =
   L.d_printfln "Checking validity of %a" AbstractValue.pp address ;
   match Graph.find_opt address attrs |> Option.bind ~f:Attributes.get_invalid with
@@ -100,9 +102,8 @@ let get_must_be_valid = get_attribute Attributes.get_must_be_valid
 
 let std_vector_reserve address memory = add_one address Attribute.StdVectorReserve memory
 
-let is_end_iterator address attrs =
-  let invalid_attrs = get_attribute Attributes.get_invalid address attrs in
-  match invalid_attrs with Some (EndIterator, _) -> true | _ -> false
+let is_end_of_collection address attrs =
+  Graph.find_opt address attrs |> Option.value_map ~default:false ~f:Attributes.is_end_of_collection
 
 
 let is_std_vector_reserved address attrs =
diff --git a/infer/src/pulse/PulseBaseAddressAttributes.mli b/infer/src/pulse/PulseBaseAddressAttributes.mli
index 1e9073911..e524307f4 100644
--- a/infer/src/pulse/PulseBaseAddressAttributes.mli
+++ b/infer/src/pulse/PulseBaseAddressAttributes.mli
@@ -33,8 +33,6 @@ val check_valid : AbstractValue.t -> t -> (unit, Invalidation.t * Trace.t) resul
 
 val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t
 
-val is_end_iterator : AbstractValue.t -> t -> bool
-
 val get_closure_proc_name : AbstractValue.t -> t -> Procname.t option
 
 val get_must_be_valid : AbstractValue.t -> t -> Trace.t option
@@ -43,6 +41,10 @@ val std_vector_reserve : AbstractValue.t -> t -> t
 
 val is_std_vector_reserved : AbstractValue.t -> t -> bool
 
+val mark_as_end_of_collection : AbstractValue.t -> t -> t
+
+val is_end_of_collection : AbstractValue.t -> t -> bool
+
 val pp : F.formatter -> t -> unit
 
 val remove_allocation_attr : AbstractValue.t -> t -> t
diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml
index bac802581..011731ddd 100644
--- a/infer/src/pulse/PulseModels.ml
+++ b/infer/src/pulse/PulseModels.ml
@@ -20,6 +20,8 @@ type model =
   -> AbductiveDomain.t
   -> ExecutionDomain.t list PulseOperations.access_result
 
+let cpp_model_namespace = QualifiedCppName.of_list ["__infer_pulse_model"]
+
 module Misc = struct
   let shallow_copy location event ret_id dest_pointer_hist src_pointer_hist astate =
     let* astate, obj = PulseOperations.eval_access location src_pointer_hist Dereference astate in
@@ -151,11 +153,7 @@ module ObjC = struct
 end
 
 module FollyOptional = struct
-  let internal_value =
-    Fieldname.make
-      (Typ.CStruct (QualifiedCppName.of_list ["__infer_pulse_model"]))
-      "__infer_model_backing_value"
-
+  let internal_value = Fieldname.make (Typ.CStruct cpp_model_namespace) "backing_value"
 
   let internal_value_access = HilExp.Access.FieldAccess internal_value
 
@@ -472,11 +470,9 @@ module StdFunction = struct
 end
 
 module GenericArrayBackedCollection = struct
-  let field =
-    Fieldname.make
-      (Typ.CStruct (QualifiedCppName.of_list ["__infer_pulse_model"]))
-      "__infer_model_backing_array"
+  let field = Fieldname.make (Typ.CStruct cpp_model_namespace) "backing_array"
 
+  let last_field = Fieldname.make (Typ.CStruct cpp_model_namespace) "past_the_end"
 
   let access = HilExp.Access.FieldAccess field
 
@@ -491,14 +487,18 @@ module GenericArrayBackedCollection = struct
   let element location collection index astate =
     let* astate, internal_array = eval location collection astate in
     eval_element location internal_array index astate
+
+
+  let eval_pointer_to_last_element location collection astate =
+    let+ astate, pointer =
+      PulseOperations.eval_access location collection (FieldAccess last_field) astate
+    in
+    let astate = AddressAttributes.mark_as_end_of_collection (fst pointer) astate in
+    (astate, pointer)
 end
 
 module GenericArrayBackedCollectionIterator = struct
-  let internal_pointer =
-    Fieldname.make
-      (Typ.CStruct (QualifiedCppName.of_list ["__infer_pulse_model"]))
-      "__infer_model_backing_pointer"
-
+  let internal_pointer = Fieldname.make (Typ.CStruct cpp_model_namespace) "backing_pointer"
 
   let internal_pointer_access = HilExp.Access.FieldAccess internal_pointer
 
@@ -512,10 +512,25 @@ module GenericArrayBackedCollectionIterator = struct
     (astate, pointer, index)
 
 
-  let to_elem_pointed_by_iterator location iterator index astate =
+  let to_elem_pointed_by_iterator ?(step = None) location iterator astate =
+    let* astate, pointer = to_internal_pointer location iterator astate in
+    let* astate, index = PulseOperations.eval_access location pointer Dereference astate in
+    (* Check if not end iterator *)
+    let is_minus_minus = match step with Some `MinusMinus -> true | _ -> false in
+    let* astate =
+      if AddressAttributes.is_end_of_collection (fst pointer) astate && not is_minus_minus then
+        let invalidation_trace = Trace.Immediate {location; history= []} in
+        let access_trace = Trace.Immediate {location; history= snd pointer} in
+        Error
+          ( Diagnostic.AccessToInvalidAddress
+              {invalidation= EndIterator; invalidation_trace; access_trace}
+          , astate )
+      else Ok astate
+    in
     (* We do not want to create internal array if iterator pointer has an invalid value *)
     let* astate = PulseOperations.check_addr_access location index astate in
-    GenericArrayBackedCollection.element location iterator (fst index) astate
+    let+ astate, elem = GenericArrayBackedCollection.element location iterator (fst index) astate in
+    (astate, pointer, elem)
 
 
   let construct location event ~init ~ref astate =
@@ -564,8 +579,7 @@ module GenericArrayBackedCollectionIterator = struct
 
   let operator_star ~desc iter _ ~callee_procname:_ location ~ret astate =
     let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
-    let* astate, pointer, index = to_internal_pointer_deref location iter astate in
-    let+ astate, (elem, _) = to_elem_pointed_by_iterator location iter index astate in
+    let+ astate, pointer, (elem, _) = to_elem_pointed_by_iterator location iter astate in
     let astate = PulseOperations.write_id (fst ret) (elem, event :: snd pointer) astate in
     [ExecutionDomain.ContinueProgram astate]
 
@@ -573,15 +587,7 @@ module GenericArrayBackedCollectionIterator = struct
   let operator_step step ~desc iter _ ~callee_procname:_ location ~ret:_ astate =
     let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
     let index_new = AbstractValue.mk_fresh () in
-    let* astate, pointer, current_index = to_internal_pointer_deref location iter astate in
-    let* astate =
-      match (step, AddressAttributes.is_end_iterator (fst current_index) astate) with
-      | `MinusMinus, true ->
-          Ok astate
-      | _ ->
-          let* astate, _ = to_elem_pointed_by_iterator location iter current_index astate in
-          Ok astate
-    in
+    let* astate, pointer, _ = to_elem_pointed_by_iterator ~step:(Some step) location iter astate in
     PulseOperations.write_deref location ~ref:pointer ~obj:(index_new, event :: snd pointer) astate
     >>| ExecutionDomain.continue >>| List.return
 end
@@ -705,23 +711,20 @@ module StdVector = struct
   let vector_end vector iter : model =
    fun _ ~callee_procname:_ location ~ret:_ astate ->
     let event = ValueHistory.Call {f= Model "std::vector::end()"; location; in_call= []} in
-    let pointer_addr = AbstractValue.mk_fresh () in
+    let* astate, (arr_addr, _) = GenericArrayBackedCollection.eval location vector astate in
+    let* astate, (pointer_addr, _) =
+      GenericArrayBackedCollection.eval_pointer_to_last_element location vector astate
+    in
     let pointer_hist = event :: snd iter in
     let pointer_val = (pointer_addr, pointer_hist) in
-    let index_last = AbstractValue.mk_fresh () in
-    let* astate, (arr_addr, _) = GenericArrayBackedCollection.eval location vector astate in
     let* astate =
       PulseOperations.write_field location ~ref:iter GenericArrayBackedCollection.field
         ~obj:(arr_addr, pointer_hist) astate
     in
-    let* astate =
+    let+ astate =
       PulseOperations.write_field location ~ref:iter
         GenericArrayBackedCollectionIterator.internal_pointer ~obj:pointer_val astate
     in
-    let* astate =
-      PulseOperations.write_deref location ~ref:pointer_val ~obj:(index_last, pointer_hist) astate
-    in
-    let+ astate = PulseOperations.invalidate location EndIterator (index_last, []) astate in
     [ExecutionDomain.ContinueProgram astate]
 
 
diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp
index 5992c0ee3..19931d647 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp
+++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp
@@ -95,6 +95,7 @@ codetoanalyze/cpp/pulse/vector.cpp, push_back_loop_bad, 6, VECTOR_INVALIDATION,
 codetoanalyze/cpp/pulse/vector.cpp, reserve_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of reserve_bad,was potentially invalidated by `std::vector::reserve()`,use-after-lifetime part of the trace starts here,parameter `vec` of reserve_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/vector.cpp, shrink_to_fit_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of shrink_to_fit_bad,was potentially invalidated by `std::vector::shrink_to_fit()`,use-after-lifetime part of the trace starts here,parameter `vec` of shrink_to_fit_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_after_push_back_loop_bad, 9, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `iter_begin` declared here,passed as argument to `std::vector::begin()` (modelled),return from call to `std::vector::begin()` (modelled),passed as argument to `iterator constructor` (modelled),return from call to `iterator constructor` (modelled),invalid access occurs here]
+codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_end_next_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,is pointed to by the `end()` iterator,use-after-lifetime part of the trace starts here,variable `iter` declared here,passed as argument to `std::vector::end()` (modelled),return from call to `std::vector::end()` (modelled),invalid access occurs here]
 codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_end_read_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,is pointed to by the `end()` iterator,use-after-lifetime part of the trace starts here,variable `iter` declared here,passed as argument to `std::vector::end()` (modelled),return from call to `std::vector::end()` (modelled),invalid access occurs here]
 codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_next_after_emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of iterator_next_after_emplace_bad,was potentially invalidated by `std::vector::emplace()`,use-after-lifetime part of the trace starts here,variable `iter` declared here,passed as argument to `std::vector::begin()` (modelled),return from call to `std::vector::begin()` (modelled),invalid access occurs here]
 codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_next_after_emplace_loop_bad, 2, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of iterator_next_after_emplace_loop_bad,was potentially invalidated by `std::vector::emplace()`,use-after-lifetime part of the trace starts here,variable `iter` declared here,passed as argument to `std::vector::begin()` (modelled),return from call to `std::vector::begin()` (modelled),invalid access occurs here]
diff --git a/infer/tests/codetoanalyze/cpp/pulse/vector_iterator.cpp b/infer/tests/codetoanalyze/cpp/pulse/vector_iterator.cpp
index 03a5a0633..4e7955c3a 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/vector_iterator.cpp
+++ b/infer/tests/codetoanalyze/cpp/pulse/vector_iterator.cpp
@@ -71,6 +71,12 @@ void iterator_end_read_bad() {
   std::cout << *iter << '\n';
 }
 
+void iterator_end_next_bad() {
+  std::vector<int> vec = {1, 2};
+  auto iter = vec.end();
+  ++iter;
+}
+
 void iterator_end_prev_read_ok() {
   std::vector<int> vec = {1, 2};
   auto iter = vec.end();
@@ -107,3 +113,21 @@ void call_iterator_loop_ok(bool b) {
       return;
   }
 }
+
+std::vector<int>::iterator find(std::vector<int>& vec, bool b) {
+  for (auto it = vec.begin(); it != vec.end(); ++it) {
+    if (b) {
+      return it;
+    }
+  }
+  return vec.end();
+}
+
+void iterator_end_returned_ok(std::vector<int> vec, bool b) {
+  auto it = find(vec, b);
+  if (it != vec.end()) {
+    *it = 3;
+  } else {
+    return;
+  }
+}