Frama_c_kernel.Logic_parse_stringexception Error of Cil_types.location * 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:Cil_types.location ->
?env:Logic_typing.Lenv.t ->
string ->
Cil_types.term_lvalval term :
Cil_types.kernel_function ->
?loc:Cil_types.location ->
?env:Logic_typing.Lenv.t ->
string ->
Cil_types.termval predicate :
Cil_types.kernel_function ->
?loc:Cil_types.location ->
?env:Logic_typing.Lenv.t ->
string ->
Cil_types.predicate