Module Debugging

Functions to help debugging of VPL code. + a function failwith to track internal errors. => Context: most of the times, internal errors of the VPL (bugs in the "non-certified" part of the code) are "masked" using a default value. Such a style is both simple for proofs and efficient at runtime (and is necessary to match Verasco interfaces). => Purpose: here, we propose to "mark" in the code where are inserted these default values with a "failwith" function. Hence, we have thus two modes of the failwith function at extraction: - the "normal" mode that propagates the default value. - the "debugging" mode that provoques a runtime-failure in Caml, and thus help to track internal errors. + trace: use the same principle than "failwith" in order to have traces from the extracted code. WARNING ON USAGE: in failwith "toto" expr or trace INFO "toto" expr evaluation of expr happens before the side-effect (error-raising or printing) Hence, in order to avoid surprise, expr must be a value. ==> The extraction modes for trace and failwith are defined in PedraExtract.v. (Thus, it is not necessary to recompile all coq!)