Merge pull request #96 from goblint/check-exp

Add standalone expression AST checking

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

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