Module WitnessUtil.InvariantParser
type t = {genv : (string, GoblintCil.Cabs2cil.envdata * GoblintCil.Cil.location)
Stdlib.Hashtbl.t;global_vars : GoblintCil.Cil.varinfo list;
}val create : GoblintCil.Cil.file -> tval parse_cabs : string -> (GoblintCil.Cabs.expression, string) Stdlib.resultval parse_cil :
t ->
?check:bool ->
fundec:GoblintCil.Cil.fundec ->
loc:GoblintCil.Cil.location ->
GoblintCil.Cabs.expression ->
(GoblintCil.Cil.exp, string) Stdlib.result