From e6b67397ca5c75582cee310edf0f79900fb3daa4 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 2 Aug 2021 17:31:10 +0200
Subject: [PATCH] [kernel] Add a function to create a term from a varinfo
---
src/kernel_services/ast_queries/cil.ml | 2 ++
src/kernel_services/ast_queries/cil.mli | 4 ++++
2 files changed, 6 insertions(+)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 695600d6793..d1b79a6fedb 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 8f83ecbc8be..d1becd81e78 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
--
GitLab