Module Eval_funs

module Eval_funs: sig .. end
Value analysis of entire functions, using the legacy engine.

Evaluate kf in state with_formals, first by reducing by the preconditions, then by evaluating the assigns, then by reducing by the post-conditions. The computation varies depending on the number of behaviors (single or multiple). Both methods are correct for any number of behaviors, but one is more efficient and the other is more precise.


val force_compute : unit -> unit
Perform a full analysis, starting from the main function.