Frama-C API - Logic_parse_string
exception Error of Fileloc.t * stringFor the three functions below, env can be used to specify which logic labels are parsed. By default, only Here is accepted. All the C labels inside the function are also accepted, regardless of env. loc is used as the source for the beginning of the string. All three functions may raise Logic_interp.Error or Parsing.Parse_error.
val code_annot : Cil_types.kernel_function -> Cil_types.stmt -> string -> Cil_types.code_annotationval term_lval : Cil_types.kernel_function -> ?loc:Fileloc.t -> ?env:Logic_typing.Lenv.t -> string -> Cil_types.term_lvalval term : Cil_types.kernel_function -> ?loc:Fileloc.t -> ?env:Logic_typing.Lenv.t -> string -> Cil_types.termval predicate : Cil_types.kernel_function -> ?loc:Fileloc.t -> ?env:Logic_typing.Lenv.t -> string -> Cil_types.predicate