diff --git a/bin/annot.ml b/bin/annot.ml
new file mode 100644
index 000000000..5424048fe
--- /dev/null
+++ b/bin/annot.ml
@@ -0,0 +1,661 @@
+(* Almost a copy of test.ml. Might be better to extract common parts. *)
+module CF = Cerb_frontend
+module CB = Cerb_backend
+open Cn
+
+let run_auto_annot
+      (* Common *)
+        filename
+      cc
+      macros
+      incl_dirs
+      incl_files
+      debug_level
+      print_level
+      csv_times
+      astprints
+      no_inherit_loc
+      magic_comment_char_dollar
+      allow_split_magic_comments
+      (* Executable spec *)
+        without_ownership_checking
+      (* without_loop_invariants *)
+      (* Test Generation *)
+        print_steps
+      output_dir
+      only
+      skip
+      dont_run
+      num_samples
+      max_backtracks
+      max_unfolds
+      max_array_length
+      build_tool
+      sanitizers
+      print_seed
+      input_timeout
+      null_in_every
+      seed
+      logging_level
+      trace_granularity
+      progress_level
+      until_timeout
+      exit_fast
+      max_stack_depth
+      _allowed_depth_failures
+      max_generator_size
+      sizing_strategy
+      random_size_splits
+      allowed_size_split_backtracks
+      _sized_null
+      coverage
+      disable_passes
+      trap
+      no_replays
+      no_replicas
+      output_tyche
+      inline_everything
+      experimental_struct_asgn_destruction
+      experimental_product_arg_destruction
+      experimental_learning
+      static_absint
+      smt_pruning_before_absinst
+      smt_pruning_after_absinst
+      smt_pruning_at_runtime
+      symbolic
+      symbolic_timeout
+      print_size_info
+      print_backtrack_info
+      print_satisfaction_info
+      print_discard_info
+  =
+  (* flags *)
+  Cerb_debug.debug_level := debug_level;
+  Pp.print_level := print_level;
+  Check.skip_and_only := (skip, only);
+  Sym.executable_spec_enabled := true;
+  let handle_error (e : TypeErrors.t) =
+    let report = TypeErrors.pp_message e.msg in
+    Pp.error e.loc report.short (Option.to_list report.descr);
+    match e.msg with TypeErrors.Unsupported _ -> exit 2 | _ -> exit 1
+  in
+  let filename = Common.there_can_only_be_one filename in
+  let output_dir =
+    Common.mk_dir_if_not_exist_maybe_tmp ~mktemp:true AutoAnnot output_dir
+  in
+  Pp.(debug 2 (lazy (item "Output directory" (string output_dir))));
+  let basefile = Filename.basename filename in
+  let pp_file = Filename.temp_file "cn_" basefile in
+  let out_file = Fulminate.get_instrumented_filename basefile in
+  let log_file = AutoAnnot.get_log_filename basefile in
+  (* Clear the log file if it already exists *)
+  (try
+     if Sys.file_exists log_file then (
+       let oc = open_out_gen [ Open_wronly; Open_creat; Open_trunc ] 0o644 log_file in
+       close_out oc)
+   with
+   | _ -> ());
+  AutoAnnot.log_filename := log_file;
+  Common.with_well_formedness_check (* CLI arguments *)
+    ~filename
+    ~cc
+    ~macros:(("__CN_TEST", None) :: ("__CN_INSTRUMENT", None) :: macros)
+    ~incl_dirs
+    ~incl_files
+    ~csv_times
+    ~coq_export_file:None
+    ~coq_mucore:false
+    ~coq_proof_log:false
+    ~coq_check_proof_log:false
+    ~astprints
+    ~no_inherit_loc
+    ~magic_comment_char_dollar
+    ~allow_split_magic_comments (* Callbacks *)
+    ~save_cpp:(Some pp_file)
+    ~disable_linemarkers:true
+    ~skip_label_inlining:true
+    ~handle_error
+    ~f:(fun ~cabs_tunit ~prog5 ~ail_prog ~statement_locs:_ ~paused ->
+      let config : TestGeneration.config =
+        { cc;
+          print_steps;
+          num_samples;
+          max_backtracks;
+          build_tool;
+          sanitizers;
+          inline_everything;
+          experimental_struct_asgn_destruction;
+          experimental_product_arg_destruction;
+          experimental_learning;
+          static_absint;
+          smt_pruning_before_absinst;
+          smt_pruning_after_absinst;
+          smt_pruning_at_runtime;
+          symbolic;
+          symbolic_timeout;
+          max_unfolds;
+          max_array_length;
+          print_seed;
+          input_timeout;
+          null_in_every;
+          seed;
+          logging_level;
+          trace_granularity;
+          progress_level;
+          until_timeout;
+          exit_fast;
+          max_stack_depth;
+          max_generator_size;
+          sizing_strategy;
+          random_size_splits;
+          allowed_size_split_backtracks;
+          coverage;
+          disable_passes;
+          trap;
+          no_replays;
+          no_replicas;
+          output_tyche;
+          print_size_info;
+          print_backtrack_info;
+          print_satisfaction_info;
+          print_discard_info;
+          with_auto_annot = true
+        }
+      in
+      TestGeneration.set_config config;
+      let _, sigma = ail_prog in
+      if
+        List.is_empty
+          (TestGeneration.functions_under_test
+             ~with_warning:true
+             cabs_tunit
+             sigma
+             prog5
+             paused)
+      then (
+        print_endline "No testable functions, trivially passing";
+        exit 0);
+      (* Enable additional instrumentations for auto-annot *)
+      Fulminate.Config.enable_auto_annot ();
+      Cerb_colour.do_colour := false;
+      (try
+         Fulminate.main
+           ~without_ownership_checking
+           ~without_loop_invariants:false
+           ~with_loop_leak_checks:true
+           ~with_testing:true
+           filename
+           cc
+           pp_file
+           out_file
+           output_dir
+           cabs_tunit
+           ail_prog
+           prog5
+       with
+       | e -> Common.handle_error_with_user_guidance ~label:"CN-Exec" e);
+      (try
+         TestGeneration.run
+           ~output_dir
+           ~filename
+           ~without_ownership_checking
+           build_tool
+           cabs_tunit
+           sigma
+           prog5
+           paused
+       with
+       | e -> Common.handle_error_with_user_guidance ~label:"CN-Test-Gen" e);
+      if not dont_run then (
+        Cerb_debug.maybe_close_csv_timing_file ();
+        Pp.(debug 10 (lazy (item "wait for auto-annotation" (string log_file))));
+        (* Run tests as a child process and wait, so we can continue afterwards *)
+        let status =
+          match build_tool with
+          | Bash ->
+            let prog = Filename.concat output_dir "run_tests.sh" in
+            let pid =
+              Unix.create_process prog [| prog |] Unix.stdin Unix.stdout Unix.stderr
+            in
+            snd (Unix.waitpid [] pid)
+          | Make ->
+            let pid =
+              Unix.create_process
+                "make"
+                [| "make"; "-C"; output_dir |]
+                Unix.stdin
+                Unix.stdout
+                Unix.stderr
+            in
+            snd (Unix.waitpid [] pid)
+        in
+        match status with
+        | Unix.WEXITED 0 -> AutoAnnot.run_autoannot (Filename.concat output_dir log_file)
+        | Unix.WEXITED n -> Pp.(debug 5 (lazy (item "Test runner exit code" (int n))))
+        | Unix.WSIGNALED n -> Pp.(debug 5 (lazy (item "Test runner signaled" (int n))))
+        | Unix.WSTOPPED n -> Pp.(debug 5 (lazy (item "Test runner stopped" (int n)))));
+      Result.ok ())
+
+
+open Cmdliner
+
+module Flags = struct
+  let print_steps =
+    let doc =
+      "Print successful stages, such as directory creation, compilation and linking."
+    in
+    Arg.(value & flag & info [ "print-steps" ] ~doc)
+
+
+  let output_dir =
+    let doc = "Place generated tests in the provided directory" in
+    Arg.(value & opt (some string) None & info [ "output-dir" ] ~docv:"DIR" ~doc)
+
+
+  let only =
+    let doc = "Only test this function (or comma-separated names)" in
+    Arg.(value & opt (list string) [] & info [ "only" ] ~doc)
+
+
+  let skip =
+    let doc = "Skip testing of this function (or comma-separated names)" in
+    Arg.(value & opt (list string) [] & info [ "skip" ] ~doc)
+
+
+  let dont_run =
+    let doc = "Do not run tests, only generate them" in
+    Arg.(value & flag & info [ "no-run" ] ~doc)
+
+
+  let gen_num_samples =
+    let doc = "Set the number of samples to test" in
+    Arg.(
+      value & opt int TestGeneration.default_cfg.num_samples & info [ "num-samples" ] ~doc)
+
+
+  let gen_backtrack_attempts =
+    let doc =
+      "Set the maximum attempts to satisfy a constraint before backtracking further, \
+       during input generation"
+    in
+    Arg.(
+      value
+      & opt int TestGeneration.default_cfg.max_backtracks
+      & info [ "max-backtrack-attempts" ] ~doc)
+
+
+  let gen_max_unfolds =
+    let doc = "Does nothing." in
+    let deprecated = "Will be removed after June 31." in
+    Arg.(value & opt (some int) None & info [ "max-unfolds" ] ~deprecated ~doc)
+
+
+  let max_array_length =
+    let doc = "Does nothing." in
+    let deprecated = "Will be removed after June 31." in
+    Arg.(value & opt int 0 & info [ "max-array-length" ] ~deprecated ~doc)
+
+
+  let build_tool =
+    let doc = "Set which build tool to use." in
+    Arg.(
+      value
+      & opt (enum TestGeneration.Options.build_tool) TestGeneration.default_cfg.build_tool
+      & info [ "build-tool" ] ~doc)
+
+
+  let sanitize =
+    let doc = "Forwarded to the '-fsanitize' argument of the C compiler" in
+    Arg.(
+      value
+      & opt (some string) (fst TestGeneration.default_cfg.sanitizers)
+      & info [ "sanitize" ] ~doc)
+
+
+  let no_sanitize =
+    let doc = "Forwarded to the '-fno-sanitize' argument of the C compiler" in
+    Arg.(
+      value
+      & opt (some string) (snd TestGeneration.default_cfg.sanitizers)
+      & info [ "no-sanitize" ] ~doc)
+
+
+  let print_seed =
+    let doc = "Print seed used by PRNG." in
+    Arg.(value & flag & info [ "print-seed" ] ~doc)
+
+
+  let input_timeout =
+    let doc = "Timeout for discarding a generation attempt (ms)" in
+    Arg.(
+      value
+      & opt (some int) TestGeneration.default_cfg.input_timeout
+      & info [ "input-timeout" ] ~doc)
+
+
+  let null_in_every =
+    let doc = "Set the likelihood of NULL being generated as 1 in every <n>" in
+    Arg.(
+      value
+      & opt (some int) TestGeneration.default_cfg.null_in_every
+      & info [ "null-in-every" ] ~doc)
+
+
+  let seed =
+    let doc = "Set the seed for random testing" in
+    Arg.(value & opt (some string) TestGeneration.default_cfg.seed & info [ "seed" ] ~doc)
+
+
+  let logging_level =
+    let doc = "Set the logging level for failing inputs from tests" in
+    Arg.(
+      value
+      & opt
+          (some (enum TestGeneration.Options.logging_level))
+          TestGeneration.default_cfg.logging_level
+      & info [ "logging-level" ] ~doc)
+
+
+  let trace_granularity =
+    let doc = "Set the trace granularity for failing inputs from tests" in
+    Arg.(
+      value
+      & opt
+          (some (enum TestGeneration.Options.trace_granularity))
+          TestGeneration.default_cfg.trace_granularity
+      & info [ "trace-granularity" ] ~doc)
+
+
+  let progress_level =
+    let doc = "Set the frequency of progress updates." in
+    Arg.(
+      value
+      & opt
+          (some (enum TestGeneration.Options.progress_level))
+          TestGeneration.default_cfg.progress_level
+      & info [ "progress-level" ] ~doc)
+
+
+  let until_timeout =
+    let doc =
+      "Keep rerunning tests until the given timeout (in seconds) has been reached"
+    in
+    Arg.(
+      value
+      & opt (some int) TestGeneration.default_cfg.until_timeout
+      & info [ "until-timeout" ] ~doc)
+
+
+  let exit_fast =
+    let doc = "Stop testing upon finding the first failure" in
+    Arg.(value & flag & info [ "exit-fast" ] ~doc)
+
+
+  let max_stack_depth =
+    let doc = "Maximum stack depth for generators" in
+    Arg.(
+      value
+      & opt (some int) TestGeneration.default_cfg.max_stack_depth
+      & info [ "max-stack-depth" ] ~doc)
+
+
+  let allowed_depth_failures =
+    let doc = "Does nothing." in
+    let deprecated = "Will be removed after July 31." in
+    Arg.(value & opt (some int) None & info [ "allowed-depth-failures" ] ~deprecated ~doc)
+
+
+  let max_generator_size =
+    let doc = "Maximum size for generated values" in
+    Arg.(
+      value
+      & opt (some int) TestGeneration.default_cfg.max_generator_size
+      & info [ "max-generator-size" ] ~doc)
+
+
+  let sizing_strategy =
+    let doc = "Strategy for deciding test case size." in
+    Arg.(
+      value
+      & opt
+          (some (enum TestGeneration.Options.sizing_strategy))
+          TestGeneration.default_cfg.sizing_strategy
+      & info [ "sizing-strategy" ] ~doc)
+
+
+  let random_size_splits =
+    let doc = "Randomly split sizes between recursive generator calls" in
+    Arg.(value & flag & info [ "random-size-splits" ] ~doc)
+
+
+  let allowed_size_split_backtracks =
+    let doc =
+      "Set the maximum attempts to split up a generator's size (between recursive calls) \
+       before backtracking further, during input generation"
+    in
+    Arg.(
+      value
+      & opt (some int) TestGeneration.default_cfg.allowed_size_split_backtracks
+      & info [ "allowed-size-split-backtracks" ] ~doc)
+
+
+  let sized_null =
+    let doc = "Does nothing." in
+    let deprecated = "Will be removed after July 31." in
+    Arg.(value & flag & info [ "sized-null" ] ~deprecated ~doc)
+
+
+  let coverage =
+    let doc = "(Experimental) Record coverage of tests via [lcov]" in
+    Arg.(value & flag & info [ "coverage" ] ~doc)
+
+
+  let disable_passes =
+    let doc = "skip this optimization pass (or comma-separated names)" in
+    Arg.(
+      value
+      & opt
+          (list
+             (enum
+                [ ("reorder", "reorder");
+                  ("picks", "picks");
+                  ("flatten", "flatten");
+                  ("consistency", "consistency");
+                  ("lift_constraints", "lift_constraints")
+                ]))
+          []
+      & info [ "disable" ] ~doc)
+
+
+  let trap =
+    let doc = "Raise SIGTRAP on test failure" in
+    Arg.(value & flag & info [ "trap" ] ~doc)
+
+
+  let no_replays =
+    let doc = "Disable replaying errors for error messages" in
+    Arg.(value & flag & info [ "no-replays" ] ~doc)
+
+
+  let no_replicas =
+    let doc = "Disable synthesizing C code to replicate bugs" in
+    Arg.(value & flag & info [ "no-replicas" ] ~doc)
+
+
+  let output_tyche =
+    let doc = "Enable output in Tyche format" in
+    Arg.(
+      value
+      & opt (some string) TestGeneration.default_cfg.output_tyche
+      & info [ "output-tyche" ] ~doc)
+
+
+  let inline_everything =
+    let doc = "Maximally inline everything" in
+    Arg.(value & flag & info [ "inline-everything" ] ~doc)
+
+
+  let experimental_struct_asgn_destruction =
+    let doc = "Destructs struct assignments" in
+    Arg.(value & flag & info [ "experimental-struct-asgn-destruction" ] ~doc)
+
+
+  let experimental_product_arg_destruction =
+    let doc = "Destructs all records and structs arguments" in
+    Arg.(value & flag & info [ "experimental-product-arg-destruction" ] ~doc)
+
+
+  let experimental_learning =
+    let doc = "Use experimental domain learning" in
+    Arg.(value & flag & info [ "experimental-learning" ] ~doc)
+
+
+  let smt_pruning_before_absinst =
+    let doc =
+      "(Experimental) Use SMT solver to prune unsatisfiable branches before abstract \
+       interpretation"
+    in
+    Arg.(
+      value
+      & opt (enum [ ("none", `None); ("fast", `Fast); ("slow", `Slow) ]) `None
+      & info [ "smt-pruning-before-absint" ] ~doc)
+
+
+  let smt_pruning_after_absinst =
+    let doc =
+      "(Experimental) Use SMT solver to prune unsatisfiable branches after abstract \
+       interpretation"
+    in
+    Arg.(
+      value
+      & opt (enum [ ("none", `None); ("fast", `Fast); ("slow", `Slow) ]) `None
+      & info [ "smt-pruning-after-absint" ] ~doc)
+
+
+  let smt_pruning_at_runtime =
+    let doc = "(Experimental) Use SMT solver to prune branches at runtime" in
+    Arg.(value & flag & info [ "smt-pruning-at-runtime" ] ~doc)
+
+
+  let static_absint =
+    let doc =
+      "(Experimental) Use static abstract interpretation with specified domain (or a \
+       comma-separated list). (e.g., 'interval', 'wrapped_interval')"
+    in
+    Arg.(
+      value
+      & opt
+          (list
+             (enum [ ("interval", "interval"); ("wrapped_interval", "wrapped_interval") ]))
+          []
+      & info [ "static-absint" ] ~docv:"DOMAIN" ~doc)
+
+
+  let print_size_info =
+    let doc = "(Experimental) Print size info" in
+    Arg.(value & flag & info [ "print-size-info" ] ~doc)
+
+
+  let print_backtrack_info =
+    let doc = "(Experimental) Print backtracking info" in
+    Arg.(value & flag & info [ "print-backtrack-info" ] ~doc)
+
+
+  let print_satisfaction_info =
+    let doc = "(Experimental) Print satisfaction info" in
+    Arg.(value & flag & info [ "print-satisfaction-info" ] ~doc)
+
+
+  let print_discard_info =
+    let doc = "(Experimental) Print discard info" in
+    Arg.(value & flag & info [ "print-discard-info" ] ~doc)
+
+
+  let symbolic =
+    let doc =
+      "(Experimental) Use symbolic execution for test generation instead of concrete \
+       value generation."
+    in
+    Arg.(value & flag & info [ "symbolic" ] ~doc)
+
+
+  let symbolic_timeout =
+    let doc = "Set timeout for SMT solver in symbolic mode (seconds)" in
+    Arg.(value & opt (some int) None & info [ "symbolic-timeout" ] ~doc)
+
+
+  let max_path_length =
+    let doc = "Set maximum symbolic path length for exploration" in
+    Arg.(value & opt (some int) None & info [ "max-path-length" ] ~doc)
+end
+
+let cmd =
+  let open Term in
+  let test_t =
+    const run_auto_annot
+    $ Common.Flags.file
+    $ Common.Flags.cc
+    $ Common.Flags.macros
+    $ Common.Flags.incl_dirs
+    $ Common.Flags.incl_files
+    $ Common.Flags.debug_level
+    $ Common.Flags.print_level
+    $ Common.Flags.csv_times
+    $ Common.Flags.astprints
+    $ Common.Flags.no_inherit_loc
+    $ Common.Flags.magic_comment_char_dollar
+    $ Common.Flags.allow_split_magic_comments
+    $ Instrument.Flags.without_ownership_checking
+    $ Flags.print_steps
+    $ Flags.output_dir
+    $ Flags.only
+    $ Flags.skip
+    $ Flags.dont_run
+    $ Flags.gen_num_samples
+    $ Flags.gen_backtrack_attempts
+    $ Flags.gen_max_unfolds
+    $ Flags.max_array_length
+    $ Flags.build_tool
+    $ Term.product Flags.sanitize Flags.no_sanitize
+    $ Flags.print_seed
+    $ Flags.input_timeout
+    $ Flags.null_in_every
+    $ Flags.seed
+    $ Flags.logging_level
+    $ Flags.trace_granularity
+    $ Flags.progress_level
+    $ Flags.until_timeout
+    $ Flags.exit_fast
+    $ Flags.max_stack_depth
+    $ Flags.allowed_depth_failures
+    $ Flags.max_generator_size
+    $ Flags.sizing_strategy
+    $ Flags.random_size_splits
+    $ Flags.allowed_size_split_backtracks
+    $ Flags.sized_null
+    $ Flags.coverage
+    $ Flags.disable_passes
+    $ Flags.trap
+    $ Flags.no_replays
+    $ Flags.no_replicas
+    $ Flags.output_tyche
+    $ Flags.inline_everything
+    $ Flags.experimental_struct_asgn_destruction
+    $ Flags.experimental_product_arg_destruction
+    $ Flags.experimental_learning
+    $ Flags.static_absint
+    $ Flags.smt_pruning_before_absinst
+    $ Flags.smt_pruning_after_absinst
+    $ Flags.smt_pruning_at_runtime
+    $ Flags.symbolic
+    $ Flags.symbolic_timeout
+    $ Flags.print_size_info
+    $ Flags.print_backtrack_info
+    $ Flags.print_satisfaction_info
+    $ Flags.print_discard_info
+  in
+  let doc =
+    "Generates proof annotations such as `unfold` and `focus` from testing executions."
+  in
+  let info = Cmd.info "auto-annot" ~doc in
+  Cmd.v info test_t
diff --git a/bin/common.ml b/bin/common.ml
index 8916cb9a2..0a7e67ae9 100644
--- a/bin/common.ml
+++ b/bin/common.ml
@@ -282,6 +282,7 @@ type subcommand =
   | Instrument
   | Test
   | SeqTest
+  | AutoAnnot
 
 let tool_name cmd =
   match cmd with
@@ -289,6 +290,7 @@ let tool_name cmd =
   | Instrument -> "Fulminate"
   | Test -> "Bennet"
   | SeqTest -> "CN-Seq-Test"
+  | AutoAnnot -> "AutoAnnot"
 
 
 open Cmdliner
diff --git a/bin/instrument.ml b/bin/instrument.ml
index eb9933f52..0d1dc393c 100644
--- a/bin/instrument.ml
+++ b/bin/instrument.ml
@@ -98,6 +98,7 @@ let generate_executable_specs
       experimental_ownership_stack_mode
       mktemp
       print_steps
+      with_auto_annot
   =
   (* flags *)
   Cerb_debug.debug_level := debug_level;
@@ -110,6 +111,7 @@ let generate_executable_specs
   Check.fail_fast := fail_fast;
   Diagnostics.diag_string := diag;
   Sym.executable_spec_enabled := true;
+  Fulminate.Config.with_auto_annot := with_auto_annot;
   let handle_error (e : TypeErrors.t) =
     let report = TypeErrors.pp_message e.msg in
     Pp.error e.loc report.short (Option.to_list report.descr);
@@ -271,6 +273,11 @@ module Flags = struct
        locations where ownership was taken for Fulminate-tracked memory"
     in
     Arg.(value & flag & info [ "ownership-stack-mode" ] ~doc)
+
+
+  let with_auto_annot =
+    let doc = "Instrument additional information for auto-annot (for debugging)" in
+    Arg.(value & flag & info [ "with-auto-annot" ] ~doc)
 end
 
 let cmd =
@@ -310,6 +317,7 @@ let cmd =
     $ Flags.experimental_ownership_stack_mode
     $ Flags.mktemp
     $ Flags.print_steps
+    $ Flags.with_auto_annot
   in
   let doc =
     "Instruments [FILE] with runtime C assertions that check the properties provided in \
diff --git a/bin/main.ml b/bin/main.ml
index af492c695..73f3479aa 100644
--- a/bin/main.ml
+++ b/bin/main.ml
@@ -1,6 +1,6 @@
 open Cmdliner
 
-let subcommands = [ Wf.cmd; Verify.cmd; Test.cmd; Instrument.cmd; SeqTest.cmd ]
+let subcommands = [ Wf.cmd; Verify.cmd; Test.cmd; Instrument.cmd; SeqTest.cmd; Annot.cmd ]
 
 let () =
   let version_str = Cn_version.git_version ^ " [" ^ Cn_version.git_version_date ^ "]" in
diff --git a/bin/test.ml b/bin/test.ml
index fdd26b2e2..dd0d85d9d 100644
--- a/bin/test.ml
+++ b/bin/test.ml
@@ -145,7 +145,8 @@ let run_tests
           print_size_info;
           print_backtrack_info;
           print_satisfaction_info;
-          print_discard_info
+          print_discard_info;
+          with_auto_annot = false
         }
       in
       TestGeneration.set_config config;
diff --git a/cn.opam b/cn.opam
index ce91c7ba3..2d0e01999 100644
--- a/cn.opam
+++ b/cn.opam
@@ -24,6 +24,7 @@ depends: [
   "ounit2" {with-test}
   "qcheck" {with-test}
   "qcheck-ounit" {with-test}
+  "z3"
 ]
 pin-depends: [
   ["cerberus-lib.dev" "git+https://github.com/rems-project/cerberus.git#9eb2ce2"]
diff --git a/lib/autoAnnot/autoAnnot.ml b/lib/autoAnnot/autoAnnot.ml
new file mode 100644
index 000000000..7aaba9fe7
--- /dev/null
+++ b/lib/autoAnnot/autoAnnot.ml
@@ -0,0 +1,213 @@
+module CF = Cerb_frontend
+module A = CF.AilSyntax
+
+let log_filename = ref "cn_auto_annot.log"
+
+let get_log_filename filename =
+  Filename.(remove_extension (basename filename)) ^ ".autoannot.log"
+
+
+type assignment =
+  { accessor : string;
+    value : int
+  }
+
+type focus =
+  { filename : string;
+    line : int;
+    kind : string;
+    ty : string;
+    (* TODO: should be int64 *)
+    target : int;
+    assignments : assignment list
+  }
+
+type annot = Focus of focus
+
+let print_focus_suggestion filename line kind ty w0 coeffs =
+  let pos = filename ^ ":" ^ string_of_int line in
+  let body =
+    List.filter_map
+      (fun (v, c) ->
+         match c with 0 -> None | 1 -> Some v | c -> Some (string_of_int c ^ " * " ^ v))
+      coeffs
+  in
+  let signature = Printf.sprintf "focus %s<%s>, " kind ty in
+  let elems = if w0 = 0 then body else string_of_int w0 :: body in
+  let sum = String.concat " + " elems in
+  let annotation = signature ^ sum in
+  Pp.progress_simple pos annotation
+
+
+let generate_focus_annot_aux filename line (kind, ty, assignments_list) : unit =
+  Pp.(
+    debug
+      10
+      (lazy
+        (item
+           "Generating annotations"
+           (string filename ^^ string ":" ^^ (line |> string_of_int |> string)))));
+  let _, first = List.hd assignments_list in
+  let variables =
+    first |> List.map (fun a -> a.accessor) |> List.sort_uniq String.compare
+  in
+  (* Sanity: all occurrences have the same variable set *)
+  let all_unique =
+    List.for_all
+      (fun x ->
+         List.fold_left
+           (fun acc y -> if String.equal x y then acc + 1 else acc)
+           0
+           variables
+         = 1)
+      variables
+  in
+  if not all_unique then
+    failwith "AutoAnnot: inconsistent environment";
+  (* Create a template *)
+  (* like ax + by + c = 0, and try to find a, b, and c *)
+  (* For [[x = 1; y = 2]; [ x = 2; y = 4]] *)
+  (* generate a * 1 + b * 2 + c = 0 /\ a * 2 + b * 4 + c = 0 *)
+  (* and find a, b, and c that satisfy the above using Z3 Optimize *)
+  let open Z3 in
+  let ctx = Z3.mk_context [ ("model", "true") ] in
+  let opt = Optimize.mk_opt ctx in
+  let i_k n = Arithmetic.Integer.mk_numeral_i ctx n in
+  let mk_int name = Arithmetic.Integer.mk_const_s ctx name in
+  let add = Arithmetic.mk_add ctx in
+  let mul x y = Arithmetic.mk_mul ctx [ x; y ] in
+  let neg x = Arithmetic.mk_unary_minus ctx x in
+  let ge = Arithmetic.mk_ge ctx in
+  let eq = Boolean.mk_eq ctx in
+  (* constant *)
+  let w0 = mk_int "w0" in
+  (* coefficients *)
+  let coeffs = List.map (fun v -> (v, mk_int ("w_" ^ v))) variables in
+  (* For each sample env, assert: w0 + sum(w_v * val_v) = 0 *)
+  let value_of v (env : assignment list) =
+    (List.find (fun a -> String.equal a.accessor v) env).value
+  in
+  let sum_terms env =
+    let terms = List.map (fun (v, wv) -> mul wv (i_k (value_of v env))) coeffs in
+    add (w0 :: terms)
+  in
+  List.iter
+    (fun (target, env) -> Optimize.add opt [ eq (sum_terms env) (i_k target) ])
+    assignments_list;
+  (* L1 norm: minimize t_v where t_v >= w_v and t_v >= -w_v*)
+  let ts =
+    List.map
+      (fun (v, wv) ->
+         let tv = mk_int ("t_" ^ v) in
+         Optimize.add opt [ ge tv wv; ge tv (neg wv) ];
+         tv)
+      coeffs
+  in
+  let objective = add ts in
+  ignore (Optimize.minimize opt objective : Optimize.handle);
+  (* Solve and read model *)
+  match Optimize.check opt with
+  | Solver.SATISFIABLE ->
+    let m = Optimize.get_model opt in
+    let get_int e =
+      let m = match m with Some m -> m | None -> failwith "No model found" in
+      match Model.eval m e true with
+      | None -> 0
+      | Some v -> int_of_string (Expr.to_string v)
+    in
+    let w0_v = get_int w0 in
+    let coeff_vals = List.map (fun (v, wv) -> (v, get_int wv)) coeffs in
+    print_focus_suggestion filename line kind ty w0_v coeff_vals
+  | Solver.UNSATISFIABLE | Solver.UNKNOWN ->
+    Pp.(
+      debug
+        5
+        (lazy
+          (item
+             "AutoAnnot: no relation found"
+             (string (filename ^ ":" ^ string_of_int line)))))
+
+
+let generate_focus_annot (annots : focus list) : unit =
+  let tbl : (string * int, string * string * (int * assignment list) list) Hashtbl.t =
+    Hashtbl.create 16
+  in
+  let add filename line assigns kind ty =
+    let key = (filename, line) in
+    let prev =
+      match Hashtbl.find_opt tbl key with
+      | Some (kind2, ty2, xs) when String.equal kind kind2 && String.equal ty ty2 -> xs
+      | Some _ -> failwith "inconsistent focus types"
+      | None -> []
+    in
+    Hashtbl.replace tbl key (kind, ty, prev @ [ assigns ])
+  in
+  List.iter
+    (function
+      | { filename; line; assignments; target; kind; ty } ->
+        add filename line (target, assignments) kind ty)
+    annots;
+  Hashtbl.iter
+    (fun (filename, line) assigns -> generate_focus_annot_aux filename line assigns)
+    tbl
+
+
+let parse (log_file : string) : annot list =
+  (* Open the file *)
+  let ic = open_in log_file in
+  let prefix = "[auto annot (focus)]" in
+  let split_and_trim ch s = String.split_on_char ch s |> List.map String.trim in
+  let parse_line (line : string) : annot =
+    if not (String.starts_with ~prefix line) then
+      failwith "ill-formed auto annot line";
+    let rest =
+      String.sub line (String.length prefix) (String.length line - String.length prefix)
+      |> String.trim
+    in
+    match split_and_trim ',' rest |> List.filter (fun s -> not (String.equal s "")) with
+    | [] -> failwith "ill-formed focus annotation"
+    | loc :: assigns_parts ->
+      (match split_and_trim ':' loc with
+       (* ex: itres.c:46:12-16:RW:signed int *)
+       | [ filename; line_str; _; kind; ty ] ->
+         (match int_of_string_opt line_str with
+          | None -> failwith "ill-formed line number"
+          | Some line ->
+            let assignments =
+              assigns_parts
+              |> List.map (fun p ->
+                match String.split_on_char '=' p |> List.map String.trim with
+                | [ key; vstr ] ->
+                  let v = int_of_string vstr in
+                  { accessor = key; value = v }
+                | _ -> failwith "ill-formed")
+            in
+            (* assignments must be non-empty; as the first element is the target*)
+            let fst = List.hd assignments in
+            assert (String.equal fst.accessor "!index");
+            let assignments = List.tl assignments in
+            Focus { filename; line; kind; ty; assignments; target = fst.value })
+       | _ -> failwith "ill-formed line")
+  in
+  let rec loop res =
+    match input_line ic with
+    | line ->
+      let res = parse_line line :: res in
+      loop res
+    | exception End_of_file -> res
+  in
+  let res =
+    try loop [] with
+    | e ->
+      close_in_noerr ic;
+      raise e
+  in
+  close_in ic;
+  res
+
+
+let run_autoannot (log_file : string) : unit =
+  Pp.print stdout (Pp.string "[Result of auto-annotation]");
+  let data = parse log_file in
+  let focus_annots = data |> List.filter_map (function Focus f -> Some f) in
+  generate_focus_annot focus_annots
diff --git a/lib/autoAnnot/autoAnnot.mli b/lib/autoAnnot/autoAnnot.mli
new file mode 100644
index 000000000..86e387b71
--- /dev/null
+++ b/lib/autoAnnot/autoAnnot.mli
@@ -0,0 +1,8 @@
+module CF = Cerb_frontend
+module A = CF.AilSyntax
+
+val log_filename : string ref
+
+val get_log_filename : string -> string
+
+val run_autoannot : string -> unit
diff --git a/lib/dune b/lib/dune
index 9b79569df..da781c008 100644
--- a/lib/dune
+++ b/lib/dune
@@ -14,6 +14,7 @@
   ppx_deriving_yojson.runtime
   result
   str
+  z3
   unix
   yojson)
  (preprocess
diff --git a/lib/fulminate/cn_to_ail.ml b/lib/fulminate/cn_to_ail.ml
index 954ca26ff..16f5d851e 100644
--- a/lib/fulminate/cn_to_ail.ml
+++ b/lib/fulminate/cn_to_ail.ml
@@ -2835,11 +2835,8 @@ let cn_to_ail_struct ((sym, (loc, attrs, tag_def)) : A.sigma_tag_definition)
   | C.UnionDef _ -> []
 
 
-let get_while_bounds_and_cond (i_sym, i_bt) it =
-  (* Translation of q.pointer *)
-  let i_it = IT.IT (IT.(Sym i_sym), i_bt, Cerb_location.unknown) in
-  (* Start of range *)
-  let start_expr =
+let get_range_from_it (i_sym, i_bt) it =
+  let lb =
     if BT.equal_sign (fst (Option.get (BT.is_bits_bt i_bt))) BT.Unsigned then
       IndexTerms.Bounds.get_lower_bound (i_sym, i_bt) it
     else (
@@ -2857,21 +2854,7 @@ let get_while_bounds_and_cond (i_sym, i_bt) it =
           ();
         exit 2)
   in
-  let start_expr =
-    IT.IT
-      ( IT.Cast (IT.get_bt start_expr, start_expr),
-        IT.get_bt start_expr,
-        Cerb_location.unknown )
-  in
-  let start_cond =
-    match start_expr with
-    | IT (Binop (Add, start_expr', IT (Const (Bits (_, n)), _, _)), _, _)
-      when Z.equal n Z.one ->
-      IT.lt_ (start_expr', i_it) Cerb_location.unknown
-    | _ -> IT.le_ (start_expr, i_it) Cerb_location.unknown
-  in
-  (* End of range *)
-  let end_expr =
+  let ub =
     match IndexTerms.Bounds.get_upper_bound_opt (i_sym, i_bt) it with
     | Some e -> e
     | None ->
@@ -2886,6 +2869,28 @@ let get_while_bounds_and_cond (i_sym, i_bt) it =
         ();
       exit 2
   in
+  (lb, ub)
+
+
+let get_while_bounds_and_cond (i_sym, i_bt) it =
+  (* Translation of q.pointer *)
+  let i_it = IT.IT (IT.(Sym i_sym), i_bt, Cerb_location.unknown) in
+  (* Start of range *)
+  let start_expr, end_expr = get_range_from_it (i_sym, i_bt) it in
+  let start_expr =
+    IT.IT
+      ( IT.Cast (IT.get_bt start_expr, start_expr),
+        IT.get_bt start_expr,
+        Cerb_location.unknown )
+  in
+  let start_cond =
+    match start_expr with
+    | IT (Binop (Add, start_expr', IT (Const (Bits (_, n)), _, _)), _, _)
+      when Z.equal n Z.one ->
+      IT.lt_ (start_expr', i_it) Cerb_location.unknown
+    | _ -> IT.le_ (start_expr, i_it) Cerb_location.unknown
+  in
+  (* End of range *)
   let end_cond =
     match end_expr with
     | IT (Binop (Sub, end_expr', IT (Const (Bits (_, n)), _, _)), _, _)
@@ -3036,10 +3041,37 @@ let cn_to_ail_resource
     }
     *)
     let i_sym, i_bt = q.q in
-    let start_expr, _, while_loop_cond = get_while_bounds_and_cond q.q q.permission in
+    let start_expr, end_expr, while_loop_cond =
+      get_while_bounds_and_cond q.q q.permission
+    in
     let _, _, e_start =
       cn_to_ail_expr filename dts globals spec_mode_opt start_expr PassBack
     in
+    let _, _, e_end =
+      cn_to_ail_expr filename dts globals spec_mode_opt end_expr PassBack
+    in
+    let pname = Sym.fresh "CN_INSERT_ITER_RES" in
+    let e_step = mk_expr A.(AilEsizeof (C.no_qualifiers, Sctypes.to_ctype q.step)) in
+    let _, _, e_pointer =
+      cn_to_ail_expr filename dts globals spec_mode_opt q.pointer PassBack
+    in
+    let iter_res_call_stmt_opt =
+      match q.name with
+      | Owned (sct, _) ->
+        let type_str = Pp.plain (Sctypes.pp sct) in
+        let ail_type_str = A.AilEstr (None, [ (Cerb_location.unknown, [ type_str ]) ]) in
+        let iter_res_call =
+          mk_expr
+            A.(
+              AilEcall
+                ( mk_expr (AilEident pname),
+                  [ e_pointer; e_start; e_end; e_step; mk_expr ail_type_str ] ))
+        in
+        let iter_res_call_stmt = A.(AilSexpr iter_res_call) in
+        Some iter_res_call_stmt
+      | _ -> None
+    in
+    (* Generate while loop condition *)
     let _, _, while_cond_expr =
       cn_to_ail_expr filename dts globals spec_mode_opt while_loop_cond PassBack
     in
@@ -3153,9 +3185,14 @@ let cn_to_ail_resource
                 mk_stmt (AilSblock ([], List.map mk_stmt [ if_stat; increment_stat ])),
                 0 ))
         in
-        let ail_block =
-          A.(AilSblock ([ start_binding ], List.map mk_stmt [ start_assign; while_loop ]))
+        let stmts = [ start_assign; while_loop ] in
+        let stmts =
+          match (iter_res_call_stmt_opt, spec_mode_opt) with
+          | (Some stmt, Some Pre | Some stmt, Some Loop) when !Config.with_auto_annot ->
+            stmt :: stmts
+          | _ -> stmts
         in
+        let ail_block = A.(AilSblock ([ start_binding ], List.map mk_stmt stmts)) in
         ([], [ ail_block ])
       | _ ->
         (* TODO: Change to mostly use index terms rather than Ail directly - avoids duplication between these functions and cn_to_ail *)
@@ -3209,9 +3246,14 @@ let cn_to_ail_resource
                 mk_stmt A.(AilSblock ([], List.map mk_stmt [ if_stat; increment_stat ])),
                 0 ))
         in
-        let ail_block =
-          A.(AilSblock ([ start_binding ], List.map mk_stmt [ start_assign; while_loop ]))
+        let stmts = [ start_assign; while_loop ] in
+        let stmts =
+          match (iter_res_call_stmt_opt, spec_mode_opt) with
+          | (Some stmt, Some Pre | Some stmt, Some Loop) when !Config.with_auto_annot ->
+            stmt :: stmts
+          | _ -> stmts
         in
+        let ail_block = A.(AilSblock ([ start_binding ], List.map mk_stmt stmts)) in
         ([ sym_binding ], [ sym_decl; ail_block ])
     in
     (b1 @ b2 @ b3 @ bs' @ bs, s1 @ s2 @ s3 @ ss @ ss')
@@ -3669,7 +3711,25 @@ let cn_to_ail_cnstatement
   | Have _lc -> failwith "TODO Have"
   | Instantiate (_to_instantiate, _it) -> (default_res_for_dest, true)
   | Split_case _ -> (default_res_for_dest, true)
-  | Extract (_, _, _it) -> (default_res_for_dest, true)
+  | Extract (_, _, _) when not !Config.with_auto_annot -> (default_res_for_dest, true)
+  | Extract (_, to_extract, it) ->
+    let b, ss, e = cn_to_ail_expr filename dts globals spec_mode_opt it PassBack in
+    (match to_extract with
+     | E_Pred (CN_owned (Some ct)) | E_Pred (CN_block (Some ct)) ->
+       let s = Pp.plain (Sctypes.pp ct) in
+       Pp.(debug 10 (lazy (string s)));
+       let s_expr = mk_expr (A.AilEstr (None, [ (Cerb_location.unknown, [ s ]) ])) in
+       let call_expr =
+         A.AilEcall (mk_expr (A.AilEident (Sym.fresh "CN_INSERT_FOCUS")), [ e; s_expr ])
+       in
+       let call_stat = A.AilSexpr (mk_expr call_expr) in
+       (prefix d (b, ss @ [ call_stat ]) (empty_for_dest d), false)
+     | E_Everything
+     | E_Pred (CN_owned None)
+     | E_Pred (CN_block None)
+     | E_Pred (CN_named _) ->
+       (* Not supported, or deprecated *)
+       (default_res_for_dest, true))
   | Unfold (_fsym, _args) -> (default_res_for_dest, true) (* fsym is a function symbol *)
   | Apply (fsym, args) ->
     ( cn_to_ail_expr
@@ -4115,8 +4175,23 @@ let cn_to_ail_loop_inv
     let cn_ownership_leak_check_call =
       A.AilSexpr (mk_expr (AilEcall (mk_expr (AilEident OE.cn_loop_leak_check_sym), [])))
     in
+    (* reset the current focus context *)
+    let pop_focus_context_fn_call =
+      A.AilSexpr
+        (mk_expr (AilEcall (mk_expr (AilEident (Sym.fresh "pop_focus_context")), [])))
+    in
+    let push_focus_context_fn_call =
+      A.AilSexpr
+        (mk_expr (AilEcall (mk_expr (AilEident (Sym.fresh "push_focus_context")), [])))
+    in
     let stats =
-      (bump_alloc_start_stat_ :: loop_ownership_state.assign :: cond_ss)
+      (bump_alloc_start_stat_
+       :: loop_ownership_state.assign
+       ::
+       (if !Config.with_auto_annot then
+          pop_focus_context_fn_call :: push_focus_context_fn_call :: cond_ss
+        else
+          cond_ss))
       @ (if with_loop_leak_checks then [ cn_ownership_leak_check_call ] else [])
       @ [ cn_loop_put_call; bump_alloc_end_stat_; dummy_expr_as_stat ]
     in
@@ -4282,7 +4357,14 @@ let rec cn_to_ail_lat_2
         List.map
           (fun fn_sym ->
              mk_stmt (A.AilSexpr (mk_expr (AilEcall (mk_expr (AilEident fn_sym), [])))))
-          OE.[ cn_stack_depth_decr_sym; cn_postcondition_leak_check_sym ]
+          (if !Config.with_auto_annot then
+             OE.
+               [ cn_stack_depth_decr_sym;
+                 cn_postcondition_leak_check_sym;
+                 Sym.fresh "pop_focus_context"
+               ]
+           else
+             OE.[ cn_stack_depth_decr_sym; cn_postcondition_leak_check_sym ])
     in
     let block =
       A.(
@@ -4504,7 +4586,15 @@ let cn_to_ail_pre_post
           A.AilSexpr
             (mk_expr (AilEcall (mk_expr (AilEident OE.cn_stack_depth_incr_sym), [])))
         in
-        [ cn_stack_depth_incr_stat_ ])
+        let push_focus_context =
+          A.AilSexpr
+            (mk_expr
+               (AilEcall (mk_expr (AilEident (Sym.fresh "push_focus_context")), [])))
+        in
+        if !Config.with_auto_annot then
+          [ cn_stack_depth_incr_stat_; push_focus_context ]
+        else
+          [ cn_stack_depth_incr_stat_ ])
     in
     let bump_alloc_binding, bump_alloc_start_stat_, bump_alloc_end_stat_ =
       gen_bump_alloc_bs_and_ss ()
diff --git a/lib/fulminate/config.ml b/lib/fulminate/config.ml
new file mode 100644
index 000000000..8efaee1ed
--- /dev/null
+++ b/lib/fulminate/config.ml
@@ -0,0 +1,5 @@
+let with_auto_annot = ref false
+
+let enable_auto_annot () = with_auto_annot := true
+
+let disable_auto_annot () = with_auto_annot := false
diff --git a/lib/fulminate/config.mli b/lib/fulminate/config.mli
new file mode 100644
index 000000000..41ee0e929
--- /dev/null
+++ b/lib/fulminate/config.mli
@@ -0,0 +1,5 @@
+val with_auto_annot : bool ref
+
+val enable_auto_annot : unit -> unit
+
+val disable_auto_annot : unit -> unit
diff --git a/lib/fulminate/fulminate.ml b/lib/fulminate/fulminate.ml
index 793f9fb62..12b286adf 100644
--- a/lib/fulminate/fulminate.ml
+++ b/lib/fulminate/fulminate.ml
@@ -6,6 +6,7 @@ module Internal = Internal
 module Records = Records
 module Ownership = Ownership
 module Utils = Utils
+module Config = Config
 
 let rec group_toplevel_defs new_list = function
   | [] -> new_list
@@ -114,7 +115,10 @@ let collect_memory_accesses (_, sigm) =
     | AilSskip | AilSbreak | AilScontinue | AilSreturnVoid | AilSgoto _ -> ()
     | AilSexpr e | AilSreturn e | AilSreg_store (_, e) -> aux_expr e env
     | AilSblock (bs, ss) ->
-      let lookup_ty sym = List.find (fun (sym', _) -> Sym.equal sym sym') bs in
+      let lookup_ty sym =
+        let _, (_, _, _, ty) = List.find (fun (sym', _) -> Sym.equal sym sym') bs in
+        (sym, ty)
+      in
       let env_cell = ref env in
       List.iter
         (fun s ->
@@ -150,10 +154,76 @@ let collect_memory_accesses (_, sigm) =
       (* AilSdeclaration must be handled in `AilSblock` *)
       failwith "unreachable"
   in
-  List.iter (fun (_, (_, _, _, _, stmt)) -> aux_stmt stmt []) sigm.function_definitions;
+  sigm.function_definitions
+  |> List.iter (fun (f, body) ->
+    match List.assoc Sym.equal f sigm.declarations with
+    | _, _, Decl_function (_, _, types, _, _, _) ->
+      let _, _, _, args, stmt = body in
+      let env = List.map2 (fun arg (_, ct, _) -> (arg, ct)) args types in
+      aux_stmt stmt env
+    | _ -> failwith "ill-formed program");
   !acc
 
 
+let gen_fmt_for_integer_type =
+  let open CF.Ctype in
+  (* Ignore IntN_t and its friends *)
+  let usable = function Ichar | Short | Int_ | Long | LongLong -> true | _ -> false in
+  function
+  | Char -> Some "%c"
+  | Bool -> Some "%d"
+  | Signed i when usable i ->
+    (match (CF.Ocaml_implementation.get ()).sizeof_ity (Signed i) with
+     | Some 1 -> Some "%c"
+     | Some 2 -> Some "%hd"
+     | Some 4 -> Some "%d"
+     | Some 8 -> Some "%lld"
+     | _ -> failwith "unimplemented")
+  | Unsigned u when usable u ->
+    (match (CF.Ocaml_implementation.get ()).sizeof_ity (Unsigned u) with
+     | Some 1 -> Some "%c"
+     | Some 2 -> Some "%hu"
+     | Some 4 -> Some "%u"
+     | Some 8 -> Some "%llu"
+     | _ -> failwith "unimplemented")
+  | _ -> None
+
+
+let get_symbol = function
+  | CF.Symbol.Symbol (_, _, CF.Symbol.SD_Id s)
+  | CF.Symbol.Symbol (_, _, CF.Symbol.SD_ObjectAddress s) ->
+    Some s
+  | CF.Symbol.Symbol (_, _, CF.Symbol.SD_FunArg _) -> failwith "funarg"
+  | CF.Symbol.Symbol (_, _, CF.Symbol.SD_FunArgValue _) -> failwith "var"
+  | CF.Symbol.Symbol (_, _, CF.Symbol.SD_CN_Id _) -> failwith "cn id"
+  | _ -> None
+
+
+let gen_env_fmt_printer x =
+  let rec aux = function
+    | [] -> ("", [])
+    | (sym, ty) :: xs ->
+      let fmt, args = aux xs in
+      let open CF.Ctype in
+      let (Ctype (_, ty)) = ty in
+      (match ty with
+       | Basic (Integer b) ->
+         (match (gen_fmt_for_integer_type b, get_symbol sym) with
+          | Some f, Some sym ->
+            let f = Printf.sprintf "%s=%s, " sym f in
+            (f ^ fmt, sym :: args)
+          | _ -> (fmt, args))
+       | Struct _ -> failwith "unimplemented"
+       | Basic (Floating _)
+       | Array _ | Function _ | Void | FunctionNoParams _ | Pointer _ | Atomic _ | Union _
+       | Byte ->
+         (fmt, args))
+  in
+  let fmt, args = aux x in
+  (* The first element is for the target index, which will be filled in CN_XXX_ANNOT macros *)
+  ("!index=%lld, " ^ fmt, args)
+
+
 let memory_accesses_injections ail_prog =
   let open Cerb_frontend in
   let open Cerb_location in
@@ -179,23 +249,66 @@ let memory_accesses_injections ail_prog =
   let acc = ref [] in
   let xs = collect_memory_accesses ail_prog in
   List.iter
-    (* HK: Currently, `env` is ignored. It will be used in future patches. *)
-    (fun (access, _env) ->
+    (fun (access, env) ->
+       (* autoannot things *)
+       let autoannot_fmt, autoannot_fmt_args =
+         if !Config.with_auto_annot then (
+           let fmt, args = gen_env_fmt_printer env in
+           (fmt ^ "\\n", List.fold_left (fun acc arg -> acc ^ ", " ^ arg) "" args))
+         else
+           ("", "")
+       in
        match access with
        | Load { loc; _ } ->
          let b, e = pos_bbox loc in
-         acc := (point b, [ "CN_LOAD(" ]) :: (point e, [ ")" ]) :: !acc
+         let pos_info = Cerb_location.location_to_string loc in
+         let autoannot_fmt_args =
+           ", \""
+           ^ "[auto annot (focus)]"
+           ^ pos_info
+           (* The fmt for type. Filled by CN_XXX_ANNOT *)
+           ^ ":%s:%s"
+           ^ ", "
+           ^ autoannot_fmt
+           ^ "\""
+           ^ autoannot_fmt_args
+         in
+         acc
+         := if !Config.with_auto_annot then
+              (point b, [ "CN_LOAD_ANNOT(" ])
+              :: (point e, [ autoannot_fmt_args ^ ")" ])
+              :: !acc
+            else
+              (point b, [ "CN_LOAD(" ]) :: (point e, [ ")" ]) :: !acc
        | Store { lvalue; expr; _ } ->
          (* NOTE: we are not using the location of the access (the AilEassign), because if
            in the source the assignment was surrounded by parens its location will contain
            the parens, which will break the CN_STORE macro call *)
          let b, pos1 = pos_bbox (loc_of_expr lvalue) in
          let pos2, e = pos_bbox (loc_of_expr expr) in
+         let pos_info = Cerb_location.location_to_string (loc_of_expr lvalue) in
+         let autoannot_fmt_args =
+           ", \""
+           ^ "[auto annot (focus)]"
+           ^ pos_info
+           (* The fmt for type. Filled by CN_XXX_ANNOT *)
+           ^ ":%s:%s"
+           ^ ", "
+           ^ autoannot_fmt
+           ^ "\""
+           ^ autoannot_fmt_args
+         in
          acc
-         := (point b, [ "CN_STORE(" ])
-            :: (region (pos1, pos2) NoCursor, [ ", " ])
-            :: (point e, [ ")" ])
-            :: !acc
+         := if !Config.with_auto_annot then
+              (point b, [ "CN_STORE_ANNOT(" ])
+              :: (region (pos1, pos2) NoCursor, [ ", " ])
+              :: (point e, [ autoannot_fmt_args ^ ")" ])
+              :: !acc
+            else
+              (point b, [ "CN_STORE(" ])
+              :: (region (pos1, pos2) NoCursor, [ ", " ])
+              :: (point e, [ ")" ])
+              :: !acc
        | StoreOp { lvalue; aop; expr; loc } ->
          (match bbox [ loc_of_expr expr ] with
           | `Other _ ->
@@ -204,28 +317,70 @@ let memory_accesses_injections ail_prog =
                      simple literals *)
             let pp_expr e = CF.Pp_utils.to_plain_string (Pp_ail.pp_expression e) in
             let sstart, ssend = pos_bbox loc in
+            let pos_info = Cerb_location.location_to_string loc in
+            let autoannot_fmt_args =
+              ", \""
+              ^ "[auto annot (focus)]"
+              ^ pos_info
+              (* The fmt for type. Filled by CN_XXX_ANNOT *)
+              ^ ":%s:%s"
+              ^ ", "
+              ^ autoannot_fmt
+              ^ "\""
+              ^ autoannot_fmt_args
+            in
             let b, _ = pos_bbox (loc_of_expr lvalue) in
             acc
             := (region (sstart, b) NoCursor, [ "" ])
-               :: ( point b,
-                    [ "CN_STORE_OP("
-                      ^ pp_expr lvalue
-                      ^ ","
-                      ^ string_of_aop aop
-                      ^ ","
-                      ^ pp_expr expr
-                      ^ ")"
-                    ] )
+               :: (if !Config.with_auto_annot then
+                     ( point b,
+                       [ "CN_STORE_OP_ANNOT("
+                         ^ pp_expr lvalue
+                         ^ ","
+                         ^ string_of_aop aop
+                         ^ ","
+                         ^ pp_expr expr
+                         ^ autoannot_fmt_args
+                         ^ ")"
+                       ] )
+                   else
+                     ( point b,
+                       [ "CN_STORE_OP("
+                         ^ pp_expr lvalue
+                         ^ ","
+                         ^ string_of_aop aop
+                         ^ ","
+                         ^ pp_expr expr
+                         ^ ")"
+                       ] ))
                :: (region (b, ssend) NoCursor, [ "" ])
                :: !acc
           | `Bbox _ ->
             let b, pos1 = pos_bbox (loc_of_expr lvalue) in
             let pos2, e = pos_bbox (loc_of_expr expr) in
+            let pos_info = Cerb_location.location_to_string (loc_of_expr lvalue) in
+            let autoannot_fmt_args =
+              ", \""
+              ^ "[auto annot (focus)]"
+              ^ pos_info
+              (* The fmt for type. Filled by CN_XXX_ANNOT *)
+              ^ ":%s:%s"
+              ^ ", "
+              ^ autoannot_fmt
+              ^ "\""
+              ^ autoannot_fmt_args
+            in
             acc
-            := (point b, [ "CN_STORE_OP(" ])
-               :: (region (pos1, pos2) NoCursor, [ "," ^ string_of_aop aop ^ "," ])
-               :: (point e, [ ")" ])
-               :: !acc)
+            := if !Config.with_auto_annot then
+                 (point b, [ "CN_STORE_OP_ANNOT(" ])
+                 :: (region (pos1, pos2) NoCursor, [ "," ^ string_of_aop aop ^ "," ])
+                 :: (point e, [ autoannot_fmt_args ^ ")" ])
+                 :: !acc
+               else
+                 (point b, [ "CN_STORE_OP(" ])
+                 :: (region (pos1, pos2) NoCursor, [ "," ^ string_of_aop aop ^ "," ])
+                 :: (point e, [ ")" ])
+                 :: !acc)
        | Postfix { loc; op; lvalue } ->
          let op_str = match op with `Incr -> "++" | `Decr -> "--" in
          let b, e = pos_bbox loc in
@@ -480,7 +635,18 @@ let main
   in
   (* Save things *)
   let oc = Stdlib.open_out out_filename in
-  output_to_oc oc [ "#define __CN_INSTRUMENT\n"; "#include <cn-executable/utils.h>\n" ];
+  if !Config.with_auto_annot then (
+    output_to_oc
+      oc
+      [ "#define __CN_INSTRUMENT\n";
+        "#include <stdint.h>\n";
+        "#include <cn-executable/utils.h>\n"
+      ];
+    output_to_oc oc [ "#include <cn-autoannot/auto_annot.h>\n" ])
+  else (
+    output_to_oc oc [ "#define __CN_INSTRUMENT\n"; "#include <cn-executable/utils.h>\n" ];
+    output_to_oc oc [ "#include <cn-autoannot/auto_annot.h>\n" ]);
+  output_to_oc oc [ "#include <stdio.h>\n" ];
   output_to_oc oc cn_header_decls_list;
   output_to_oc
     oc
diff --git a/lib/fulminate/fulminate.mli b/lib/fulminate/fulminate.mli
index 19ffa26ec..bf0171f0a 100644
--- a/lib/fulminate/fulminate.mli
+++ b/lib/fulminate/fulminate.mli
@@ -5,6 +5,7 @@ module Internal = Internal
 module Ownership = Ownership
 module Records = Records
 module Utils = Utils
+module Config = Config
 
 val get_instrumented_filename : string -> string
 
diff --git a/lib/fulminate/internal.ml b/lib/fulminate/internal.ml
index a9b7f50bf..b4c806d9f 100644
--- a/lib/fulminate/internal.ml
+++ b/lib/fulminate/internal.ml
@@ -114,7 +114,8 @@ let generate_c_loop_invariants
         ail_loop_decls
     in
     let ail_loop_close_block_injs =
-      List.map (fun (loc, _) -> (get_end_loc loc, [ "}" ])) ail_loop_decls
+      let close_token = if !Config.with_auto_annot then "}\nclear_focus ();" else "}" in
+      List.map (fun (loc, _) -> (get_end_loc loc, [ close_token ])) ail_loop_decls
     in
     ail_cond_injs @ ail_loop_decl_injs @ ail_loop_close_block_injs)
 
@@ -571,6 +572,13 @@ let has_main (sigm : CF.GenTypes.genTypeCategory CF.AilSyntax.sigma) =
   List.non_empty (get_main sigm)
 
 
+let finalize_auto_annot () =
+  let cn_finalize_auto_annot_fcall =
+    mk_expr A.(AilEcall (mk_expr (AilEident (Sym.fresh "finalize_auto_annot")), []))
+  in
+  A.(AilSexpr cn_finalize_auto_annot_fcall)
+
+
 let generate_global_assignments
       ?(experimental_ownership_stack_mode = false)
       (sigm : CF.GenTypes.genTypeCategory CF.AilSyntax.sigma)
@@ -608,5 +616,12 @@ let generate_global_assignments
              :: global_map_stmts_) )
     in
     let global_unmapping_stmts_ = List.map OE.generate_c_local_ownership_exit globals in
+    let global_unmapping_stmts_ =
+      if !Config.with_auto_annot then (
+        let finalize_stmt = finalize_auto_annot () in
+        finalize_stmt :: global_unmapping_stmts_)
+      else
+        global_unmapping_stmts_
+    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/lib/fulminate/ownership.ml b/lib/fulminate/ownership.ml
index 0c1a5977d..78a8b3d42 100644
--- a/lib/fulminate/ownership.ml
+++ b/lib/fulminate/ownership.ml
@@ -66,12 +66,26 @@ let get_ownership_global_init_stats ?(ghost_array_size = 100) () =
                    (ConstantInteger (IConstant (Z.of_int ghost_array_size, Decimal, None))))
             ] ))
   in
-  List.map
-    (fun e -> A.(AilSexpr e))
-    [ cn_ghost_state_init_fcall;
-      cn_ghost_stack_depth_init_fcall;
-      cn_ghost_arg_array_alloc_fcall
-    ]
+  let log_filename =
+    mk_expr (A.AilEstr (None, [ (Cerb_location.unknown, [ !AutoAnnot.log_filename ]) ]))
+  in
+  let cn_initialize_auto_annot_fcall =
+    mk_expr
+      A.(
+        AilEcall
+          (mk_expr (AilEident (Sym.fresh "initialize_auto_annot")), [ log_filename ]))
+  in
+  let fns =
+    if !Config.with_auto_annot then
+      [ cn_ghost_state_init_fcall;
+        cn_ghost_stack_depth_init_fcall;
+        cn_ghost_arg_array_alloc_fcall;
+        cn_initialize_auto_annot_fcall
+      ]
+    else
+      [ cn_ghost_state_init_fcall; cn_ghost_stack_depth_init_fcall ]
+  in
+  List.map (fun e -> A.(AilSexpr e)) fns
 
 
 let generate_c_local_cn_addr_var sym =
diff --git a/lib/testGeneration/testGenConfig.ml b/lib/testGeneration/testGenConfig.ml
index fd6c76d5a..59933a82b 100644
--- a/lib/testGeneration/testGenConfig.ml
+++ b/lib/testGeneration/testGenConfig.ml
@@ -69,7 +69,8 @@ type t =
     print_size_info : bool;
     print_backtrack_info : bool;
     print_satisfaction_info : bool;
-    print_discard_info : bool
+    print_discard_info : bool;
+    with_auto_annot : bool
   }
 
 let default =
@@ -114,7 +115,8 @@ let default =
     print_size_info = false;
     print_backtrack_info = false;
     print_satisfaction_info = false;
-    print_discard_info = false
+    print_discard_info = false;
+    with_auto_annot = false
   }
 
 
@@ -269,3 +271,5 @@ let has_symbolic_timeout () = (Option.get !instance).symbolic_timeout
 let get_max_unfolds () = (Option.get !instance).max_unfolds
 
 let get_max_array_length () = (Option.get !instance).max_array_length
+
+let with_auto_annot () = (Option.get !instance).with_auto_annot
diff --git a/lib/testGeneration/testGenConfig.mli b/lib/testGeneration/testGenConfig.mli
index 0a829e817..361b2aa5e 100644
--- a/lib/testGeneration/testGenConfig.mli
+++ b/lib/testGeneration/testGenConfig.mli
@@ -69,7 +69,8 @@ type t =
     print_size_info : bool;
     print_backtrack_info : bool;
     print_satisfaction_info : bool;
-    print_discard_info : bool
+    print_discard_info : bool;
+    with_auto_annot : bool
   }
 
 val default : t
@@ -179,3 +180,5 @@ val has_symbolic_timeout : unit -> int option
 val get_max_unfolds : unit -> int option
 
 val get_max_array_length : unit -> int
+
+val with_auto_annot : unit -> bool
diff --git a/lib/testGeneration/testGeneration.ml b/lib/testGeneration/testGeneration.ml
index a71c62dcf..6f448c361 100644
--- a/lib/testGeneration/testGeneration.ml
+++ b/lib/testGeneration/testGeneration.ml
@@ -236,6 +236,10 @@ let compile_test_file
           "#include <cn-executable/utils.h>\n";
           "#include <cn-executable/cerb_types.h>\n"
         ];
+        (if Config.with_auto_annot () then
+           [ "#include <cn-autoannot/auto_annot.h>\n" ]
+         else
+           []);
         [ c_struct_decls ];
         [ (* (if not (String.equal record_defs "") then "\n/* CN RECORDS */\n\n" else ""); *)
           (*  record_defs; *)
@@ -276,6 +280,13 @@ let compile_test_file
     |> Pp.(separate hardline)
   in
   let open Pp in
+  let initialize_auto_annot, finalize_auto_annot =
+    if Config.with_auto_annot () then
+      ( string ("initialize_auto_annot(\"" ^ !AutoAnnot.log_filename ^ "\");") ^^ hardline,
+        string "finalize_auto_annot();" ^^ hardline )
+    else
+      (string "", string "")
+  in
   !^(String.concat " " cn_header_decls_list)
   ^^ compile_includes ~filename ~generators:(List.non_empty generator_tests)
   ^^ twice hardline
@@ -295,9 +306,13 @@ let compile_test_file
               (nest
                  2
                  (hardline
+                  ^^ initialize_auto_annot
                   ^^ separate_map hardline compile_test all_tests
                   ^^ twice hardline
-                  ^^ !^"return cn_test_main(argc, argv);")
+                  ^^ !^"int cn_test_main_ret = cn_test_main(argc, argv);"
+                  ^^ hardline
+                  ^^ finalize_auto_annot
+                  ^^ !^"return cn_test_main_ret;")
                ^^ hardline))
   ^^ hardline
   ^^ !^(String.concat
diff --git a/runtime/libcn/include/cn-autoannot/auto_annot.h b/runtime/libcn/include/cn-autoannot/auto_annot.h
new file mode 100644
index 000000000..e65d8bcdd
--- /dev/null
+++ b/runtime/libcn/include/cn-autoannot/auto_annot.h
@@ -0,0 +1,102 @@
+#ifndef FOCUS_CTX_H
+#define FOCUS_CTX_H
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <cn-executable/cerb_types.h>
+#include <stdint.h>
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+typedef const char *type_sig;
+
+// Defined in cn-autoannot/auto_annot.c
+extern FILE *auto_annot_log_file;
+
+#define cn_auto_annot_printf(...) fprintf(auto_annot_log_file, __VA_ARGS__)
+
+// Wrapper for cn values
+#define CN_INSERT_ITER_RES(base, start, end, size, sig)                                  \
+  insert_iter_res((uint64_t)base->ptr, start->val, end->val, size, sig)
+
+#define CN_INSERT_FOCUS(index, sig) insert_focus(index->val, sig)
+
+#define CN_LOAD_ANNOT(LV, FMT, ...)                                                      \
+  ({                                                                                     \
+    typeof(LV) *__tmp = &(LV);                                                           \
+    int64_t index;                                                                       \
+    type_sig sig;                                                                        \
+    if (needs_focus((uint64_t)__tmp, sizeof(typeof(LV)), &index, &sig))                  \
+      cn_auto_annot_printf(FMT, "RW", sig, index, ##__VA_ARGS__);                        \
+    CN_LOAD(LV);                                                                         \
+  })
+
+#define CN_STORE_OP_ANNOT(LV, op, X, FMT, ...)                                           \
+  ({                                                                                     \
+    typeof(LV) *__tmp;                                                                   \
+    __tmp = &(LV);                                                                       \
+    int64_t index;                                                                       \
+    type_sig sig;                                                                        \
+    if (needs_focus((uint64_t)__tmp, sizeof(typeof(LV)), &index, &sig))                  \
+      cn_auto_annot_printf(FMT, "RW", sig, index, ##__VA_ARGS__);                        \
+    CN_STORE_OP(LV, op, X);                                                              \
+  })
+
+#define CN_STORE_ANNOT(LV, X, FMT, ...) CN_STORE_OP_ANNOT(LV, , X, FMT, ##__VA_ARGS__)
+
+void initialize_auto_annot(const char *log_file);
+void finalize_auto_annot(void);
+
+// Limitation: we only consider contiguous iter ress.
+struct iter_res {
+  uint64_t ptr;
+  // contiguous indices (closed interval)
+  uint64_t start;
+  uint64_t end;
+  // step
+  uint64_t size;
+  // type signature
+  type_sig sig;
+};
+
+enum cn_res_type {
+  CN_RES_ITER,
+  OTHER,
+};
+
+struct cn_res {
+  enum cn_res_type type;
+  union {
+    struct iter_res iter_res;
+  };
+};
+
+struct focus_info {
+  int64_t index;
+  type_sig sig;
+};
+
+typedef struct focus_set {
+  struct focus_info info;
+  struct focus_set *next;
+} focus_set;
+
+struct focus_context {
+  focus_set *indices;
+  struct focus_context *prev;
+};
+
+void initialise_focus_context();
+void push_focus_context(void);
+void pop_focus_context(void);
+void clear_focus(void);
+void insert_focus(int64_t index, type_sig sig);
+int needs_focus(uint64_t address, uint64_t size, int64_t *index_out, type_sig *sig_out);
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif  // FOCUS_CTX_H
diff --git a/runtime/libcn/include/cn-executable/utils.h b/runtime/libcn/include/cn-executable/utils.h
index bed8e632b..0ece3c64f 100644
--- a/runtime/libcn/include/cn-executable/utils.h
+++ b/runtime/libcn/include/cn-executable/utils.h
@@ -7,6 +7,7 @@
 #include "hash_table.h"
 #include "rts_deps.h"
 #include "stack.h"
+#include <cn-autoannot/auto_annot.h>
 
 #define cn_printf(level, ...)                                                            \
   if (get_cn_logging_level() >= level) {                                                 \
@@ -143,10 +144,17 @@ typedef struct cn_alloc_id {
 
 typedef hash_table cn_map;
 
+enum RuntimeMode {
+  RUNTIME_NORMAL_MODE,
+  RUNTIME_OWNERSHIP_STACK_MODE,
+  RUNTIME_AUTO_ANNOT_MODE,
+};
+extern enum RuntimeMode runtime_mode;
+
 void initialise_ownership_ghost_state(void);
 void free_ownership_ghost_state(void);
 void initialise_ghost_stack_depth(void);
-void initialise_ownership_stack_mode(bool flag);
+void initialise_runtime_mode(enum RuntimeMode mode);
 signed long get_cn_stack_depth(void);
 void ghost_stack_depth_incr(void);
 void ghost_stack_depth_decr(void);
@@ -543,11 +551,17 @@ CN_GEN_MAP_GET(cn_map)
 /* OWNERSHIP */
 
 GEN_ALL_STACK(cn_source_location, char*);
+GEN_ALL_STACK(cn_res_info, struct cn_res*);
 
 typedef struct ownership_ghost_info {
   int depth;
-  cn_source_location_stack*
-      source_loc_stack;  // set to null if ownership_stack_mode is disabled
+  union {
+    // runtime_mode == RUNTIME_OWNERSHIP_STACK_MODE
+    cn_source_location_stack* source_loc_stack;  // set to null if ownership_stack_mode is disabled
+
+    // runtime_mode == RUNTIME_AUTO_ANNOT_MODE
+    cn_res_info_stack* res_info_stack;
+  };
 } ownership_ghost_info;
 
 enum STACK_OP {
@@ -557,6 +571,8 @@ enum STACK_OP {
 };
 
 int ownership_ghost_state_get_depth(int64_t address);
+ownership_ghost_info* ownership_ghost_state_get(int64_t address);
+
 void ownership_ghost_state_set(int64_t address,
     size_t size,
     int stack_depth_val,
diff --git a/runtime/libcn/include/dune b/runtime/libcn/include/dune
index 545fecc57..062a95338 100644
--- a/runtime/libcn/include/dune
+++ b/runtime/libcn/include/dune
@@ -20,6 +20,8 @@
   (cn-executable/rts_deps.h as runtime/include/cn-executable/rts_deps.h)
   (cn-executable/cerb_types.h as runtime/include/cn-executable/cerb_types.h)
   (cn-executable/stack.h as runtime/include/cn-executable/stack.h)
+  ; AutoAnnot
+  (cn-autoannot/auto_annot.h as runtime/include/cn-autoannot/auto_annot.h)
   ; Bennet
   (bennet/prelude.h as runtime/include/bennet/prelude.h)
   (bennet/dsl/arbitrary.h as runtime/include/bennet/dsl/arbitrary.h)
diff --git a/runtime/libcn/lib/dune b/runtime/libcn/lib/dune
index 4ef0c4642..c6ec32ce5 100644
--- a/runtime/libcn/lib/dune
+++ b/runtime/libcn/lib/dune
@@ -2,9 +2,12 @@
  (target libcn_exec.a)
  (deps
   (:headers
-   (glob_files ../include/cn-executable/*.h))
+   (glob_files ../include/cn-executable/*.h)
+   (glob_files ../include/cn-autoannot/*.h))
   (:src
-   (glob_files ../src/cn-executable/*.c)))
+   (glob_files ../src/cn-executable/*.c)
+   (file ../src/cn-autoannot/focus_ctx.c)
+   (file ../src/cn-autoannot/auto_annot.c)))
  (action
   (progn
    (run mkdir -p cn-executable)
@@ -18,7 +21,9 @@
     cn-executable/fulminate_alloc.o
     cn-executable/bump_alloc.o
     cn-executable/hash_table.o
-    cn-executable/utils.o))))
+    cn-executable/utils.o
+    cn-executable/focus_ctx.o
+    cn-executable/auto_annot.o))))
 
 (rule
  (target libbennet.a)
diff --git a/runtime/libcn/src/cn-autoannot/auto_annot.c b/runtime/libcn/src/cn-autoannot/auto_annot.c
new file mode 100644
index 000000000..0dfca866e
--- /dev/null
+++ b/runtime/libcn/src/cn-autoannot/auto_annot.c
@@ -0,0 +1,23 @@
+#include <cn-autoannot/auto_annot.h>
+
+#include <stdlib.h>
+
+#include <cn-executable/utils.h>
+
+// Single definition of the global log file pointer
+FILE *auto_annot_log_file = NULL;
+
+//void initialise_focus_context();
+
+void initialize_auto_annot(const char *log_file) {
+  auto_annot_log_file = fopen(log_file, "a");
+  if (auto_annot_log_file == NULL) {
+    cn_printf(CN_LOGGING_ERROR, "Failed to open log file: %s\n", log_file);
+    exit(EXIT_FAILURE);
+  }
+  initialise_focus_context();
+}
+
+void finalize_auto_annot() {
+  fclose(auto_annot_log_file);
+}
diff --git a/runtime/libcn/src/cn-autoannot/focus_ctx.c b/runtime/libcn/src/cn-autoannot/focus_ctx.c
new file mode 100644
index 000000000..0cfcff7ba
--- /dev/null
+++ b/runtime/libcn/src/cn-autoannot/focus_ctx.c
@@ -0,0 +1,101 @@
+#include <cn-autoannot/auto_annot.h>
+
+#include <assert.h>
+#include <inttypes.h>
+#include <limits.h>
+#include <signal.h>  // for SIGABRT
+#include <stdint.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+
+#include <cn-executable/cerb_types.h>
+#include <cn-executable/fulminate_alloc.h>
+#include <cn-executable/utils.h>
+
+// Note(HK):
+// we don't have to care about the difference between Owned/Block here
+// because they are handled by the standard Fulminate machinery.
+// i.e., if there is a discrepancy, it will be caught by Fulminate.
+
+struct focus_context *cn_focus_global_context;  // top of the stack
+
+// should happen simultaneously with ghost_stack_depth_incr
+void push_focus_context(void) {
+  struct focus_context *new_context =
+      fulm_default_alloc.malloc(sizeof(struct focus_context));
+  new_context->indices = NULL;
+  new_context->prev = cn_focus_global_context;
+  cn_focus_global_context = new_context;
+}
+
+void initialise_focus_context() {
+  push_focus_context();
+}
+
+void pop_focus_context(void) {
+  struct focus_context *old_context = cn_focus_global_context;
+  cn_focus_global_context = cn_focus_global_context->prev;
+  // free
+  focus_set *cur_focus = old_context->indices;
+  while (cur_focus) {
+    focus_set *next = cur_focus->next;
+    fulm_free(cur_focus, &fulm_default_alloc);
+    cur_focus = next;
+  }
+
+}
+
+void insert_focus(int64_t index, type_sig sig) {
+  struct focus_set *new_set = fulm_malloc(sizeof(struct focus_set), &fulm_default_alloc);
+  new_set->info.index = index;
+  new_set->info.sig = sig;
+  new_set->next = cn_focus_global_context->indices;
+  cn_focus_global_context->indices = new_set;
+}
+
+void clear_focus() {
+  focus_set *cur_focus = cn_focus_global_context->indices;
+  while (cur_focus) {
+    focus_set *next = cur_focus->next;
+    fulm_free(cur_focus, &fulm_default_alloc);
+    cur_focus = next;
+  }
+  cn_focus_global_context->indices = NULL;
+}
+
+/// Checks if the given address
+///  (i) is in a iterated resource
+///  (ii) is not focused
+/// If (i) and (ii), it needs focus, and returns 1.
+int needs_focus(uint64_t address, uint64_t size, int64_t *index_out, type_sig *sig_out) {
+  assert(cn_focus_global_context != NULL);
+  ownership_ghost_info * info = ownership_ghost_state_get(address);
+  if (!info) {
+    return 0;
+  }
+  struct cn_res* res_info = info->res_info_stack->top->cn_res_info;
+
+  if (res_info->type != CN_RES_ITER) {
+    return 0;
+  }
+  struct iter_res* res = &res_info->iter_res;
+
+  int64_t offset = address - res->ptr;
+  uint64_t index = offset / res->size;
+
+  // Case: an appropriate iterated resource is found
+  // (ii) search for focus
+  focus_set *cur_focus = cn_focus_global_context->indices;
+  while (cur_focus) {
+    if (cur_focus->info.index == index &&
+        strcmp(cur_focus->info.sig, res->sig) == 0) {
+      return 0;
+    }
+    cur_focus = cur_focus->next;
+  }
+  // The index is not focused
+  *index_out = index;
+  *sig_out = res->sig;
+  return 1;
+}
diff --git a/runtime/libcn/src/cn-executable/utils.c b/runtime/libcn/src/cn-executable/utils.c
index b8f2573bd..bd376d5fd 100644
--- a/runtime/libcn/src/cn-executable/utils.c
+++ b/runtime/libcn/src/cn-executable/utils.c
@@ -19,21 +19,29 @@ signed long cn_stack_depth;
 
 signed long nr_owned_predicates;
 
-_Bool ownership_stack_mode;
+enum RuntimeMode runtime_mode = RUNTIME_NORMAL_MODE;
 
-static signed long UNMAPPED_VAL = -1;
+    static signed long UNMAPPED_VAL = -1;
 static signed long WILDCARD_DEPTH = INT_MIN + 1;
 
 static allocator bump_alloc = (allocator){
     .malloc = &cn_bump_malloc, .calloc = &cn_bump_calloc, .free = &cn_bump_free};
 
+int is_ownership_stack_mode() {
+  return runtime_mode == RUNTIME_OWNERSHIP_STACK_MODE;
+}
+
+int is_auto_annot_mode() {
+  return runtime_mode == RUNTIME_AUTO_ANNOT_MODE;
+}
+
 void reset_fulminate(void) {
   cn_bump_free_all();
   free_ownership_ghost_state();
   reset_error_msg_info();
   initialise_ownership_ghost_state();
   initialise_ghost_stack_depth();
-  initialise_ownership_stack_mode(0);
+  initialise_runtime_mode(RUNTIME_NORMAL_MODE);
 }
 
 static enum cn_logging_level logging_level = CN_LOGGING_INFO;
@@ -223,8 +231,8 @@ void initialise_ghost_stack_depth(void) {
   cn_stack_depth = 0;
 }
 
-void initialise_ownership_stack_mode(_Bool flag) {
-  ownership_stack_mode = flag;
+void initialise_runtime_mode(enum RuntimeMode mode) {
+  runtime_mode = mode;
 }
 
 signed long get_cn_stack_depth(void) {
@@ -287,7 +295,7 @@ void cn_postcondition_leak_check(void) {
     int64_t* key = it.key;
     ownership_ghost_info* info = (ownership_ghost_info*)it.value;
     if (info->depth != WILDCARD_DEPTH && info->depth > cn_stack_depth) {
-      if (ownership_stack_mode) {
+      if (is_ownership_stack_mode()) {
         print_owned_calls_stack(info);
       }
       print_error_msg_info(global_error_msg_info);
@@ -309,7 +317,7 @@ void cn_loop_leak_check(void) {
     ownership_ghost_info* info = (ownership_ghost_info*)it.value;
     /* Everything mapped to the function stack depth should have been bumped up by calls to Owned in invariant */
     if (info->depth != WILDCARD_DEPTH && info->depth == cn_stack_depth) {
-      if (ownership_stack_mode) {
+      if (is_ownership_stack_mode()) {
         print_owned_calls_stack(info);
       }
       print_error_msg_info(global_error_msg_info);
@@ -385,14 +393,14 @@ void ownership_ghost_state_set(int64_t address,
         (ownership_ghost_info*)ht_get(cn_ownership_global_ghost_state, &k);
     if (!entry) {
       entry = fulm_malloc(sizeof(ownership_ghost_info), &fulm_default_alloc);
-      if (ownership_stack_mode) {
+      if (is_ownership_stack_mode()) {
         entry->source_loc_stack = cn_source_location_stack_init(&fulm_default_alloc);
       } else {
         entry->source_loc_stack = 0;
       }
     }
     entry->depth = stack_depth_val;
-    if (ownership_stack_mode) {
+    if (is_ownership_stack_mode()) {
       switch (op) {
         case NO_OP:
           break;
@@ -539,7 +547,7 @@ void c_ownership_check(char* access_kind,
         ownership_ghost_state_get((uintptr_t)generic_c_ptr + i);
     int curr_depth = entry_maybe ? entry_maybe->depth : UNMAPPED_VAL;
     if (curr_depth != WILDCARD_DEPTH && curr_depth != expected_stack_depth) {
-      if (ownership_stack_mode) {
+      if (is_ownership_stack_mode()) {
         print_owned_calls_stack(entry_maybe);
       }
       print_error_msg_info(global_error_msg_info);
diff --git a/runtime/libcn/test/CMakeLists.txt b/runtime/libcn/test/CMakeLists.txt
index 9b778ca87..39105bf65 100644
--- a/runtime/libcn/test/CMakeLists.txt
+++ b/runtime/libcn/test/CMakeLists.txt
@@ -35,6 +35,7 @@ add_executable(libcn_tests
     cn-smt/subst.cpp
     cn-smt/sexp.cpp
     cn-smt/solver.cpp
+    autoannot/focus.cpp
 )
 
 # Disable narrowing warnings
diff --git a/runtime/libcn/test/autoannot/focus.cpp b/runtime/libcn/test/autoannot/focus.cpp
new file mode 100644
index 000000000..7628266ea
--- /dev/null
+++ b/runtime/libcn/test/autoannot/focus.cpp
@@ -0,0 +1,73 @@
+#include <cn-autoannot/auto_annot.h>
+#include <gtest/gtest.h>
+
+class LibAutoAnnot : public ::testing::Test {
+ protected:
+  void SetUp() override;
+};
+
+TEST(LibAutoAnnot, BasicOperations) {
+  initialise_focus_context();
+  push_focus_context();
+  int64_t index = -1;
+  type_sig sig = NULL;
+
+  /*
+  let p = 0xcafe000;
+  take X = each(u64 i; i < 4) { RW<u64>(p) };
+  */
+  insert_iter_res(0xcafe0000, 0, 4, 8, "unsigned long");
+  /* focus RW<u64>, 1u64; */
+  insert_focus(1, "unsigned long");
+
+  ASSERT_EQ(needs_focus(0xcafe0000, 8, &index, &sig), 1) << "Lack of focus for p[0]";
+  ASSERT_EQ(index, 0) << "Focused index should be 0";
+  ASSERT_EQ(strcmp(sig, "unsigned long"), 0) << "Focused type should be unsigned long";
+  ASSERT_EQ(needs_focus(0xcafe0008, 8, &index, &sig), 0) << "Focused";
+  ASSERT_EQ(needs_focus(0xcafe1000, 8, &index, &sig), 0)
+      << "No appropriate resource, so we don't need focus";
+
+  clear_focus();
+  ASSERT_EQ(needs_focus(0xcafe0008, 8, &index, &sig), 1) << "Cleared";
+  ASSERT_EQ(index, 1) << "Focused index should be 1";
+  ASSERT_EQ(strcmp(sig, "unsigned long"), 0) << "Focused type should be unsigned long";
+
+  insert_focus(1, "unsigned long");
+  ASSERT_EQ(needs_focus(0xcafe0008, 8, &index, &sig), 0) << "Focused";
+
+  push_focus_context();
+  insert_iter_res(0xcafe0000, 0, 4, 8, "unsigned long");
+  insert_iter_res(0x10000000, 1, 4, 8, "unsigned long");
+  insert_iter_res(0x20000000, 0, 4, 4, "unsigned int");
+  ASSERT_EQ(needs_focus(0xcafe0008, 8, &index, &sig), 1)
+      << "No focus in the current level";
+  ASSERT_EQ(index, 1) << "Focused index should be 1";
+  ASSERT_EQ(strcmp(sig, "unsigned long"), 0) << "Focused type should be unsigned long";
+  ASSERT_EQ(needs_focus(0xcafe0000, 8, &index, &sig), 1)
+      << "No focus in the current level";
+  ASSERT_EQ(index, 0) << "Focused index should be 0";
+  ASSERT_EQ(strcmp(sig, "unsigned long"), 0) << "Focused type should be unsigned long";
+
+  insert_focus(1, "unsigned long");
+  ASSERT_EQ(needs_focus(0xcafe0008, 8, &index, &sig), 0) << "Just focused";
+  ASSERT_EQ(needs_focus(0x10000008, 8, &index, &sig), 0) << "Just focused";
+  ASSERT_EQ(needs_focus(0x20000004, 4, &index, &sig), 1) << "Type mismatch";
+  ASSERT_EQ(index, 1) << "Focused index should be 1";
+  ASSERT_EQ(strcmp(sig, "unsigned int"), 0) << "Focused type should be unsigned int";
+  ASSERT_EQ(needs_focus(0x10000000, 8, &index, &sig), 0) << "Out of the iter_res";
+  insert_focus(1, "unsigned int");
+  ASSERT_EQ(needs_focus(0x20000004, 4, &index, &sig), 0) << "Just focused";
+
+  pop_focus_context();
+
+  // Check if it remembers the context
+  ASSERT_EQ(needs_focus(0xcafe0000, 8, &index, &sig), 1) << "Lack of focus for p[0]";
+  ASSERT_EQ(index, 0) << "Focused index should be 0";
+  ASSERT_EQ(needs_focus(0xcafe0008, 8, &index, &sig), 0)
+      << "Focus has already been annotated";
+  ASSERT_EQ(strcmp(sig, "unsigned long"), 0) << "Focused type should be unsigned long";
+
+  pop_focus_context();
+  ASSERT_EQ(needs_focus(0xcafe0000, 8, &index, &sig), 0) << "No need for focus";
+  ASSERT_EQ(needs_focus(0xcafe0008, 8, &index, &sig), 0) << "No need for focus";
+}
diff --git a/runtime/libcn/test/build/dune b/runtime/libcn/test/build/dune
index 5bb03cc82..00ad7d402 100644
--- a/runtime/libcn/test/build/dune
+++ b/runtime/libcn/test/build/dune
@@ -15,7 +15,8 @@
   (file Makefile)
   (glob_files ../bennet/*.hpp)
   (glob_files ../bennet/*.cpp)
-  (glob_files ../cn-smt/*.cpp))
+  (glob_files ../cn-smt/*.cpp)
+  (glob_files ../autoannot/*.cpp))
  (action
   (run make)))