Frama_c_kernel.Logic_parse_string
exception Error of Cil_types.location * string
For 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_annotation
val term_lval :
Cil_types.kernel_function ->
?loc:Cil_types.location ->
?env:Logic_typing.Lenv.t ->
string ->
Cil_types.term_lval
val term :
Cil_types.kernel_function ->
?loc:Cil_types.location ->
?env:Logic_typing.Lenv.t ->
string ->
Cil_types.term
val predicate :
Cil_types.kernel_function ->
?loc:Cil_types.location ->
?env:Logic_typing.Lenv.t ->
string ->
Cil_types.predicate