package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
val add_specific_equality : for_tau:(Lang.tau -> bool) -> mk_new_eq:Lang.F.binop -> unit

Equality used in the goal, simpler to prove than polymorphic equality

val prove : ?mode:VCS.mode -> ?timeout:float -> ?steplimit:int -> ?memlimit:int -> prover:Why3Provers.t -> Wpo.t -> VCS.result Frama_c_kernel.Task.task

Return NoResult if it is already proved by Qed