package frama-c

  1. Overview
  2. Docs

Module Wpo.VC_AnnotSource

Sourcetype t = {
  1. axioms : Definitions.axioms option;
  2. goal : GOAL.t;
  3. tags : Splitter.tag list;
  4. warn : Warning.t list;
  5. deps : Frama_c_kernel.Property.Set.t;
  6. path : Frama_c_kernel.Cil_datatype.Stmt.Set.t;
  7. source : (Frama_c_kernel.Cil_types.stmt * Wp__.Mcfg.goal_source) option;
}
Sourceval is_trivial : t -> bool
Sourceval resolve : pid:WpPropId.prop_id -> t -> bool