package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

frama-c

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module `Wp.ProverWhy3`Source

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

Source

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

package frama-c

Module Wp.ProverWhy3Source

Module `Wp.ProverWhy3`Source