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