From bbfc0b3a3a2604f6a7e8060082ba29e3b61f8d47 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 25 May 2022 10:47:47 +0300
Subject: [PATCH] Add Check.checkStandaloneExp

---
 src/check.ml  | 25 ++++++++++++++++++++++++-
 src/check.mli |  2 ++
 2 files changed, 26 insertions(+), 1 deletion(-)

diff --git a/src/check.ml b/src/check.ml
index 1c7af61d2..4554c2b20 100644
--- a/src/check.ml
+++ b/src/check.ml
@@ -79,7 +79,7 @@ let checkAttributes (attrs: attribute list) : unit =
 
 
   (* Keep track of defined types *)
-let typeDefs : (string, typ) H.t = H.create 117
+let typeDefs : (string, typ) H.t = H.create 117 (* TODO: unused *)
 
 
   (* Keep track of all variables names, enum tags and type names *)
@@ -1086,3 +1086,26 @@ let checkFile flags fl =
   if !E.verboseFlag then
     ignore (E.log "Finished checking file %s\n" fl.fileName);
   !valid
+
+
+let checkStandaloneExp ~(vars: varinfo list) (exp: exp) =
+  if !E.verboseFlag then ignore (E.log "Checking exp %a\n" d_exp exp);
+  valid := true;
+  List.iter defineVariable vars;
+
+  (try ignore (checkExp false exp) with _ -> ());
+
+  (* Clean the hashes to let the GC do its job *)
+  H.clear typeDefs;
+  H.clear varNamesEnv;
+  H.clear varIdsEnv;
+  H.clear allVarIds;
+  H.clear fundecForVarIds;
+  H.clear compNames;
+  H.clear compUsed;
+  H.clear enumUsed;
+  H.clear typUsed;
+  varNamesList := [];
+  if !E.verboseFlag then
+    ignore (E.log "Finished checking exp %a\n" d_exp exp);
+  !valid
diff --git a/src/check.mli b/src/check.mli
index 69c681ee2..73c21cd67 100644
--- a/src/check.mli
+++ b/src/check.mli
@@ -45,3 +45,5 @@ type checkFlags =
                        (** Ignore the specified instructions *)
  
 val checkFile: checkFlags list -> Cil.file -> bool
+
+val checkStandaloneExp: vars:Cil.varinfo list -> Cil.exp -> bool