frama-c 27.0 · OCaml Package

type t_env

type t_prop

val pretty : Format.formatter -> t_prop -> unit

val merge : t_env -> t_prop -> t_prop -> t_prop

val empty : t_prop

val new_env : 
  ?lvars:Frama_c_kernel.Cil_types.logic_var list ->
  Frama_c_kernel.Cil_types.kernel_function ->
  t_env

optionally init env with user logic variables

val add_axiom : WpPropId.prop_id -> LogicUsage.logic_lemma -> unit

val add_hyp : 
  ?for_pid:WpPropId.prop_id ->
  t_env ->
  WpPropId.pred_info ->
  t_prop ->
  t_prop

val add_goal : t_env -> WpPropId.pred_info -> t_prop -> t_prop

val add_terminates_subgoal : 
  t_env ->
  (WpPropId.prop_id * 'a) ->
  ?deps:Frama_c_kernel.Property.Set.t ->
  Frama_c_kernel.Cil_types.predicate ->
  Frama_c_kernel.Cil_types.stmt ->
  Wp__.Mcfg.terminates_source ->
  t_prop ->
  t_prop

val add_assigns : t_env -> WpPropId.assigns_info -> t_prop -> t_prop

val use_assigns : 
  t_env ->
  WpPropId.prop_id option ->
  WpPropId.assigns_desc ->
  t_prop ->
  t_prop

use_assigns env hid kind assgn goal performs the havoc on the goal. * hid should be None iff assgn is WritesAny, * and tied to the corresponding identified_property otherwise.

val label : 
  t_env ->
  Frama_c_kernel.Cil_types.stmt option ->
  Clabels.c_label ->
  t_prop ->
  t_prop

val init : 
  t_env ->
  Frama_c_kernel.Cil_types.varinfo ->
  Frama_c_kernel.Cil_types.init option ->
  t_prop ->
  t_prop

val const : t_env -> Frama_c_kernel.Cil_types.varinfo -> t_prop -> t_prop

val assign : 
  t_env ->
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.lval ->
  Frama_c_kernel.Cil_types.exp ->
  t_prop ->
  t_prop

val return : 
  t_env ->
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.exp option ->
  t_prop ->
  t_prop

val test : 
  t_env ->
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.exp ->
  t_prop ->
  t_prop ->
  t_prop

val switch : 
  t_env ->
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.exp ->
  (Frama_c_kernel.Cil_types.exp list * t_prop) list ->
  t_prop ->
  t_prop

val has_init : t_env -> bool

val loop_entry : t_prop -> t_prop

val loop_step : t_prop -> t_prop

val call_dynamic : 
  t_env ->
  Frama_c_kernel.Cil_types.stmt ->
  WpPropId.prop_id ->
  Frama_c_kernel.Cil_types.exp ->
  (Frama_c_kernel.Cil_types.kernel_function * t_prop) list ->
  t_prop

val call_goal_precond : 
  t_env ->
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.exp list ->
  pre:WpPropId.pred_info list ->
  t_prop ->
  t_prop

val call_terminates : 
  t_env ->
  Frama_c_kernel.Cil_types.stmt ->
  kind:Wp__.Mcfg.terminates_source ->
  ?kf:Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.exp list ->
  WpPropId.pred_info ->
  callee_t:Frama_c_kernel.Cil_types.predicate ->
  t_prop ->
  t_prop

val call_decreases : 
  t_env ->
  Frama_c_kernel.Cil_types.stmt ->
  ?kf:Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.exp list ->
  WpPropId.variant_info ->
  ?caller_t:Frama_c_kernel.Cil_types.predicate ->
  ?callee_d:Frama_c_kernel.Cil_types.variant ->
  t_prop ->
  t_prop

val call : 
  t_env ->
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.lval option ->
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.exp list ->
  pre:WpPropId.pred_info list ->
  post:WpPropId.pred_info list ->
  pexit:WpPropId.pred_info list ->
  assigns:Frama_c_kernel.Cil_types.assigns ->
  p_post:t_prop ->
  p_exit:t_prop ->
  t_prop

val scope : 
  t_env ->
  Frama_c_kernel.Cil_types.varinfo list ->
  Wp__.Mcfg.scope ->
  t_prop ->
  t_prop

val close : t_env -> t_prop -> t_prop

val build_prop_of_from : t_env -> WpPropId.pred_info list -> t_prop -> t_prop

build p => alpha(p) for functional dependencies verification.

package frama-c