package frama-c

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

This module is used to check the assigns specification of a given function so that if it is not precise enough to enable precise memory models hypotheses computation, the assigns specification is considered incomplete.

All these functions are memoized.

val compute : Frama_c_kernel.Kernel_function.t -> unit
val is_complete : Frama_c_kernel.Kernel_function.t -> bool

Displays a warning if the given kernel function has incomplete assigns. Note that the warning is configured with ~once set to true.

val wkey_pedantic : Wp_parameters.warn_category