cntexmp_printer.mli 1.83 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
MARCHE Claude's avatar
MARCHE Claude committed
5 6 7 8 9 10 11
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

12 13
open Wstdlib
open Ident
14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38
open Term

(* Information about the term that triggers VC.  *)
type vc_term_info = {
  mutable vc_inside : bool;
  (* true if the term that triggers VC is currently processed *)
  mutable vc_loc : Loc.position option;
  (* the position of the term that triggers VC *)
  mutable vc_func_name : string option;
  (* the name of the function for that VC was made. None if VC
     is not generated for postcondition or precondition) *)
}

module TermCmp : sig
  type t = term

  val before: Loc.position option -> Loc.position option -> bool

  val compare: term -> term -> int
end

module S : Set.S with type elt = term and type t = Set.Make(TermCmp).t

val add_model_element: Term.term -> S.t -> S.t

39
(*
Andrei Paskevich's avatar
Andrei Paskevich committed
40 41
val model_trace_for_postcondition:
  attrs:Ident.Sattr.t -> vc_term_info -> Ident.Sattr.t
42
 *)
43 44 45 46

val check_enter_vc_term: Term.term -> bool -> vc_term_info -> unit

val check_exit_vc_term: Term.term -> bool -> vc_term_info -> unit
47 48 49

val update_info_labels: string -> Sattr.t Mstr.t -> Term.term ->
  Term.lsymbol -> Sattr.t Mstr.t
50 51 52

val check_for_counterexample: Term.term -> bool
(* Check if a term should be added for counterexample analysis *)