package why3find

  1. Overview
  2. Docs
A Why3 Package Manager

Install 

dune-project
 Dependency

git.frama-c.com Readme Changelog LGPL-2.1-only License Edit opam file Versions (3)

Authors

  1. L
    Loïc Correnson <loic.correnson@cea.fr>
  2. B
    Benjamin Jorge <benjamin.jorge@cea.fr>

Maintainers

  1. B
    benjamin.jorge@cea.fr
  2. L
    loic.correnson@cea.fr

Sources

why3find-1.3.0.tar.gz
md5=435da830a513fd91ec5411c91126b763
sha512=fd8b04eb16d569c0dc9e5595a40b174d7858121b080c81d459b2f28fb3af1ebc32ef408859d5c1c5f45c61790625c027c2ecfc3d45e597943543de7212bab8d6

doc/why3find.utils/Why3findUtils/Dap/index.html

Module Why3findUtils.DapSource

Debug Adapater Protocol

Sourcetype adapter
Sourceval trace : bool ref

Base Protocol

Sourcetype handler = adapter -> Json.t -> Json.t
Sourceval establish : Rpc.transport -> adapter

Establish the adapter or exit

Sourceval running : adapter -> bool

Testing if the adapter is still running. Returns true when there is no more in/out pending messages.

Sourceval emit : adapter -> string -> Json.t -> unit

Send and Event to the client

Sourceval register : ?force:bool -> string -> handler -> unit

Register a request handler

Sourceval process : adapter -> bool

Process (at most) one pending LSP message of one scheduled callback, if any. Always process pending non-blocking I/O. Then, provided no request nor callback is being processed: flush one pending callback, if any, or process one LSP message, if any. Returns true is some request or callback has been processed.

Sourceval yield : adapter -> unit

Same as process.

Sourceval flush : adapter -> unit

Flush output channel.

Sourceval schedule : adapter -> (adapter -> unit) -> unit

Schedule a callback to be executed during subsequent calls to `process` or `yield`.

Sourceval register_capability : string -> ?value:Json.t -> unit -> unit

Register adapter capbility. Default value `true`.

Output & Logging

Sourcetype category = [
  1. | `console
  2. | `important
  3. | `stdout
  4. | `stderr
]
Sourceval output : adapter -> ?category:category -> ('a, Format.formatter, unit, unit) format4 -> 'a

Initialization Sequence

Sourceval initialized : adapter -> unit
Sourceval on_init : (adapter -> unit) -> unit

By default, on_init emits an initialized event. If overriden, don't forget to emit an initialized event at some point.

Sourceval on_configured : (adapter -> unit) -> unit

See also breakpoint callback, below

Launch Sequence

Sourceval no_debug : unit -> bool
Sourceval restarted : unit -> Json.t
Sourceval on_attach : (adapter -> unit) -> unit

Attached Request callback

Sourceval on_launch : (adapter -> unit) -> unit

Launched Request callback

End Sequence

Sourceval exited : adapter -> int -> unit

Emits an exited event with the corresponding exit code.

Sourceval terminated : adapter -> ?restart:Json.t -> unit -> unit

Emits a terminated event.

Sourceval on_terminate : (adapter -> restart:bool -> unit) -> unit

Terminate request callback.

Sourcetype disconnect =
  1. | Disconnect of {
    1. restart : bool;
    2. terminate : bool;
    3. suspend : bool;
    }
    (*

    Disconnect request callback. Use the options to register the associated capabilities.

    *)

Disconnect request arguments

Sourceval on_disconnect : ?terminate:bool -> ?suspend:bool -> (adapter -> disconnect -> unit) -> unit

Progress

Sourcetype progress
Sourceval idle : progress
Sourceval progress : adapter -> ?id:string -> title:string -> ?cancel:(adapter -> unit) -> ?message:string -> ?percent:int -> unit -> progress
Sourceval update : progress -> ?message:string -> ?percent:int -> unit -> unit
Sourceval finished : progress -> ?message:string -> unit -> unit

Locations

Sourceval of_line : Json.t -> int
Sourceval to_line : int -> Json.t
Sourceval of_column : Json.t -> int
Sourceval to_column : int -> Json.t
Sourceval of_source : Json.t -> string
Sourceval to_source : string -> Json.t
Sourcetype location =
  1. | Loc of {
    1. file : string;
    2. line : int;
    3. column : int;
    4. end_line : int;
    5. end_column : int;
    }
Sourceval js_rangefields : location -> (string * Json.t) list
Sourceval js_sourcefields : location -> (string * Json.t) list
Sourceval loc : ?file:string -> ?line:int -> ?column:int -> ?end_line:int -> ?end_column:int -> unit -> location

Breakpoints

Sourcetype breakpoint
Sourceval failed : ?message:string -> unit -> breakpoint
Sourceval pending : id:int -> ?message:string -> unit -> breakpoint
Sourceval verified : id:int -> ?message:string -> ?file:string -> ?line:int -> ?column:int -> ?end_line:int -> ?end_column:int -> unit -> breakpoint
Sourceval breakpoint : adapter -> id:int -> ?reason:string -> ?verified:bool -> ?message:string -> ?file:string -> ?line:int -> ?column:int -> ?end_line:int -> ?end_column:int -> unit -> unit

Update a (pending) breakpoint.

Sourcetype source_breakpoint =
  1. | SourceBreakpoint of {
    1. file : string;
    2. line : int;
    3. column : int;
    4. condition : string;
    5. hit_condition : string;
    6. log_message : string;
    }
Sourceval on_breakpoint : ?condition:bool -> ?hit_condition:bool -> ?log_message:bool -> ?clear:(unit -> unit) -> (source_breakpoint -> breakpoint) -> unit

If specified, the flags will activate the associated capabilities.

Identified Objects

For custom requests, it is possible to attach attributes to identified objects and to recover them by object identifier.

You first create an attribute map with attribute function. Then, you can create values for this attribue map with value and attach them to variables, frames and/or threads. Values can be obtained back from identifiers with find_by_varId, find_by_frameId and find_by_threadId.

Lifetime of identifiers ends on stopped events.

Sourcetype 'a attribute
Sourceand value
Sourceval attribute : unit -> 'a attribute
Sourceval value : 'a attribute -> 'a -> value
Sourceval get_by_varId : 'a attribute -> int -> 'a option
Sourceval get_by_frameId : 'a attribute -> int -> 'a option
Sourceval get_by_threadId : 'a attribute -> int -> 'a option

Variables

Its is recommended to use Darray.delayed for returning large array of variables.

Sourcetype variable
Sourceval variable : name:string -> ?value:string -> ?vtype:string -> ?kind:string -> ?attributes:string list -> ?visiblity:string -> ?index:variable Darray.t -> ?named:variable Darray.t -> ?decl:location -> ?vdecl:location -> ?values:value list -> unit -> variable
  • parameter kind

    "property", "method", "class", "data", "event", "baseClass", "innerClass", "interface", "mostDerivedClass", "virtual", etc.

  • parameter attributes

    "static", "constant", "readOnly", "rawString", etc.

  • parameter visibility

    "public", "private", "protected", "internal", "final", etc.

Scopes

Its is recommended to use Darray.delayed for returning large array of variables.

Sourcetype scope
Sourceval scope : name:string -> ?kind:string -> ?index:variable Darray.t -> ?named:variable Darray.t -> ?expensive:bool -> ?range:location -> unit -> scope

Stack Frames

Sourceval setRestartableFrames : unit -> unit
Sourcetype frame
Sourceval label : name:string -> frame
Sourceval frame : name:string -> ?subtle:bool -> ?range:location -> ?restart:(adapter -> unit) -> ?scopes:scope list -> ?values:value list -> unit -> frame

Threads

Sourcetype thread
Sourceval thread : adapter -> name:string -> ?frames:(thread -> frame Darray.t) -> ?on_pause:(thread -> unit) -> ?on_next:(thread -> unit) -> ?on_step_in:(thread -> unit) -> ?on_step_out:(thread -> unit) -> ?on_continue:(thread -> unit) -> unit -> thread
Sourceval connect : thread -> ?frames:(thread -> frame Darray.t) -> ?on_pause:(thread -> unit) -> ?on_next:(thread -> unit) -> ?on_step_in:(thread -> unit) -> ?on_step_out:(thread -> unit) -> ?on_continue:(thread -> unit) -> unit -> unit
Sourceval id : thread -> int
Sourceval on : thread -> adapter
Sourceval name : thread -> string
Sourceval threads : unit -> thread list

Sorted by Id.

Sourceval find : int -> thread

Find by Id

Sourceval get : 'a attribute -> thread -> 'a option
Sourceval set : 'a attribute -> thread -> 'a -> unit
Sourceval remove : 'a attribute -> thread -> unit
Sourceval living : thread -> bool
Sourceval updated : ?reason:string -> thread -> unit
Sourceval terminate : thread -> unit
Sourcetype reason = [
  1. | `step
  2. | `breakpoint
  3. | `pause
  4. | `entry
  5. | `except
  6. | `error
]
Sourceval stopped : reason:reason -> ?description:string -> ?text:string -> ?all:bool -> ?preserveFocus:bool -> ?breakpoints:int list -> thread -> unit
Sourceval set_single_thread_support : unit -> unit