Module Soteria_rust_lib.Error

type t = [
  1. | `DoubleFree
    (*

    Tried freeing the same allocation twice

    *)
  2. | `InvalidFree
    (*

    Tried freeing memory at a non-0 offset

    *)
  3. | `MemoryLeak
    (*

    Dynamically allocated memory was not freed

    *)
  4. | `MisalignedPointer of Soteria_rust_lib.Typed.T.nonzero Typed.t * Soteria_rust_lib.Typed.T.nonzero Typed.t * Soteria_rust_lib.Typed.T.sint Typed.t
    (*

    Tried accessing memory with a misaligned pointer (expected, received, offset)

    *)
  5. | `NullDereference
    (*

    Dereferenced a null pointer

    *)
  6. | `OutOfBounds
    (*

    Tried accessing memory outside the allocation bounds

    *)
  7. | `UninitializedMemoryAccess
    (*

    Accessed uninitialised memory

    *)
  8. | `UseAfterFree
    (*

    Use a location in memory after it was freed

    *)
  9. | `MisalignedFnPointer
    (*

    Tried calling a function pointer with a non-0 offset

    *)
  10. | `NotAFnPointer
    (*

    Tried calling a function pointer, but it doesn't represent a function

    *)
  11. | `AccessedFnPointer
    (*

    Tried accessing a function pointer's pointee

    *)
  12. | `InvalidFnArgCount of int * int
    (*

    Invalid argument count for function (function pointers only) (expected, received)

    *)
  13. | `InvalidFnArgTys of Charon.Types.ty * Charon.Types.ty
    (*

    Invalid arguments for function (function pointers only) (expected, received)

    *)
  14. | `DivisionByZero
    (*

    Integer division by zero

    *)
  15. | `InvalidShift
    (*

    Binary shift that is less than 0 or that exceeds the bit size of the type

    *)
  16. | `Overflow
    (*

    Arithmetic over or underflow

    *)
  17. | `RefToUninhabited of Charon.Types.ty
    (*

    Attempt to have a reference to an uninhabited value

    *)
  18. | `InvalidRef of t
    (*

    Attempt to have a reference that is not valid, e.g. because it points to uninitialised memory. Keeps track of the inner error

    *)
  19. | `StdErr of string
    (*

    Error caused by the std library (mainly intrinsics); kind of equivalent to `Panic

    *)
  20. | `UBAbort
    (*

    Abort caused by an UB trap being triggered

    *)
  21. | `UBDanglingPointer
    (*

    Pointer was offset outside of its allocation

    *)
  22. | `UBPointerArithmetic
    (*

    Arithmetics on two pointers

    *)
  23. | `UBPointerComparison
    (*

    Comparison of pointers with different provenance

    *)
  24. | `UBIntToPointerNoProvenance of Soteria_rust_lib.Typed.T.sint Typed.t
    (*

    Integer to pointer cast with no provenance

    *)
  25. | `UBIntToPointerStrict
    (*

    Integer to pointer cast with strict provenance

    *)
  26. | `UBTransmute of string
    (*

    Invalid transmute, e.g. null reference, wrong enum discriminant

    *)
  27. | `AliasingError
    (*

    Tree borrow violation that lead to UB

    *)
  28. | `RefInvalidatedEarly
    (*

    A protected reference was invalidated before the end of the function

    *)
  29. | `InvalidFreeStrongProtector
    (*

    Tried freeing an allocation when a strongly protected reference to it still exists

    *)
  30. | `FailedAssert of string option
    (*

    Failed assert!(cond)

    *)
  31. | `Panic of string option
    (*

    Regular panic, with a message

    *)
  32. | `UnwindTerminate
    (*

    Unwinding terminated

    *)
  33. | `DeadVariable
    (*

    Local was not initialised (impossible without `mir!`)

    *)
  34. | `Breakpoint
    (*

    Breakpoint intrinsic

    *)
  35. | `MetaExpectedError
    (*

    Function was marked as expecting an error; none happened

    *)
  36. | `InvalidLayout of Charon.Types.ty
    (*

    Type is too large for memory

    *)
  37. | `InvalidAlloc
    (*

    Error in alloc/realloc; a wrong alignment or size was provided

    *)
]
type warn_reason =
  1. | InvalidReference of Soteria_rust_lib.Typed.T.sloc Typed.t
val hash_warn_reason : warn_reason -> int
val is_unwindable : [> t ] -> bool
val pp : Stdlib.Format.formatter -> t -> unit
type with_trace = t * Charon.Meta.span_data Soteria.Terminal.Call_trace.t
val pp_with_trace : Stdlib.Format.formatter -> (t * Charon.Meta.span_data Soteria.Terminal.Call_trace.element list) -> unit
val compare_with_trace : (t * 'a) -> (t * 'a) -> int
val add_to_call_trace : with_trace -> Charon.Meta.span_data Soteria.Terminal.Call_trace.element -> t * Charon.Meta.span_data Soteria.Terminal.Call_trace.element list
val log_at : Trace.t -> t -> unit
val decorate : Trace.t -> t -> with_trace
module Diagnostic : sig ... end