|
|
@ -31,12 +31,18 @@ val get_instr : unit -> Sil.instr option
|
|
|
|
val get_loc_exn : unit -> Location.t
|
|
|
|
val get_loc_exn : unit -> Location.t
|
|
|
|
(** Get last location seen in symbolic execution *)
|
|
|
|
(** Get last location seen in symbolic execution *)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
val get_loc : unit -> Location.t option
|
|
|
|
|
|
|
|
(** Get last location seen in symbolic execution *)
|
|
|
|
|
|
|
|
|
|
|
|
val get_loc_trace : unit -> Errlog.loc_trace
|
|
|
|
val get_loc_trace : unit -> Errlog.loc_trace
|
|
|
|
(** Get the location trace of the last path seen in symbolic execution *)
|
|
|
|
(** Get the location trace of the last path seen in symbolic execution *)
|
|
|
|
|
|
|
|
|
|
|
|
val get_node_exn : unit -> Procdesc.Node.t
|
|
|
|
val get_node_exn : unit -> Procdesc.Node.t
|
|
|
|
(** Get last node seen in symbolic execution *)
|
|
|
|
(** Get last node seen in symbolic execution *)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
val get_node : unit -> Procdesc.Node.t option
|
|
|
|
|
|
|
|
(** Get last node seen in symbolic execution *)
|
|
|
|
|
|
|
|
|
|
|
|
val get_normalized_pre :
|
|
|
|
val get_normalized_pre :
|
|
|
|
(Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t) -> Prop.normal Prop.t option
|
|
|
|
(Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t) -> Prop.normal Prop.t option
|
|
|
|
(** return the normalized precondition extracted form the last prop seen, if any
|
|
|
|
(** return the normalized precondition extracted form the last prop seen, if any
|
|
|
|