package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-31.0-Gallium.tar.gz

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

doc/frama-c-e-acsl.core/E_ACSL/Translation_error/index.html

Module `E_ACSL.Translation_error`

include Error.S

type 'a result = ('a, exn) Frama_c_kernel.Result.t

Represent either a result of type 'a or an error with an exception.

exception Typing_error of Frama_c_kernel.Cil_datatype.Location.t
  * Options.category option
  * string

Typing error where the first element is the phase where the error occured and the second element is the error message.

exception Not_yet of Frama_c_kernel.Cil_datatype.Location.t
  * Options.category option
  * string

"Not yet supported" error where the first element is the phase where the error occured and the second element is the error message.

exception Not_memoized of Frama_c_kernel.Cil_datatype.Location.t
  * Options.category option

"Not memoized" error with the phase where the error occured.

val make_untypable : 
  ?loc:Frama_c_kernel.Cil_datatype.Location.t ->
  string ->
  exn

Make a Typing_error exception with the given message.

val make_not_yet : ?loc:Frama_c_kernel.Cil_datatype.Location.t -> string -> exn

Make a Not_yet exception with the given message.

val make_not_memoized : 
  ?loc:Frama_c_kernel.Cil_datatype.Location.t ->
  unit ->
  exn

Make a Not_memoized exception with the given message.

val untypable : ?loc:Frama_c_kernel.Cil_datatype.Location.t -> string -> 'a

raises Typing_error
with the given message for the current phase.

val not_yet : ?loc:Frama_c_kernel.Cil_datatype.Location.t -> string -> 'a

raises Not_yet
with the given message for the current phase.

val not_memoized : ?loc:Frama_c_kernel.Cil_datatype.Location.t -> unit -> 'a

raises Not_memoized
for the current phase.

val print_not_yet : string -> unit

Print the "not yet supported" message without raising an exception.

val handle : ('a -> 'a) -> 'a -> 'a

Run the closure with the given argument and handle potential errors. Return the provide argument in case of errors.

val generic_handle : ('a -> 'b) -> 'b -> 'a -> 'b

Run the closure with the given argument and handle potential errors. Return the additional argument in case of errors.

val retrieve_preprocessing : 
  string ->
  ('a -> 'b result) ->
  'a ->
  (Format.formatter -> 'a -> unit) ->
  'b

Retrieve the result of a preprocessing phase, which possibly failed. The string argument and the formatter are used to display a message in case the preprocessing phase did not compute the required result.

val pp_result : 
  (Format.formatter -> 'a -> unit) ->
  Format.formatter ->
  'a result ->
  unit

pp_result pp where pp is a formatter for 'a returns a formatter for 'a result.

val map : ('a -> 'b) -> 'a result -> 'b

val map2 : ('a -> 'b -> 'c) -> 'a result -> 'b result -> 'c

val map3 : ('a -> 'b -> 'c -> 'd) -> 'a result -> 'b result -> 'c result -> 'd

Apply a function to one or several results and propagate the errors