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/Pure_fun/Make/argument-1-Symex/Value/index.html

Module Symex.Value

type +'a t

The type of symbolic values, parameterized by their type. For example, sbool t represents a symbolic boolean.

Values also expose an Expr module for their syntactic representation.

type +'a ty

Type of values.

type sbool

The type for booleans.

val is_bool_ty : 'a ty -> bool

Whether the given type is sbool ty

val not : sbool t -> sbool t

not b returns the logical negation of boolean b.

val ppa : Format.formatter -> 'a t -> unit
val sem_eq_untyped : 'a t -> 'b t -> sbool t
val mk_var : Symex.Var.t -> 'a ty -> 'a t

mk_var var ty creates a symbolic variable with name var and type ty.

val to_bool : 'a t -> bool option

to_bool v returns Some b if v is a concrete boolean b, or None if v is symbolic.

val of_bool : bool -> sbool t

of_bool b creates a concrete boolean value from b.

module Expr : Symex.Value.Expr with type 'a ty := 'a ty and type 'a v := 'a t

Expr.t describes a syntactic representation of a value of type 'a v. Syntactic objects, unlike semantic values, can contain "free" variables and operations such as substitution have meaning.