diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 695600d6793e3315cf8301ee56e07dade97e4744..d1b79a6fedb352a8138091d5ccf32606c3145864 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -4998,6 +4998,8 @@ let cvar_to_lvar vi = match vi.vlogic_var_assoc with
     vi.vlogic_var_assoc <- Some lv; lv
   | Some lv -> lv
 
+let cvar_to_term ~loc vi = tvar ~loc (cvar_to_lvar vi)
+
 let copyVarinfo (vi: varinfo) (newname: string) : varinfo =
   let vi' = Cil_const.copy_with_new_vid vi in
   vi'.vname <- newname;
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 8f83ecbc8bee2cb5310a838a341e18069184317a..d1becd81e78c77f38f492e668ac7d82f5cd20cc1 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -2281,6 +2281,10 @@ val stmt_of_instr_list : ?loc:location -> instr list -> stmtkind
     The returned logic variable is unique for a given C variable. *)
 val cvar_to_lvar : varinfo -> logic_var
 
+(** Convert a C variable into a logic term.
+    @since Frama-C+dev *)
+val cvar_to_term: loc:location -> varinfo -> term
+
 (** Make a temporary variable to use in annotations *)
 val make_temp_logic_var: logic_type -> logic_var