Module Soteria_c_lib.Summary

module Var = Soteria.Symex.Var
module Agv = Aggregate_val
type after_exec = [
  1. | `After_exec
]
type pruned = [
  1. | `Pruned
]
type analysed = [
  1. | `Analysed
]
val leaks_to_error : loc:Cerb_location.t -> Cerb_location.t list -> [> `Memory_leak ] * Cerb_location.t Soteria.Terminal.Call_trace.element list
type raw = {
  1. args : Agv.syn list;
    (*

    List of arguments values, corresponding to the formal arguments in order. Really a form of (x == a0) * (y == a1)

    *)
  2. pre : State.syn list;
    (*

    Pre-condition as a list of fixes

    *)
  3. pc : Expr.t list;
    (*

    Path condition. Whether it is in the post or in the pre, it doesn't matter for UX.

    *)
  4. post : State.syn list;
    (*

    Post condition as a serialized heap

    *)
  5. ret : (Agv.syn, Error.t * Cerb_location.t Soteria.Terminal.Call_trace.t) Stdlib.result;
    (*

    Return value. If `ok` then it is the C value that the function returned, if `err` then it is a description of the bug exhibitied by the code

    *)
}
val pp_raw : Ppx_deriving_runtime.Format.formatter -> raw -> Ppx_deriving_runtime.unit
val show_raw : raw -> Ppx_deriving_runtime.string
type _ t =
  1. | After_exec : raw -> after_exec t
  2. | Pruned : {
    1. raw : raw;
    2. memory_leaks : Cerb_location.t list option;
      (*

      If None, no memory leak was detected. If Some l, then some memory leak was detected and, in addition, we return a list of all *known* code location where something that leaked was allocated. It is possible for this field to be Some [], which means that there was a leak, but we did not track any allocation site for it.

      *)
    } -> pruned t
  3. | Analysed : {
    1. raw : raw;
    2. manifest_bugs : (Error.t * Cerb_location.t Soteria.Terminal.Call_trace.t) list;
    } -> analysed t
val pp : 'a. Stdlib.Format.formatter -> 'a t -> unit
module Var_graph : sig ... end
module Var_hashset = Var_graph.Node_set
module Leak_set : sig ... end
val filter_serialized_state : Var_hashset.t -> State.syn list -> State_intf.syn list * Leak_set.elt list

Removes any bit of the state that does not any "relevant variables". i.e., bits that are not reachable from the precondition.

val init_reachable_vars : raw -> Var_hashset.t
val make : args:Agv.syn list -> pre:State.syn list -> pc:Expr.t list -> post:State.syn list -> ret: (Agv.syn, Error.t * Cerb_location.t Soteria.Terminal.Call_trace.t) Stdlib.result -> unit -> after_exec t
val prune : after_exec t -> pruned t

This function prunes the summary by removing anything that isn't reachable from the arguments or the return value. It returns the updated summary, as well as a boolean capturing whether a memory leak was detected. A memory leak is detected if there was an unreachable block that was not freed.

module Logic : sig ... end
module Execute : sig ... end
val analyse : 'a. fid:Ail_tys.sym -> 'a t -> analysed t

Current criterion: a bug is manifest if its path condition is a consequence of the heap's and function arguments well-formedness conditions

val manifest_bugs : fid:Ail_tys.sym -> 'a t -> (Error.t * Cerb_location.t Soteria.Terminal.Call_trace.t) list