diff --git a/backend/cn/lib/fulminate/executable_spec_internal.ml b/backend/cn/lib/fulminate/executable_spec_internal.ml
index 27e509924..391b3c663 100644
--- a/backend/cn/lib/fulminate/executable_spec_internal.ml
+++ b/backend/cn/lib/fulminate/executable_spec_internal.ml
@@ -8,6 +8,7 @@ module IT = IndexTerms
 module LRT = LogicalReturnTypes
 module LAT = LogicalArgumentTypes
 module AT = ArgumentTypes
+module OE = Ownership_exec
 
 type executable_spec =
   { pre_post : (CF.Symbol.sym * (string list * string list)) list;
@@ -87,7 +88,7 @@ let generate_c_pres_and_posts_internal
       ((pre_str, post_str), [])
     else (
       let fn_ownership_stats_opt, block_ownership_injs =
-        Ownership_exec.get_c_fn_local_ownership_checking_injs instrumentation.fn sigm
+        OE.get_c_fn_local_ownership_checking_injs instrumentation.fn sigm
       in
       match fn_ownership_stats_opt with
       | Some (entry_ownership_stats, exit_ownership_stats) ->
@@ -118,18 +119,21 @@ let generate_c_pres_and_posts_internal
         (modify_magic_comment_loc loc, generate_ail_stat_strs bs_and_ss))
       ail_executable_spec.in_stmt
   in
-  let return_injs =
-    List.filter_map
-      (fun (loc, e_opt, bs, ss) ->
-        match e_opt with Some e_opt' -> Some (loc, e_opt', bs, ss) | None -> None)
-      block_ownership_injs
+  let rec split_return_and_non_return_injs rs nrs = function
+    | [] -> (rs, nrs)
+    | (inj : OE.ownership_injection) :: injs ->
+      (match inj.injection_kind with
+       | OE.ReturnInj _ -> split_return_and_non_return_injs (inj :: rs) nrs injs
+       | NonReturnInj -> split_return_and_non_return_injs rs (inj :: nrs) injs)
   in
-  let non_return_injs =
-    List.filter (fun (_, e_opt, _, _) -> Option.is_none e_opt) block_ownership_injs
+  let return_injs, non_return_injs =
+    split_return_and_non_return_injs [] [] block_ownership_injs
   in
   let block_ownership_stmts =
     List.map
-      (fun (loc, _, bs, ss) -> (loc, generate_ail_stat_strs ~with_newline:true (bs, ss)))
+      (fun (ownership_inj : OE.ownership_injection) ->
+        ( ownership_inj.loc,
+          generate_ail_stat_strs ~with_newline:true ownership_inj.bs_and_ss ))
       non_return_injs
   in
   let block_ownership_stmts =
@@ -137,13 +141,26 @@ let generate_c_pres_and_posts_internal
   in
   let return_ownership_stmts =
     List.map
-      (fun (loc, e_opt, bs, ss) ->
-        (loc, e_opt, generate_ail_stat_strs ~with_newline:true (bs, ss)))
+      (fun (ownership_inj : OE.ownership_injection) ->
+        let return_kind =
+          match ownership_inj.injection_kind with
+          | OE.ReturnInj r -> r
+          | NonReturnInj ->
+            failwith
+              (__LOC__
+               ^ "Non-return injection should have been filtered out by this point")
+        in
+        let return_inj_expr_opt =
+          match return_kind with OE.ReturnExpr e -> Some e | ReturnVoid -> None
+        in
+        ( ownership_inj.loc,
+          return_inj_expr_opt,
+          generate_ail_stat_strs ~with_newline:true ownership_inj.bs_and_ss ))
       return_injs
   in
   let return_ownership_stmts =
     List.map
-      (fun (loc, e_opt, strs) -> (loc, e_opt, [ String.concat "\n" strs ]))
+      (fun (loc, e_opt, strs) -> (loc, (e_opt, [ String.concat "\n" strs ])))
       return_ownership_stmts
   in
   ( [ (instrumentation.fn, (pre_str, post_str)) ],
@@ -198,10 +215,10 @@ let generate_c_specs_internal
   in
   let specs = List.map generate_c_spec instrumentation_list in
   let pre_post, in_stmt, returns = Executable_spec_utils.list_split_three specs in
-  let returns =
-    List.map (fun (l, e_opt, strs) -> (l, (e_opt, strs))) (List.concat returns)
-  in
-  { pre_post = List.concat pre_post; in_stmt = List.concat in_stmt; returns }
+  { pre_post = List.concat pre_post;
+    in_stmt = List.concat in_stmt;
+    returns = List.concat returns
+  }
 
 
 let generate_doc_from_ail_struct ail_struct =
@@ -407,16 +424,12 @@ let generate_ownership_global_assignments
   | [] -> failwith "CN-exec: No main function so ownership globals cannot be initialised"
   | (main_sym, _) :: _ ->
     let globals = extract_global_variables prog5.globs in
-    let global_map_fcalls =
-      List.map Ownership_exec.generate_c_local_ownership_entry_fcall globals
-    in
+    let global_map_fcalls = List.map OE.generate_c_local_ownership_entry_fcall globals in
     let global_map_stmts_ = List.map (fun e -> A.AilSexpr e) global_map_fcalls in
-    let assignments = Ownership_exec.get_ownership_global_init_stats () in
+    let assignments = OE.get_ownership_global_init_stats () in
     let init_and_global_mapping_str =
       generate_ail_stat_strs ([], assignments @ global_map_stmts_)
     in
-    let global_unmapping_stmts_ =
-      List.map Ownership_exec.generate_c_local_ownership_exit globals
-    in
+    let global_unmapping_stmts_ = List.map OE.generate_c_local_ownership_exit globals in
     let global_unmapping_str = generate_ail_stat_strs ([], global_unmapping_stmts_) in
     [ (main_sym, (init_and_global_mapping_str, global_unmapping_str)) ]
diff --git a/backend/cn/lib/fulminate/executable_spec_internal.mli b/backend/cn/lib/fulminate/executable_spec_internal.mli
deleted file mode 100644
index bb79e4c5e..000000000
--- a/backend/cn/lib/fulminate/executable_spec_internal.mli
+++ /dev/null
@@ -1,125 +0,0 @@
-module CF = Cerb_frontend
-module CB = Cerb_backend
-module BT = BaseTypes
-module A = Cn_to_ail.A
-module IT = IndexTerms
-module LRT = LogicalReturnTypes
-module LAT = LogicalArgumentTypes
-module AT = ArgumentTypes
-
-type executable_spec =
-  { pre_post : (A.ail_identifier * (string list * string list)) list;
-    in_stmt : (Cerb_location.t * string list) list;
-    returns :
-      (Cerb_location.t * (CF.GenTypes.genTypeCategory A.expression option * string list))
-        list
-  }
-
-val doc_to_pretty_string : ?rfrac:float -> ?width:int -> PPrint.document -> string
-
-val generate_ail_stat_strs
-  :  ?with_newline:bool ->
-  Cn_to_ail.A.bindings * Cerb_frontend.GenTypes.genTypeCategory A.statement_ list ->
-  string list
-
-val extract_global_variables
-  :  ('a * 'b Mucore.globs) list ->
-  ('a * Cn_to_ail.C.ctype) list
-
-val generate_c_pres_and_posts_internal
-  :  bool ->
-  Executable_spec_extract.instrumentation ->
-  Cerb_frontend.GenTypes.genTypeCategory Cn_to_ail.A.sigma ->
-  unit Mucore.file ->
-  (Sym.t * (string list * string list)) list
-  * (Cerb_location.t * string list) list
-  * (Cerb_location.t
-    * Cerb_frontend.GenTypes.genTypeCategory Cn_to_ail.A.expression option
-    * string list)
-      list
-
-val generate_c_assume_pres_internal
-  :  Executable_spec_extract.instrumentation list ->
-  Cerb_frontend.GenTypes.genTypeCategory A.sigma ->
-  unit Mucore.file ->
-  (Cn_to_ail.A.sigma_declaration
-  * Cerb_frontend.GenTypes.genTypeCategory Cn_to_ail.A.sigma_function_definition)
-    list
-
-val generate_c_specs_internal
-  :  bool ->
-  Executable_spec_extract.instrumentation list ->
-  Cerb_frontend.GenTypes.genTypeCategory Cn_to_ail.A.sigma ->
-  unit Mucore.file ->
-  executable_spec
-
-val generate_doc_from_ail_struct
-  :  Sym.t
-     * (Cerb_location.t * Cerb_frontend.Annot.attributes * Cn_to_ail.C.tag_definition) ->
-  PPrint.document
-
-val generate_struct_decl_str : Sym.t * ('a * 'b * Cn_to_ail.C.tag_definition) -> string
-
-val generate_c_records
-  :  (Sym.t
-     * (Cerb_location.t * Cerb_frontend.Annot.attributes * Cn_to_ail.C.tag_definition))
-       list ->
-  string
-
-val generate_str_from_ail_struct
-  :  Sym.t
-     * (Cerb_location.t * Cerb_frontend.Annot.attributes * Cn_to_ail.C.tag_definition) ->
-  string
-
-val generate_str_from_ail_structs
-  :  (Sym.t
-     * (Cerb_location.t * Cerb_frontend.Annot.attributes * Cn_to_ail.C.tag_definition))
-       list ->
-  string
-
-val generate_c_datatypes
-  :  Cerb_frontend.GenTypes.genTypeCategory Cn_to_ail.A.sigma ->
-  (Cerb_location.t * string) list
-
-val generate_c_struct_strs
-  :  (Sym.t
-     * (Cerb_location.t * Cerb_frontend.Annot.attributes * Cn_to_ail.C.tag_definition))
-       list ->
-  string
-
-val generate_cn_versions_of_structs : Cn_to_ail.A.sigma_tag_definition list -> string
-
-val generate_fun_def_and_decl_docs
-  :  (Cn_to_ail.A.sigma_declaration
-     * Cerb_frontend.GenTypes.genTypeCategory Cn_to_ail.A.sigma_function_definition)
-       list ->
-  PPrint.document * PPrint.document
-
-val generate_c_functions
-  :  Cerb_frontend.GenTypes.genTypeCategory Cn_to_ail.A.sigma ->
-  (Sym.t * Definition.Function.t) list ->
-  string * string * Cerb_location.t list
-
-val remove_duplicates : ('a -> 'a -> bool) -> 'a list -> 'a list
-
-val generate_c_predicates
-  :  Cerb_frontend.GenTypes.genTypeCategory Cn_to_ail.A.sigma ->
-  (Sym.t * Definition.Predicate.t) list ->
-  string * string * Cerb_location.t list
-
-val generate_ownership_functions : bool -> Cn_to_ail.C.ctype list -> string * string
-
-val generate_conversion_and_equality_functions
-  :  Cerb_frontend.GenTypes.genTypeCategory Cn_to_ail.A.sigma ->
-  string * string
-
-val get_main
-  :  Cerb_frontend.GenTypes.genTypeCategory Cn_to_ail.A.sigma ->
-  Cerb_frontend.GenTypes.genTypeCategory Cn_to_ail.A.sigma_function_definition list
-
-val has_main : Cerb_frontend.GenTypes.genTypeCategory Cn_to_ail.A.sigma -> bool
-
-val generate_ownership_global_assignments
-  :  Cerb_frontend.GenTypes.genTypeCategory Cn_to_ail.A.sigma ->
-  unit Mucore.file ->
-  (Sym.t * (string list * string list)) list
diff --git a/backend/cn/lib/fulminate/ownership_exec.ml b/backend/cn/lib/fulminate/ownership_exec.ml
index 509c8949b..506630c36 100644
--- a/backend/cn/lib/fulminate/ownership_exec.ml
+++ b/backend/cn/lib/fulminate/ownership_exec.ml
@@ -3,6 +3,25 @@ open Executable_spec_utils
 module A = CF.AilSyntax
 module C = CF.Ctype
 
+type ail_bindings_and_statements =
+  A.bindings * CF.GenTypes.genTypeCategory A.statement_ list
+
+(* Differentiate between whether return statement carries an expression or not *)
+type return_kind =
+  | ReturnVoid
+  | ReturnExpr of CF.GenTypes.genTypeCategory A.expression
+
+(* Injections are treated differently depending on whether they involve returns or not *)
+type injection_kind =
+  | ReturnInj of return_kind
+  | NonReturnInj
+
+type ownership_injection =
+  { loc : Cerb_location.t;
+    bs_and_ss : ail_bindings_and_statements;
+    injection_kind : injection_kind
+  }
+
 let cn_ghost_state_sym = Sym.fresh_pretty "cn_ownership_global_ghost_state"
 
 let cn_ghost_state_struct_type =
@@ -166,9 +185,6 @@ let get_c_local_ownership_checking params =
 let rec collect_visibles bindings = function
   | [] -> []
   | A.(AnnotatedStatement (_, _, AilSdeclaration decls)) :: ss ->
-    (* Printf.printf "Bindings: \n" ; List.iter (fun (b_sym, _) -> Printf.printf "%s\n"
-       (Sym.pp_string b_sym)) bindings; Printf.printf "Decl syms: \n" ; List.iter (fun
-       (decl_sym, _) -> Printf.printf "%s\n" (Sym.pp_string decl_sym)) decls; *)
     let decl_syms_and_ctypes =
       List.map (fun (sym, _) -> (sym, find_ctype_from_bindings bindings sym)) decls
     in
@@ -192,6 +208,7 @@ let rec get_c_control_flow_block_unmaps_aux
   return_vars
   bindings
   A.(AnnotatedStatement (loc, _, s_))
+  : ownership_injection list
   =
   match s_ with
   | A.(AilSdeclaration _) -> []
@@ -231,19 +248,31 @@ let rec get_c_control_flow_block_unmaps_aux
     get_c_control_flow_block_unmaps_aux break_vars continue_vars return_vars bindings s
   | AilSgoto _ -> [] (* TODO *)
   | AilSreturnVoid ->
-    [ (loc, Some None, [], List.map generate_c_local_ownership_exit return_vars) ]
+    [ { loc;
+        bs_and_ss = ([], List.map generate_c_local_ownership_exit return_vars);
+        injection_kind = ReturnInj ReturnVoid
+      }
+    ]
   | AilSreturn e ->
-    [ (loc, Some (Some e), [], List.map generate_c_local_ownership_exit return_vars) ]
+    [ { loc;
+        bs_and_ss = ([], List.map generate_c_local_ownership_exit return_vars);
+        injection_kind = ReturnInj (ReturnExpr e)
+      }
+    ]
   | AilScontinue ->
     let loc_before_continue = get_start_loc loc in
-    [ ( loc_before_continue,
-        None,
-        [],
-        List.map generate_c_local_ownership_exit continue_vars )
+    [ { loc = loc_before_continue;
+        bs_and_ss = ([], List.map generate_c_local_ownership_exit continue_vars);
+        injection_kind = NonReturnInj
+      }
     ]
   | AilSbreak ->
     let loc_before_break = get_start_loc loc in
-    [ (loc_before_break, None, [], List.map generate_c_local_ownership_exit break_vars) ]
+    [ { loc = loc_before_break;
+        bs_and_ss = ([], List.map generate_c_local_ownership_exit break_vars);
+        injection_kind = NonReturnInj
+      }
+    ]
   | AilSskip | AilSexpr _ | AilSpar _ | AilSreg_store _ | AilSmarker _ -> []
 
 
@@ -293,31 +322,11 @@ let rec get_c_block_entry_exit_injs_aux bindings A.(AnnotatedStatement (loc, _,
     []
 
 
-let get_c_block_entry_exit_injs stat =
+let get_c_block_entry_exit_injs stat : ownership_injection list =
   let injs = get_c_block_entry_exit_injs_aux [] stat in
-  List.map (fun (loc, bs, ss) -> (loc, None, bs, ss)) injs
-
-
-let rec combine_injs_over_location loc = function
-  | [] -> []
-  | (loc', expr_opt, bs, inj_stmt) :: injs' ->
-    let stmt =
-      if
-        String.equal
-          (Cerb_location.location_to_string loc)
-          (Cerb_location.location_to_string loc')
-      then
-        [ (expr_opt, bs, inj_stmt) ]
-      else
-        []
-    in
-    stmt @ combine_injs_over_location loc injs'
-
-
-let rec get_return_expr_opt = function
-  | [] -> None
-  | Some e :: _ -> Some e
-  | None :: xs -> get_return_expr_opt xs
+  List.map
+    (fun (loc, bs, ss) -> { loc; bs_and_ss = (bs, ss); injection_kind = NonReturnInj })
+    injs
 
 
 let rec remove_duplicates ds = function
@@ -334,7 +343,6 @@ let rec remove_duplicates ds = function
       l :: remove_duplicates (l :: ds) ls
 
 
-(* TODO: Clean up this mess *)
 let get_c_block_local_ownership_checking_injs
   A.(AnnotatedStatement (_, _, fn_block) as statement)
   =
@@ -343,17 +351,40 @@ let get_c_block_local_ownership_checking_injs
     let injs = get_c_block_entry_exit_injs statement in
     let injs' = get_c_control_flow_block_unmaps statement in
     let injs = injs @ injs' in
-    let locs = List.map (fun (l, _, _, _) -> l) injs in
+    let locs = List.map (fun o_inj -> o_inj.loc) injs in
     let locs = remove_duplicates [] locs in
+    let rec combine_injs_over_location loc = function
+      | [] -> []
+      | inj :: injs' ->
+        if
+          String.equal
+            (Cerb_location.location_to_string loc)
+            (Cerb_location.location_to_string inj.loc)
+        then (
+          let bs, ss = inj.bs_and_ss in
+          (bs, ss, inj.injection_kind) :: combine_injs_over_location loc injs')
+        else
+          combine_injs_over_location loc injs'
+    in
+    (* If any of the individual injections to be combined is a return injection, the entire combined injection becomes a return injection *)
+    let rec get_return_inj_kind = function
+      | [] -> NonReturnInj
+      | ReturnInj r :: _ -> ReturnInj r
+      | NonReturnInj :: xs -> get_return_inj_kind xs
+    in
+    (* Injections at the same location need to be grouped together *)
     let combined_injs =
       List.map
         (fun l ->
           let injs' = combine_injs_over_location l injs in
-          let expr_opt_list, bs_list, stats_list =
+          let bs_list, ss_list, inj_kind_list =
             Executable_spec_utils.list_split_three injs'
           in
-          let return_expr_opt = get_return_expr_opt expr_opt_list in
-          (l, return_expr_opt, List.concat bs_list, List.concat stats_list))
+          let inj_kind = get_return_inj_kind inj_kind_list in
+          { loc = l;
+            bs_and_ss = (List.concat bs_list, List.concat ss_list);
+            injection_kind = inj_kind
+          })
         locs
     in
     combined_injs
@@ -376,7 +407,6 @@ let get_c_fn_local_ownership_checking_injs
     let param_types = List.map (fun (_, ctype, _) -> ctype) param_types in
     let params = List.combine param_syms param_types in
     let ownership_stats_pair = get_c_local_ownership_checking params in
-    (* TODO: Separate return injections here since they are now done differently *)
     let block_ownership_injs = get_c_block_local_ownership_checking_injs fn_body in
     (Some ownership_stats_pair, block_ownership_injs)
   | _, _ -> (None, [])
diff --git a/backend/cn/lib/fulminate/ownership_exec.mli b/backend/cn/lib/fulminate/ownership_exec.mli
index c6d5990dd..48fe8566c 100644
--- a/backend/cn/lib/fulminate/ownership_exec.mli
+++ b/backend/cn/lib/fulminate/ownership_exec.mli
@@ -2,6 +2,23 @@ module CF = Cerb_frontend
 module A = Executable_spec_utils.A
 module C = Executable_spec_utils.C
 
+type ail_bindings_and_statements =
+  A.bindings * CF.GenTypes.genTypeCategory A.statement_ list
+
+type return_kind =
+  | ReturnVoid
+  | ReturnExpr of CF.GenTypes.genTypeCategory A.expression
+
+type injection_kind =
+  | ReturnInj of return_kind
+  | NonReturnInj
+
+type ownership_injection =
+  { loc : Cerb_location.t;
+    bs_and_ss : ail_bindings_and_statements;
+    injection_kind : injection_kind
+  }
+
 val cn_ghost_state_sym : Sym.t
 
 val cn_ghost_state_struct_type : Executable_spec_utils.C.ctype
@@ -90,20 +107,12 @@ val get_c_control_flow_block_unmaps_aux
     * Executable_spec_utils.C.qualifiers
     * Executable_spec_utils.C.ctype))
     list ->
-  'a A.statement ->
-  (Cerb_location.t
-  * 'a A.expression option option
-  * 'b list
-  * Cerb_frontend.GenTypes.genTypeCategory A.statement_ list)
-    list
+  Cerb_frontend.GenTypes.genTypeCategory A.statement ->
+  ownership_injection list
 
 val get_c_control_flow_block_unmaps
-  :  'a A.statement ->
-  (Cerb_location.t
-  * 'a A.expression option option
-  * 'b list
-  * Cerb_frontend.GenTypes.genTypeCategory A.statement_ list)
-    list
+  :  Cerb_frontend.GenTypes.genTypeCategory A.statement ->
+  ownership_injection list
 
 val get_c_block_entry_exit_injs_aux
   :  A.bindings ->
@@ -120,23 +129,7 @@ val get_c_block_entry_exit_injs_aux
 
 val get_c_block_entry_exit_injs
   :  Cerb_frontend.GenTypes.genTypeCategory A.statement ->
-  (Cerb_location.t
-  * 'a option
-  * (Sym.t
-    * ((Cerb_location.t * Executable_spec_utils.A.storageDuration * bool)
-      * 'b option
-      * Executable_spec_utils.C.qualifiers
-      * Executable_spec_utils.C.ctype))
-      list
-  * Cerb_frontend.GenTypes.genTypeCategory A.statement_ list)
-    list
-
-val combine_injs_over_location
-  :  Cerb_location.t ->
-  (Cerb_location.t * 'a * 'b * 'c) list ->
-  ('a * 'b * 'c) list
-
-val get_return_expr_opt : 'a option list -> 'a option
+  ownership_injection list
 
 val remove_duplicates
   :  Cerb_location.t list ->
@@ -145,16 +138,7 @@ val remove_duplicates
 
 val get_c_block_local_ownership_checking_injs
   :  Cerb_frontend.GenTypes.genTypeCategory A.statement ->
-  (Cerb_location.t
-  * Cerb_frontend.GenTypes.genTypeCategory A.expression option option
-  * (Sym.t
-    * ((Cerb_location.t * Executable_spec_utils.A.storageDuration * bool)
-      * 'a option
-      * Executable_spec_utils.C.qualifiers
-      * Executable_spec_utils.C.ctype))
-      list
-  * Cerb_frontend.GenTypes.genTypeCategory A.statement_ list)
-    list
+  ownership_injection list
 
 val get_c_fn_local_ownership_checking_injs
   :  Sym.t ->
@@ -162,13 +146,4 @@ val get_c_fn_local_ownership_checking_injs
   (Cerb_frontend.GenTypes.genTypeCategory A.statement_ list
   * Cerb_frontend.GenTypes.genTypeCategory A.statement_ list)
     option
-  * (Cerb_location.t
-    * Cerb_frontend.GenTypes.genTypeCategory A.expression option option
-    * (Sym.t
-      * ((Cerb_location.t * Executable_spec_utils.A.storageDuration * bool)
-        * 'a option
-        * Executable_spec_utils.C.qualifiers
-        * Executable_spec_utils.C.ctype))
-        list
-    * Cerb_frontend.GenTypes.genTypeCategory A.statement_ list)
-      list
+  * ownership_injection list