diff --git a/book/tutorial/Makefile b/book/tutorial/Makefile
index b1456e01..5ba570f6 100644
--- a/book/tutorial/Makefile
+++ b/book/tutorial/Makefile
@@ -46,11 +46,10 @@ FSTAR_EXTRACT = --extract 'OCaml:-* +Spec'
 # But also:
 # - --cmi, for cross-module inlining, a must-have for anyone who relies on
 #   inline_for_extraction in the presence of interfaces
-# - --cache_checked_modules to rely on a pre-built ulib and krmllib
-# - --cache_dir, to avoid polluting our generated build artifacts outside o
+# - --cache_dir, to place checked files there
 
 FSTAR_NO_FLAGS = $(FSTAR_EXE) --ext context_pruning \
-  --odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
+  --odir obj $(FSTAR_INCLUDES) --cmi \
   --already_cached 'Prims FStar LowStar C Spec.Loops TestLib WasmSupport' --warn_error '+241@247+285' \
   --cache_dir obj
 
@@ -72,7 +71,7 @@ FSTAR_ROOTS = $(wildcard $(addsuffix /*.fsti,$(SOURCE_DIRS))) \
 # mtime of the moved files.
 ifndef MAKE_RESTARTS
 .depend: .FORCE
-	$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) $(FSTAR_EXTRACT) --output_deps_to $@
+	$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) $(FSTAR_EXTRACT) -o $@
 
 .PHONY: .FORCE
 .FORCE:
@@ -115,32 +114,22 @@ obj:
 # up-to-date (checksum matches, file unchanged), but this will confuse
 # make and result in endless rebuilds. So, we touch that file.
 %.checked: | obj
-	$(FSTAR) $< $(FSTAR_FLAGS) && touch -c $@
+	$(FSTAR) $(FSTAR_FLAGS) -c $< -o $@ && touch -c $@
 
 # Extraction
 # ----------
 
-# A few mismatches here between the dependencies present in the .depend and the
-# expected F* invocation. In .depend:
-#
-# obj/Bignum_Impl.ml: obj/Bignum.Impl.fst.checked ... more dependencies ...
-#
-# But F* wants (remember that F* searches for source files anywhere on the
-# include path):
-#
-# fstar Bignum.Impl.fst --extract_module BigNum.Impl
-#
-# We use basename because we may also extract krml files from .fsti.checked
-# files (not true for OCaml, we don't extract mlis from fstis).
 .PRECIOUS: obj/%.ml
 obj/%.ml:
-	$(FSTAR) $(notdir $(subst .checked,,$<)) --codegen OCaml \
-	--extract_module $(basename $(notdir $(subst .checked,,$<)))
+	$(FSTAR) --codegen OCaml $< -o $@
 
+# By default, krml extraction in F* will extract every module into a
+# single out.krml file. Make sure to extract the single module we want.
 .PRECIOUS: obj/%.krml
 obj/%.krml:
-	$(FSTAR) $(notdir $(subst .checked,,$<)) --codegen krml \
-	--extract_module $(basename $(notdir $(subst .checked,,$<)))
+	$(FSTAR) $< --codegen krml \
+	--extract_module $(basename $(notdir $(subst .checked,,$<))) \
+	-o $@
 
 obj/Specs_Driver.ml: specs/ml/Specs_Driver.ml
 	# This ensures that all the source directories are not polluted with
diff --git a/include/krml/internal/target.h b/include/krml/internal/target.h
index f385010d..c5922146 100644
--- a/include/krml/internal/target.h
+++ b/include/krml/internal/target.h
@@ -76,7 +76,7 @@
 #endif
 
 #ifndef KRML_MAYBE_UNUSED
-#  if defined(__GNUC__)
+#  if defined(__GNUC__) || defined(__clang__)
 #    define KRML_MAYBE_UNUSED __attribute__((unused))
 #  else
 #    define KRML_MAYBE_UNUSED
@@ -84,7 +84,7 @@
 #endif
 
 #ifndef KRML_ATTRIBUTE_TARGET
-#  if defined(__GNUC__)
+#  if defined(__GNUC__) || defined(__clang__)
 #    define KRML_ATTRIBUTE_TARGET(x) __attribute__((target(x)))
 #  else
 #    define KRML_ATTRIBUTE_TARGET(x)
@@ -92,10 +92,10 @@
 #endif
 
 #ifndef KRML_NOINLINE
-#  if defined(_MSC_VER)
-#    define KRML_NOINLINE __declspec(noinline)
-#  elif defined (__GNUC__)
+#  if defined (__GNUC__) || defined (__clang__)
 #    define KRML_NOINLINE __attribute__((noinline,unused))
+#  elif defined(_MSC_VER)
+#    define KRML_NOINLINE __declspec(noinline)
 #  elif defined (__SUNPRO_C)
 #    define KRML_NOINLINE __attribute__((noinline))
 #  else
diff --git a/krmllib/Makefile b/krmllib/Makefile
index 1cbb6fe9..d119c012 100644
--- a/krmllib/Makefile
+++ b/krmllib/Makefile
@@ -36,7 +36,7 @@ ifneq ($(RESOURCEMONITOR),)
   RUNLIM = runlim -p -o $@.runlim
 endif
 
-FSTAR = $(RUNLIM) $(FSTAR_EXE) $(FSTAR_OPTIONS) --cache_checked_modules --cache_dir obj \
+FSTAR = $(RUNLIM) $(FSTAR_EXE) $(FSTAR_OPTIONS) --cache_dir obj \
   $(addprefix --include , $(INCLUDE_PATHS)) --cmi \
   --already_cached 'Prims FStar -FStar.Krml.Endianness LowStar -LowStar.Lib'
 
@@ -64,7 +64,7 @@ FSTAR_EXTRACT+=-FStar.Stubs # This namespace is for interfaces into the compiler
 ifndef NODEPEND
 ifndef MAKE_RESTARTS
 .depend: .FORCE obj
-	$(FSTAR) $(OTHERFLAGS) --extract '$(FSTAR_EXTRACT)' --dep full $(ROOTS) --output_deps_to $@
+	$(FSTAR) $(OTHERFLAGS) --extract '$(FSTAR_EXTRACT)' --dep full $(ROOTS) -o $@
 
 .PHONY: .FORCE
 .FORCE:
@@ -77,15 +77,15 @@ obj:
 	mkdir $@
 
 %.checked: | obj
-	$(FSTAR) $(OTHERFLAGS) $< && \
+	$(FSTAR) $(OTHERFLAGS) -c $< -o $@ && \
 	touch $@
 
 verify-all: $(ALL_CHECKED_FILES)
 
 $(EXTRACT_DIR)/%.krml: | .depend
-	$(FSTAR) $(OTHERFLAGS) --codegen krml \
+	$(FSTAR) $(OTHERFLAGS) $< --codegen krml \
 	  --extract_module $(basename $(notdir $(subst .checked,,$<))) \
-	  $(notdir $(subst .checked,,$<)) && \
+	  -o $@ && \
 	touch -c $@
 
 # We don't extract LowStar.Lib as everything is generic data structures that
diff --git a/lib/AstToMiniRust.ml b/lib/AstToMiniRust.ml
index 529b69fb..f34a2c5f 100644
--- a/lib/AstToMiniRust.ml
+++ b/lib/AstToMiniRust.ml
@@ -412,8 +412,30 @@ let compress_prefix prefix =
 
 (* Types *)
 
+(* This is the name translation facility for things that are missing from the scope; typically,
+   external definitions that are to be implemented by hand.
+
+   Some background (current as of Feb 2025): things that *do* have a definition end up with Rust
+   name crate::foo::bar where `foo` is the file that the definition got assigned to, and `bar` is
+   the last component of the `lident`. So, for instance, if Hacl.Streaming.Keccak.hash_len ends up
+   in Rust *file* hash_sha3.rs, then it becomes crate::hash_sha3::hash_len and is emitted as `fn
+   hash_len` within that file. The environment knows about this. Notably, this means that
+   rename-prefix is completely ignored for Rust, for good reason -- there is a better namespacing
+   story.
+
+   Now for things that are completely external (e.g. assumed library, like LowStar.Endianness), this
+   is a different story -- how do we meaningfully steer the name generation towards the naming
+   scheme we *would like*?
+
+   So, here, for things that do not get the nice Rust namespacing, we *do* honor rename-prefix to
+   give the user a little more control over how things get emitted when they don't have definitions
+   in scope.*)
 let translate_unknown_lid (m, n) =
-  let m = compress_prefix m in
+  let m =
+    match GlobalNames.rename_prefix (m, n) with
+    | Some m -> [ m ]
+    | None -> compress_prefix m
+  in
   List.map String.lowercase_ascii m @ [ n ]
 
 let borrow_kind_of_bool b: MiniRust.borrow_kind =
@@ -483,7 +505,7 @@ let translate_type env = translate_type_with_config env default_config
 (* Expressions *)
 
 (* Allocate a target Rust name for a definition named `lid` pertaining to file
-   (i.e. future rust module) `prefix`.
+   (i.e. future rust module) `env.prefix`.
 
    We do something super simple: we only retain the last component of `lid` and
    prefix it with the current namespace. This ensures that at Rust
diff --git a/lib/Driver.ml b/lib/Driver.ml
index 1af728b5..b7334463 100644
--- a/lib/Driver.ml
+++ b/lib/Driver.ml
@@ -6,34 +6,40 @@
 
 open Warn
 
-(* Abstracting over - (dash) for msvc. vs. gcc-like. *)
+(** These three filled in by [detect_cc] and others *)
+let cc = ref ""
+let cc_args = ref []
+let cc_flavor = ref Options.Generic
+
+(* Abstracting over - (dash) for msvc. vs. gcc-like. This module
+ reads cc_flavor. *)
 module Dash = struct
   let i dir =
-    if !Options.cc = "msvc" then
+    if !cc_flavor = MSVC then
       [ "/I"; dir ]
     else
       [ "-I"; dir ]
 
   let c file =
-    if !Options.cc = "msvc" then
+    if !cc_flavor = MSVC then
       [ "/c"; file ]
     else
       [ "-c"; file ]
 
   let d opt =
-    if !Options.cc = "msvc" then
+    if !cc_flavor = MSVC then
       "/D" ^ opt
     else
       "-D" ^ opt
 
   let o_obj file =
-    if !Options.cc = "msvc" then
+    if !cc_flavor = MSVC then
       [ "/Fo:"; file ]
     else
       [ "-o"; file ]
 
   let o_exe file =
-    if !Options.cc = "msvc" then
+    if !cc_flavor = MSVC then
       [ "/Fe:"; file ]
     else
       [ "-o"; file ]
@@ -44,6 +50,8 @@ module P = Process
 (* Note: don't open [Process], otherwise any reference to [Output] will be
  * understood as a cyclic dependency on our own [Output] module. *)
 
+let cc_flavor_callback = ref (fun (_ : Options.compiler_flavor) -> ())
+
 (** These three variables filled in by [detect_fstar] *)
 let fstar = Options.fstar
 let fstar_lib = ref ""
@@ -57,10 +65,6 @@ let include_dir = ref ""
 let misc_dir = ref ""
 let krml_rev = ref "<unknown>"
 
-(** These two filled in by [detect_gcc] and others *)
-let cc = ref ""
-let cc_args = ref []
-
 (** The base tools *)
 let readlink = ref ""
 
@@ -339,41 +343,46 @@ let run_fstar verify skip_extract skip_translate files =
       exit 0;
     !Options.tmpdir ^^ "out.krml"
 
-let detect_gnu flavor =
-  if not !Options.silent then
-    KPrint.bprintf "%s⚙ KaRaMeL will drive the C compiler.%s Here's what we found:\n" Ansi.blue Ansi.reset;
-  let rec search = function
-    | fmt :: rest ->
-        let cmd = KPrint.bsprintf fmt flavor in
-        if success "which" [| cmd |] then
-          cc := cmd
-        else
-          search rest
-    | [] ->
-        Warn.fatal_error "gcc not found in path!";
+let detect_compiler_flavor cc =
+  let is_gcc () =
+    try
+      (* If cc points to gcc, cc --version will say "cc version ...", instead of
+      gcc. So use -v instead, but that prints to stderr. *)
+      let rc = Process.run cc [| "-v" |] in
+      let lines = rc.stderr in
+      List.exists (fun l -> KString.starts_with l "gcc version") lines
+    with | _ -> false
   in
-  let crosscc = if !Options.m32 then format_of_string "i686-w64-mingw32-%s" else format_of_string "x86_64-w64-mingw32-%s" in
-  search [ "%s-10"; "%s-9"; "%s-8"; "%s-7"; "%s-6"; "%s-5"; crosscc; "%s" ];
-
-  if not !Options.silent then
-    KPrint.bprintf "%sgcc is:%s %s\n" Ansi.underline Ansi.reset !cc;
-
-  if !Options.m32 then
-    cc_args := "-m32" :: !cc_args;
-  if not !Options.silent then
-    KPrint.bprintf "%s%s options are:%s %s\n" Ansi.underline !cc Ansi.reset
-      (String.concat " " !cc_args)
-
-
-let detect_compcert () =
-  if success "which" [| "ccomp" |] then
-    cc := "ccomp"
-  else
-    Warn.fatal_error "ccomp not found in path!"
-
+  let is_clang () =
+    try
+      let lines = Process.read_stdout cc [| "--version" |] in
+      List.exists (fun l -> KString.exists l "clang version") lines
+    with | _ -> false
+  in
+  let is_compcert () =
+    try
+      let lines = Process.read_stdout cc [| "--version" |] in
+      List.exists (fun l -> KString.exists l "CompCert") lines
+    with | _ -> false
+  in
+  let is_msvc () =
+    try
+      let rc = Process.run cc [| |] in
+      let lines = rc.stderr in
+      List.exists (fun l -> KString.exists l "Microsoft") lines
+    with | _ -> false
+  in
+  if is_gcc ()           then Options.GCC
+  else if is_clang ()    then Options.Clang
+  else if is_compcert () then Options.Compcert
+  else if is_msvc ()     then Options.MSVC
+  else (
+    Warn.maybe_fatal_error ("detect_compiler_flavor", UnrecognizedCCompiler cc);
+    Generic
+  )
 
 let fill_cc_args () =
-  (** For the side-effect of filling in [Options.include] *)
+  (** For the side-effect of filling in [Options.includes] *)
   detect_karamel_if ();
 
   cc_args :=
@@ -383,26 +392,83 @@ let fill_cc_args () =
     @ List.rev !Options.ccopts
     @ !cc_args
 
+(* Sets cc, cc_flavor *)
+let auto_detect_cc () =
+  (* !cc can be relative or absolute, `which` handles both. *)
+  if not (success "which" [| !cc |]) then
+    Warn.fatal_error "C compiler '%s' not found!" !cc;
+
+  if not !Options.silent then begin
+    (* If not absolute print realpath too *)
+    let real =
+      if KString.starts_with !cc "/" then
+        ""
+      else
+        match
+          read_one_line !readlink [| "-f"; read_one_line "which" [| !cc |] |]
+        with
+        | exception _ -> " (couldn't resolve?)"
+        | s -> " (= " ^ s ^ ")"
+    in
+    KPrint.bprintf "%scc is:%s %s%s\n" Ansi.underline Ansi.reset !cc real
+  end;
+  match !Options.cc_flavor with
+  | Some f -> cc_flavor := f
+  | None ->   cc_flavor := detect_compiler_flavor !cc
+
+let detect_cc () =
+  detect_base_tools_if ();
+
+  if not !Options.silent then
+    KPrint.bprintf "%s⚙ KaRaMeL will drive the C compiler.%s Here's what we found:\n" Ansi.blue Ansi.reset;
+
+  (* Use Options.cc if passed, otherwise CC from env, otherwise "cc" *)
+  let cc_name =
+    if !Options.cc <> ""
+    then !Options.cc
+    else
+      match Sys.getenv "CC" with
+      | s -> s
+      | exception _ -> "cc"
+  in
+
+  if cc_name = "msvc" then (
+    (* We special-case "msvc" and use this wrapper script to find it
+       and set its environment up, it's not really feasible to
+       just find the cl.exe *)
+    KPrint.bprintf "%scc is:%s MSVC (will use cl-wrapper script)\n" Ansi.underline Ansi.reset;
+    cc := !misc_dir ^^ "cl-wrapper.bat";
+    cc_flavor := MSVC
+  ) else (
+    (* Otherwise cc_name is a normal command or path like gcc/clang,
+       auto-detect its flavor. *)
+    cc := cc_name;
+    auto_detect_cc ()
+  );
+
+  if not !Options.silent then
+    KPrint.bprintf "%scc flavor is:%s %s\n" Ansi.underline Ansi.reset
+      (Options.string_of_compiler_flavor !cc_flavor);
+
+  (* Now that we detected the flavor, call this callback to
+     right default arguments for the compiler filled in. *)
+  !cc_flavor_callback !cc_flavor;
 
-let detect_cc_if () =
   fill_cc_args ();
+
+  if !cc_flavor = GCC && !Options.m32 then
+    cc_args := "-m32" :: !cc_args;
+
+  if not !Options.silent then
+    KPrint.bprintf "%scc options are:%s %s\n" Ansi.underline Ansi.reset
+      (String.concat " " !cc_args)
+
+let detect_cc_if () =
   if !cc = "" then
-    match !Options.cc with
-    | "gcc" ->
-        detect_gnu "gcc"
-    | "compcert" ->
-        detect_compcert ()
-    | "g++" ->
-        detect_gnu "g++"
-    | "clang" ->
-        detect_gnu "clang"
-    | "msvc" ->
-        cc := !misc_dir ^^ "cl-wrapper.bat";
-    | _ ->
-        fatal_error "Unrecognized value for -cc: %s" !Options.cc
+    detect_cc ()
 
 let o_of_c f =
-  let dot_o = if !Options.cc = "msvc" then ".obj" else ".o" in
+  let dot_o = if !cc_flavor = MSVC then ".obj" else ".o" in
   !Options.tmpdir ^^ Filename.chop_suffix (Filename.basename f) ".c" ^ dot_o
 
 
diff --git a/lib/Error.ml b/lib/Error.ml
index 513ece48..70835db3 100644
--- a/lib/Error.ml
+++ b/lib/Error.ml
@@ -35,6 +35,7 @@ and raw_error =
   | IfDefOnGlobal of lident
   | NotLowStarCast of expr
   | LibraryPointerAmbiguity of lident * expr
+  | UnrecognizedCCompiler of string
 
 and location =
   string
diff --git a/lib/GlobalNames.mli b/lib/GlobalNames.mli
index fc60213b..bdfec31c 100644
--- a/lib/GlobalNames.mli
+++ b/lib/GlobalNames.mli
@@ -34,3 +34,5 @@ val camel_case: string -> string
 val skip_prefix: Ast.lident -> bool
 
 val keywords: string list
+
+val rename_prefix: Ast.lident -> string option
diff --git a/lib/Options.ml b/lib/Options.ml
index fb344505..c2341d22 100644
--- a/lib/Options.ml
+++ b/lib/Options.ml
@@ -3,6 +3,28 @@
 
 type include_ = All | InternalOnly of string | HeaderOnly of string | COnly of string
 
+type compiler_flavor =
+  | Generic
+  | GCC
+  | Clang
+  | Compcert
+  | MSVC
+
+let string_of_compiler_flavor = function
+  | Generic -> "generic"
+  | GCC -> "gcc"
+  | Clang -> "clang"
+  | Compcert -> "compcert"
+  | MSVC -> "msvc"
+
+let compiler_flavor_of_string = function
+  | "generic" -> Generic
+  | "gcc" -> GCC
+  | "clang" -> Clang
+  | "compcert" -> Compcert
+  | "msvc" -> MSVC
+  | s -> failwith ("unrecognized compiler flavor: " ^ s)
+
 let pinc b = function
   | All -> Buffer.add_string b "*"
   | InternalOnly h
@@ -23,13 +45,14 @@ let fstar = ref "fstar.exe" (* F* command to use *)
 let add_include: (include_ * string) list ref = ref [ ]
 let add_include_tmh = ref false
 let add_early_include: (include_ * string) list ref = ref [ ]
-let warn_error = ref "+1@2@3+4..8@9+10@11+12..18@19+20..22+24..25@26@27"
+let warn_error = ref "+1@2@3+4..8@9+10@11+12..18@19+20..22+24..25@26..28"
 let tmpdir = ref "."
 let includes: string list ref = ref []
 let verbose = ref false
 let silent = ref false
 let exe_name = ref ""
-let cc = ref "gcc"
+let cc = ref ""
+let cc_flavor : compiler_flavor option ref = ref None
 let m32 = ref false
 let fsopts: string list ref = ref []
 let ccopts: string list ref = ref []
@@ -92,8 +115,8 @@ let c89_std = ref false
 let c89_scope = ref false
 
 (* A set of extra command-line arguments one gets for free depending on the
- * value of -cc *)
-let default_options () =
+ * detected C compiler. *)
+let default_options (k : compiler_flavor) =
   (* Note: the 14.04 versions of Ubuntu rely on the presence of _BSD_SOURCE to
    * enable the macros in endian.h; future versions use _DEFAULT_SOURCE which is
    * enabled by default, it seems, but there are talks of issuing a warning if
@@ -109,21 +132,20 @@ let default_options () =
   let gcc_options = Array.append gcc_like_options
     [| "-ccopt"; if !c89_std then "-std=c89" else "-std=c11" |]
   in
-  [
-    "gcc", gcc_options;
-    "clang", gcc_options;
-    "g++", gcc_like_options;
-    "compcert", [|
+  match k with
+  | GCC | Clang ->
+    if !cxx_compat
+    then gcc_like_options
+    else gcc_options
+  | Compcert -> [|
       "-warn-error"; "@6@8";
       "-fnostruct-passing"; "-fnoanonymous-unions";
       "-ccopts"; "-g,-D_BSD_SOURCE,-D_DEFAULT_SOURCE";
-    |];
-    "msvc", [|
+    |]
+  | MSVC -> [|
       "-warn-error"; "+6"; "-falloca"
-    |];
-    "", [| |]
-  ]
-
+    |]
+  | Generic -> [| |]
 
 (** Drop is now deprecated and there is not a single situation left that calls
     for it. If you must implement something with macros or static inline (i.e.,
diff --git a/lib/Warn.ml b/lib/Warn.ml
index a511e933..0ee0cf85 100644
--- a/lib/Warn.ml
+++ b/lib/Warn.ml
@@ -45,7 +45,7 @@ let failwith fmt =
 
 (* The main error printing function. *)
 
-let flags = Array.make 28 CError;;
+let flags = Array.make 29 CError;;
 
 (* When adding a new user-configurable error, there are *several* things to
  * update:
@@ -108,6 +108,8 @@ let errno_of_error = function
       26
   | LibraryPointerAmbiguity _ ->
       27
+  | UnrecognizedCCompiler _ ->
+      28
   | _ ->
       (** Things that cannot be silenced! *)
       0
@@ -216,6 +218,8 @@ let rec perr buf (loc, raw_error) =
       -library; and its definition is too ambiguous to tell whether it's an \
       array or a pointer. Disabling this warning is unsound. Definition \
       below:\n%a" plid lid pexpr e
+  | UnrecognizedCCompiler cc ->
+      p "Unrecognized C compiler: %s" cc
 
 let maybe_fatal_error error =
   flush stdout;
diff --git a/src/Karamel.ml b/src/Karamel.ml
index 44e6ef73..35374c74 100644
--- a/src/Karamel.ml
+++ b/src/Karamel.ml
@@ -65,7 +65,6 @@ let _ =
   let js_files = ref [] in
   let fst_files = ref [] in
   let filenames = ref [] in
-  let p k = String.concat " " (Array.to_list (List.assoc k (Options.default_options ()))) in
   let usage = Printf.sprintf
 {|KaRaMeL: from a ML-like subset to C
 
@@ -137,12 +136,11 @@ All include directories and paths supports special prefixes:
   - if a path starts with FSTAR_LIB, this will expand to wherever F*'s ulib
     directory is
 
-The compiler switches turn on the following options.
-  [-cc gcc] (default) adds [%s]
-  [-cc clang] adds [%s]
-  [-cc g++] adds [%s]
-  [-cc msvc] adds [%s]
-  [-cc compcert] adds [%s]
+Karamel will also enable some default options according to the the flavor of C
+compiler being used.
+%s
+If the compiler flavor cannot be detected (and you ignore this error) no flags
+will be added. You can force a flavor with the -ccflavor option.
 
 The [-fc89] option triggers [-fnoanonymous-unions], [-fnocompound-literals] and
 [-fc89-scope]. It also changes the invocations above to use [-std=c89]. Note
@@ -162,11 +160,13 @@ Supported options:|}
     ) !Options.bundle @ List.concat_map (fun p ->
       [ "-drop"; Bundle.string_of_pattern p ]
     ) !Options.drop))
-    (p "gcc")
-    (p "clang")
-    (p "g++")
-    (p "msvc")
-    (p "compcert")
+    (
+      let open Options in
+      let flavors = [GCC; Clang; Compcert; MSVC] in
+      let p k = String.concat " " (Array.to_list (Options.default_options k)) in
+      String.concat "\n" (
+      List.map (fun k -> KPrint.bsprintf "  For %s adds [%s]" (Options.string_of_compiler_flavor k) (p k)) flavors)
+    )
   in
   let found_file = ref false in
   let used_drop = ref false in
@@ -196,8 +196,12 @@ Supported options:|}
     (* KaRaMeL as a driver *)
     "-fstar", Arg.Set_string Options.fstar, " fstar.exe to use; defaults to \
       'fstar.exe'";
-    "-cc", Arg.Set_string Options.cc, " compiler to use; one of gcc (default), \
-      compcert, g++, clang, msvc";
+    "-cc", Arg.Set_string Options.cc, " compiler to use; default is 'cc', \
+      you can also set the CC environment variable";
+    "-ccflavor", Arg.String (fun s ->
+        let flav = Options.compiler_flavor_of_string s in
+        Options.cc_flavor := Some flav), " C compiler flavor; normally autodetected, \
+        can be set to 'gcc', 'clang', 'compcert', 'msvc' or 'generic'";
     "-m32", Arg.Set Options.m32, " turn on 32-bit cross-compiling";
     "-fsopt", Arg.String (prepend Options.fsopts), " option to pass to F* (use \
       -fsopts to pass a comma-separated list of values)";
@@ -490,14 +494,6 @@ Supported options:|}
     Options.ccopts := Driver.Dash.d "KRML_VERIFIED_UINT128" :: !Options.ccopts
   end;
 
-  (* Then, bring in the "default options" for each compiler. *)
-  let ccopts = !Options.ccopts in
-  Options.ccopts := [];
-  Arg.parse_argv ~current:(ref 0)
-    (Array.append [| Sys.argv.(0) |] (List.assoc !Options.cc (Options.default_options ())))
-    spec anon_fun usage;
-  Options.ccopts := ccopts @ !Options.ccopts;
-
   (* Then refine that based on the user's preferences. *)
   if !arg_warn_error <> "" then
     Warn.parse_warn_error !arg_warn_error;
@@ -831,6 +827,20 @@ Supported options:|}
 
     if !arg_skip_compilation then
       exit 0;
+
+    let cc_flavor_callback (k : Options.compiler_flavor) : unit =
+      (* With the compiler flavor detected, add the default options for the compiler.
+         We just call the option parser again to process the default_options. *)
+      let ccopts = !Options.ccopts in
+      Options.ccopts := [];
+      Arg.parse_argv ~current:(ref 0)
+        (Array.append [| Sys.argv.(0) |] (Options.default_options k))
+        spec anon_fun usage;
+      Options.ccopts := ccopts @ !Options.ccopts;
+    in
+
+    Driver.cc_flavor_callback := cc_flavor_callback;
+
     let remaining_c_files = Driver.compile (List.map fst files) !c_files in
 
     if !arg_skip_linking then
diff --git a/test/Makefile b/test/Makefile
index 66469537..59293ba0 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -74,7 +74,7 @@ OUTPUT_DIR	= .output
 ifneq ($(CRYPTO),)
   INCLUDE_CRYPTO=--include $(CRYPTO)
 endif
-FSTAR		= $(FSTAR_EXE) --cache_checked_modules \
+FSTAR		= $(FSTAR_EXE) \
   --cache_dir $(CACHE_DIR) --odir $(OUTPUT_DIR) \
   --include hello-system --include ../krmllib/compat --include ../krmllib/obj \
   --include ../krmllib --include ../runtime \
@@ -83,7 +83,7 @@ FSTAR		= $(FSTAR_EXE) --cache_checked_modules \
   --trivial_pre_for_unannotated_effectful_fns false \
   --cmi --warn_error -274
 
-all: $(FILES) rust $(WASM_FILES) $(CUSTOM) ctypes-test sepcomp-test
+all: $(FILES) rust $(WASM_FILES) $(CUSTOM) ctypes-test sepcomp-test rust-val-test
 
 # Needs node
 wasm: $(WASM_FILES)
@@ -99,7 +99,7 @@ ifndef MAKE_RESTARTS
 ifndef NODEPEND
 .depend: .FORCE
 	$(FSTAR) --dep full $(subst .wasm-test,.fst,$(WASM_FILES)) $(subst .test,.fst,$(FILES)) \
-	  $(BROKEN) ../runtime/WasmSupport.fst --extract 'krml:*,-Prims' --output_deps_to $@
+	  $(BROKEN) ../runtime/WasmSupport.fst --extract 'krml:*,-Prims' -o $@
 
 .PHONY: .FORCE
 .FORCE:
@@ -109,13 +109,14 @@ endif
 include .depend
 
 $(CACHE_DIR)/%.checked: | .depend
-	$(FSTAR) $(OTHERFLAGS) $< && \
+	$(FSTAR) $(OTHERFLAGS) -c $< -o $@ && \
 	touch $@
 
 $(OUTPUT_DIR)/%.krml: | .depend
 	$(FSTAR) $(OTHERFLAGS) --codegen krml \
 	  --extract_module $(basename $(notdir $(subst .checked,,$<))) \
-	  $(notdir $(subst .checked,,$<))
+	  -o $@ \
+	  $<
 
 ###############
 # Regular (C) #
@@ -266,6 +267,10 @@ sepcomp-test:
 	+$(MAKE) -C sepcomp
 .PHONY: sepcomp-test
 
+rust-val-test:
+	+$(MAKE) -C rust-val
+.PHONY: rust-val-test
+
 CTYPES_HAND_WRITTEN_FILES=Client.ml Makefile
 
 .PHONY: $(LOWLEVEL_DIR)/Client.native
diff --git a/test/rust-val/.gitignore b/test/rust-val/.gitignore
new file mode 100644
index 00000000..6643cd43
--- /dev/null
+++ b/test/rust-val/.gitignore
@@ -0,0 +1,3 @@
+*.exe
+*.krml
+rusttest.rs
diff --git a/test/rust-val/AuxA.fsti b/test/rust-val/AuxA.fsti
new file mode 100644
index 00000000..ab39c8b4
--- /dev/null
+++ b/test/rust-val/AuxA.fsti
@@ -0,0 +1,4 @@
+module AuxA
+
+val foo : bool -> bool
+
diff --git a/test/rust-val/AuxB.fsti b/test/rust-val/AuxB.fsti
new file mode 100644
index 00000000..5f2e4f03
--- /dev/null
+++ b/test/rust-val/AuxB.fsti
@@ -0,0 +1,3 @@
+module AuxB
+
+val bar : bool -> bool
diff --git a/test/rust-val/Makefile b/test/rust-val/Makefile
new file mode 100644
index 00000000..71da305a
--- /dev/null
+++ b/test/rust-val/Makefile
@@ -0,0 +1,70 @@
+RECENT_GCC	= $(shell [ "$$(gcc -dumpversion | cut -c -1)" -ge 5 ] && echo yes)
+
+ifeq (3.81,$(MAKE_VERSION))
+  $(error You seem to be using the OSX antiquated Make version. Hint: brew \
+    install make, then invoke gmake instead of make)
+endif
+
+FSTAR_EXE ?= fstar.exe
+
+TEST_OPTS	= -warn-error @4 -verbose -skip-makefiles
+KRML_BIN	= ../../_build/default/src/Karamel.exe
+KRML		= $(KRML_BIN) -fstar $(FSTAR_EXE) $(KOPTS) $(TEST_OPTS)
+CACHE_DIR	= .cache
+FSTAR		= $(FSTAR_EXE) --cache_checked_modules \
+  --cache_dir $(CACHE_DIR) \
+  --include ../../krmllib/compat --include ../../krmllib/obj \
+  --include ../../krmllib --include ../../runtime \
+  --ext context_pruning \
+  --already_cached 'Prims FStar C TestLib Spec.Loops -C.Compat -C.Nullity LowStar WasmSupport' \
+  --trivial_pre_for_unannotated_effectful_fns false \
+  --cmi --warn_error -274
+SED=$(shell which gsed >/dev/null 2>&1 && echo gsed || echo sed)
+
+all: rusttest.rust-test impl
+
+impl:
+	+$(MAKE) -C $@
+
+.PHONY: impl
+
+FSTAR_FILES=$(wildcard *.fst *.fsti)
+
+.PRECIOUS: %.krml
+
+# Use F*'s dependency mechanism and fill out the missing rules.
+
+ifndef MAKE_RESTARTS
+ifndef NODEPEND
+.depend: .FORCE
+	$(FSTAR) --dep full $(FSTAR_FILES) --extract 'krml:*,-Prims' --output_deps_to $@
+
+.PHONY: .FORCE
+.FORCE:
+endif
+endif
+
+include .depend
+
+$(CACHE_DIR)/%.checked: | .depend
+	$(FSTAR) $(OTHERFLAGS) $< && \
+	touch $@
+
+%.krml: | .depend
+	$(FSTAR) $(OTHERFLAGS) --codegen krml \
+	  --extract_module $(basename $(notdir $(subst .checked,,$<))) \
+	  $(notdir $(subst .checked,,$<))
+
+########
+# Rust #
+########
+
+.PRECIOUS: %.rs
+%.rs: $(ALL_KRML_FILES) $(KRML_BIN)
+	$(KRML) -minimal -bundle AuxA+AuxB=[rename=Aux,rename-prefix] -bundle $(notdir $(subst rust,Rust,$*))=\* \
+	  -backend rust $(EXTRA) -tmpdir $(dir $@) $(filter %.krml,$^)
+	$(SED) -i 's/\(patterns..\)/\1\nmod aux; mod lowstar { pub mod ignore { pub fn ignore<T>(_x: T) {}}}\n/' $@
+	echo 'fn main () { let r = main_ (); if r != 0 { println!("main_ returned: {}\\n", r); panic!() } }' >> $@
+
+%.rust-test: %.rs
+	rustc $< -o $*.exe && ./$*.exe
diff --git a/test/rust-val/Rusttest.fst b/test/rust-val/Rusttest.fst
new file mode 100644
index 00000000..5adc5ef5
--- /dev/null
+++ b/test/rust-val/Rusttest.fst
@@ -0,0 +1,24 @@
+module Rusttest
+
+module B = LowStar.Buffer
+module HST = FStar.HyperStack.ST
+module I32 = FStar.Int32
+
+let test2 (b: B.buffer bool) : HST.Stack bool
+  (fun h -> B.live h b /\ B.length b == 1)
+  (fun _ _ _ -> True)
+=
+  let x = B.index b C._zero_for_deref in
+  let r1 = AuxA.foo x in
+  let r2 = AuxB.bar x in
+  r1 && r2
+
+let main_ () : HST.Stack I32.t
+  (fun _ -> True)
+  (fun _ _ _ -> True)
+= 
+  HST.push_frame ();
+  let b = B.alloca true 1ul in
+  let _ = test2 b in
+  HST.pop_frame ();
+  0l
diff --git a/test/rust-val/aux.rs b/test/rust-val/aux.rs
new file mode 100644
index 00000000..9a4f8903
--- /dev/null
+++ b/test/rust-val/aux.rs
@@ -0,0 +1,15 @@
+#![allow(non_snake_case)]
+#![allow(non_upper_case_globals)]
+#![allow(non_camel_case_types)]
+#![allow(unused_assignments)]
+#![allow(unreachable_patterns)]
+
+pub fn foo(x: bool) -> bool
+{
+    return !x;
+}
+
+pub fn bar(x: bool) -> bool
+{
+    return x;
+}
diff --git a/test/rust-val/impl/.gitignore b/test/rust-val/impl/.gitignore
new file mode 100644
index 00000000..a3976a52
--- /dev/null
+++ b/test/rust-val/impl/.gitignore
@@ -0,0 +1,2 @@
+*.rs
+*.rlib
diff --git a/test/rust-val/impl/AuxA.fst b/test/rust-val/impl/AuxA.fst
new file mode 100644
index 00000000..efd7fc38
--- /dev/null
+++ b/test/rust-val/impl/AuxA.fst
@@ -0,0 +1,3 @@
+module AuxA
+
+let foo x = not x
diff --git a/test/rust-val/impl/AuxB.fst b/test/rust-val/impl/AuxB.fst
new file mode 100644
index 00000000..3ec633f7
--- /dev/null
+++ b/test/rust-val/impl/AuxB.fst
@@ -0,0 +1,3 @@
+module AuxB
+
+let bar x = x
diff --git a/test/rust-val/impl/Makefile b/test/rust-val/impl/Makefile
new file mode 100644
index 00000000..53d90cce
--- /dev/null
+++ b/test/rust-val/impl/Makefile
@@ -0,0 +1,64 @@
+RECENT_GCC	= $(shell [ "$$(gcc -dumpversion | cut -c -1)" -ge 5 ] && echo yes)
+
+ifeq (3.81,$(MAKE_VERSION))
+  $(error You seem to be using the OSX antiquated Make version. Hint: brew \
+    install make, then invoke gmake instead of make)
+endif
+
+FSTAR_EXE ?= fstar.exe
+
+TEST_OPTS	= -warn-error @4 -verbose -skip-makefiles
+KRML_BIN	= ../../../_build/default/src/Karamel.exe
+KRML		= $(KRML_BIN) -fstar $(FSTAR_EXE) $(KOPTS) $(TEST_OPTS)
+CACHE_DIR	= .cache
+FSTAR		= $(FSTAR_EXE) --cache_checked_modules \
+  --cache_dir $(CACHE_DIR) \
+  --include ../../../krmllib/compat --include ../../../krmllib/obj \
+  --include ../../../krmllib --include ../../../runtime \
+  --include .. \
+  --ext context_pruning \
+  --already_cached 'Prims FStar C TestLib Spec.Loops -C.Compat -C.Nullity LowStar WasmSupport' \
+  --trivial_pre_for_unannotated_effectful_fns false \
+  --cmi --warn_error -274
+SED=$(shell which gsed >/dev/null 2>&1 && echo gsed || echo sed)
+
+all: aux.rust-test
+
+FSTAR_FILES=$(wildcard *.fst *.fsti)
+
+.PRECIOUS: %.krml
+
+# Use F*'s dependency mechanism and fill out the missing rules.
+
+ifndef MAKE_RESTARTS
+ifndef NODEPEND
+.depend: .FORCE
+	$(FSTAR) --dep full $(FSTAR_FILES) --extract 'krml:*,-Prims' --output_deps_to $@
+
+.PHONY: .FORCE
+.FORCE:
+endif
+endif
+
+include .depend
+
+$(CACHE_DIR)/%.checked: | .depend
+	$(FSTAR) $(OTHERFLAGS) $< && \
+	touch $@
+
+%.krml: | .depend
+	$(FSTAR) $(OTHERFLAGS) --codegen krml \
+	  --extract_module $(basename $(notdir $(subst .checked,,$<))) \
+	  $(notdir $(subst .checked,,$<))
+
+########
+# Rust #
+########
+
+.PRECIOUS: %.rs
+%.rs: $(ALL_KRML_FILES) $(KRML_BIN)
+	$(KRML) -minimal -bundle AuxA+AuxB=\*[rename=Aux,rename-prefix] \
+	  -backend rust $(EXTRA) -tmpdir $(dir $@) $(filter %.krml,$^)
+
+%.rust-test: %.rs
+	rustc --crate-type rlib $< -o $*.rlib
diff --git a/test/sepcomp/a/Makefile b/test/sepcomp/a/Makefile
index e32e8cc3..1b496ec9 100644
--- a/test/sepcomp/a/Makefile
+++ b/test/sepcomp/a/Makefile
@@ -35,12 +35,11 @@ include Makefile.include
 # But also:
 # - --cmi, for cross-module inlining, a must-have for anyone who relies on
 #   inline_for_extraction in the presence of interfaces
-# - --cache_checked_modules to rely on a pre-built ulib and krmllib
-# - --cache_dir, to avoid polluting our generated build artifacts outside o
+# - --cache_dir, to place checked files there
 
 FSTAR_EXE ?= fstar.exe
 FSTAR_NO_FLAGS = $(FSTAR_EXE) \
-  --odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
+  --odir obj $(FSTAR_INCLUDES) --cmi \
   --already_cached 'Prims FStar LowStar C Spec.Loops TestLib WasmSupport' --warn_error '+241@247+285' \
   --cache_dir obj
 
@@ -63,7 +62,7 @@ FSTAR_ROOTS = $(wildcard $(addsuffix /*.fsti,$(SOURCE_DIRS))) \
 ifndef MAKE_RESTARTS
 obj/.depend: .FORCE
 	mkdir -p obj
-	$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) $(FSTAR_EXTRACT) --output_deps_to $@
+	$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) $(FSTAR_EXTRACT) -o $@
 
 .PHONY: .FORCE
 .FORCE:
@@ -106,32 +105,23 @@ obj:
 # up-to-date (checksum matches, file unchanged), but this will confuse
 # make and result in endless rebuilds. So, we touch that file.
 %.checked: | obj
-	$(FSTAR) $< $(FSTAR_FLAGS) && touch -c $@
+	$(FSTAR) $(FSTAR_FLAGS) -c $< -o $@ && touch -c $@
 
 # Extraction
 # ----------
 
-# A few mismatches here between the dependencies present in the .depend and the
-# expected F* invocation. In .depend:
-#
-# obj/Bignum_Impl.ml: obj/Bignum.Impl.fst.checked ... more dependencies ...
-#
-# But F* wants (remember that F* searches for source files anywhere on the
-# include path):
-#
-# fstar Bignum.Impl.fst --extract_module BigNum.Impl
-#
-# We use basename because we may also extract krml files from .fsti.checked
-# files (not true for OCaml, we don't extract mlis from fstis).
 .PRECIOUS: obj/%.ml
 obj/%.ml:
-	$(FSTAR) $(notdir $(subst .checked,,$<)) --codegen OCaml \
-	--extract_module $(basename $(notdir $(subst .checked,,$<)))
+	$(FSTAR) $< --codegen OCaml
 
+# By default, krml extraction in F* will extract every module into a
+# single out.krml file. Make sure to extract the single module we want
+# to get a single-properly named file.
 .PRECIOUS: obj/%.krml
 obj/%.krml:
-	$(FSTAR) $(notdir $(subst .checked,,$<)) --codegen krml \
-	--extract_module $(basename $(notdir $(subst .checked,,$<)))
+	$(FSTAR) $< --codegen krml \
+	--extract_module $(basename $(notdir $(subst .checked,,$<))) \
+	-o $@
 
 # F* --> C
 # --------
diff --git a/test/sepcomp/b/Makefile b/test/sepcomp/b/Makefile
index e8c20d86..1ef3b99b 100644
--- a/test/sepcomp/b/Makefile
+++ b/test/sepcomp/b/Makefile
@@ -37,12 +37,11 @@ include Makefile.include
 # But also:
 # - --cmi, for cross-module inlining, a must-have for anyone who relies on
 #   inline_for_extraction in the presence of interfaces
-# - --cache_checked_modules to rely on a pre-built ulib and krmllib
-# - --cache_dir, to avoid polluting our generated build artifacts outside o
+# - --cache_dir, to place checked files there
 
 FSTAR_EXE ?= fstar.exe
 FSTAR_NO_FLAGS = $(FSTAR_EXE) \
-  --odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
+  --odir obj $(FSTAR_INCLUDES) --cmi \
   --already_cached 'Prims FStar LowStar C Spec.Loops TestLib WasmSupport A' --warn_error '+241@247+285' \
   --cache_dir obj
 
@@ -65,7 +64,7 @@ FSTAR_ROOTS = $(wildcard $(addsuffix /*.fsti,$(SOURCE_DIRS))) \
 ifndef MAKE_RESTARTS
 obj/.depend: .FORCE
 	mkdir -p obj
-	$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) $(FSTAR_EXTRACT) --output_deps_to $@
+	$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) $(FSTAR_EXTRACT) -o $@
 
 .PHONY: .FORCE
 .FORCE:
@@ -108,32 +107,23 @@ obj:
 # up-to-date (checksum matches, file unchanged), but this will confuse
 # make and result in endless rebuilds. So, we touch that file.
 %.checked: | obj
-	$(FSTAR) $< $(FSTAR_FLAGS) && touch -c $@
+	$(FSTAR) $(FSTAR_FLAGS) -c $< -o $@ && touch -c $@
 
 # Extraction
 # ----------
 
-# A few mismatches here between the dependencies present in the .depend and the
-# expected F* invocation. In .depend:
-#
-# obj/Bignum_Impl.ml: obj/Bignum.Impl.fst.checked ... more dependencies ...
-#
-# But F* wants (remember that F* searches for source files anywhere on the
-# include path):
-#
-# fstar Bignum.Impl.fst --extract_module BigNum.Impl
-#
-# We use basename because we may also extract krml files from .fsti.checked
-# files (not true for OCaml, we don't extract mlis from fstis).
 .PRECIOUS: obj/%.ml
 obj/%.ml:
-	$(FSTAR) $(notdir $(subst .checked,,$<)) --codegen OCaml \
-	--extract_module $(basename $(notdir $(subst .checked,,$<)))
+	$(FSTAR) $< --codegen OCaml
 
+# By default, krml extraction in F* will extract every module into a
+# single out.krml file. Make sure to extract the single module we want
+# to get a single-properly named file.
 .PRECIOUS: obj/%.krml
 obj/%.krml:
-	$(FSTAR) $(notdir $(subst .checked,,$<)) --codegen krml \
-	--extract_module $(basename $(notdir $(subst .checked,,$<)))
+	$(FSTAR) $< --codegen krml \
+	--extract_module $(basename $(notdir $(subst .checked,,$<))) \
+	-o $@
 
 # F* --> C
 # --------