package soteria

  1. Overview
  2. Docs
Soteria is a toolkit for writing symbolic bug-finding tools

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (2)

Authors

  1. S
    Sacha-Élie Ayoun <s.ayoun17@imperial.ac.uk>
  2. O
    Opale Sjöstedt <opale.sjostedt23@imperial.ac.uk>

Maintainers

  1. S
    Sacha-Élie Ayoun <s.ayoun17@imperial.ac.uk>
  2. O
    Opale Sjöstedt <opale.sjostedt23@imperial.ac.uk>

Sources

v0.1.0.tar.gz
md5=8f15271b81e34caa12a39e3b7a63313a
sha512=5f6987cf362bc06402d9bed324c7b060384d7ef02479e2a614ca4b4122cc65082f6afc892c398c6562b0eb42fc13d6cc77e76c2518221590576215aaa00ee5bd

doc/soteria/Soteria/Sym_states/Pmap/Make_patricia_tree/argument-1-Symex/Consumer/index.html

Module Symex.Consumer

type subst := Value.Expr.Subst.t
type 'a symex := 'a t
type ('a, 'fix) t
include Soteria.Soteria_std.Monad.Extension2 with type ('a, 'fix) t := ('a, 'fix) t
val fold : (module M : Soteria_std.Sigs.Foldable) -> 'elem M.t -> init:'a -> f:('a -> 'elem -> ('a, 'b) t) -> ('a, 'b) t
val fold_list : 'elem list -> init:'a -> f:('a -> 'elem -> ('a, 'b) t) -> ('a, 'b) t
val fold_iter : 'elem Iter.t -> init:'a -> f:('a -> 'elem -> ('a, 'b) t) -> ('a, 'b) t
val iter : (module M : Soteria_std.Sigs.Foldable) -> 'elem M.t -> f:('elem -> (unit, 'b) t) -> (unit, 'b) t
val iter_list : 'elem list -> f:('elem -> (unit, 'b) t) -> (unit, 'b) t
val iter_iter : 'elem Iter.t -> f:('elem -> (unit, 'b) t) -> (unit, 'b) t
val map_list : 'elem list -> f:('elem -> ('a, 'b) t) -> ('a list, 'b) t
val map_iter : 'elem Iter.t -> f:('elem -> ('a, 'b) t) -> ('a list, 'b) t
val all : ('a -> ('b, 'c) t) -> 'a list -> ('b list, 'c) t
val apply_subst : ((Value.Expr.t -> 'a Value.t) -> 'syn -> 'sem) -> 'syn -> ('sem, 'fix) t
val assert_pure : Value.sbool Value.t -> (unit, 'fix) t
val consume_pure : Value.Expr.t -> (unit, 'fix) t
val learn_eq : Value.Expr.t -> 'a Value.t -> (unit, 'fix) t
val expose_subst : unit -> (subst, 'fix) t
val lift_res : ('a, cons_fail, 'fix) Result.t -> ('a, 'fix) t
val lift : 'a symex -> ('a, 'fix) t
val branches : (unit -> ('a, 'fix) t) list -> ('a, 'fix) t
val ok : 'a -> ('a, 'fix) t
val lfail : Value.sbool Value.t -> ('a, 'fix) t
val miss : 'fix list -> ('a, 'fix) t
val miss_no_fix : reason:string -> unit -> ('a, 'fix) t
val map : ('a -> 'b) -> ('a, 'fix) t -> ('b, 'fix) t
val map_missing : ('fix -> 'g) -> ('a, 'fix) t -> ('a, 'g) t
val bind : ('a -> ('b, 'fix) t) -> ('a, 'fix) t -> ('b, 'fix) t
val bind_res : (('a, cons_fail, 'fix) Soteria.Soteria_std.Compo_res.t -> ('b, 'fix2) t) -> ('a, 'fix) t -> ('b, 'fix2) t
val run : subst:subst -> ('a, 'fix) t -> ('a * subst, cons_fail, 'fix) Result.t
val from_raw_UNSAFE : (subst -> ('a * subst, cons_fail, 'fix) Result.t) -> ('a, 'fix) t

This is unsafe and shouldn't be used in clients, it is only available to enable the implementation of the state monad transformer.

module Syntax : sig ... end