plugins/cfg/cfg_ast.mli

   1 (********************************************************************)
   2 (*                                                                  *)
   3 (*  The Why3 Verification Platform   /   The Why3 Development Team  *)
   4 (*  Copyright 2010-2023 --  Inria - CNRS - Paris-Saclay University  *)
   5 (*                                                                  *)
   6 (*  This software is distributed under the terms of the GNU Lesser  *)
   7 (*  General Public License version 2.1, with the special exception  *)
   8 (*  on linking described in file LICENSE.                           *)
   9 (*                                                                  *)
  10 (********************************************************************)
  11
  12 open Why3
  13
  14 type ident = Ptree.ident
  15
  16 type label = Ptree.ident
  17
  18 type loop_clause = Invariant | Variant
  19
  20 type cfg_instr = {
  21     cfg_instr_desc : cfg_instr_desc;
  22     cfg_instr_loc  : Loc.position;
  23   }
  24
  25 and cfg_term = {
  26     cfg_term_desc : cfg_term_desc;
  27     cfg_term_loc : Loc.position;
  28   }
  29
  30 and cfg_instr_desc =
  31   | CFGinvariant of (loop_clause * ident option * Ptree.term * int option ref) list
  32   (** possibly named invariants *)
  33   | CFGexpr of Ptree.expr
  34   (** any other regular WhyML expressions *)
  35
  36 and cfg_term_desc =
  37   | CFGgoto of label
  38   (** goto a label "goto L" *)
  39   | CFGswitch of Ptree.expr * switch_branch list
  40   (** pattern-matching *)
  41   | CFGreturn of Ptree.expr
  42   (** return from a cfg *)
  43   | CFGabsurd
  44   (** unreachable *)
  45
  46 and switch_branch = Ptree.pattern * cfg_term
  47 (** pattern -> regular WhyML expression ; goto ident *)
  48
  49 and block = (cfg_instr list * cfg_term)
  50
  51 type cfg_fundef =
  52   { cf_name: ident;
  53     cf_args: Ptree.binder list;
  54     cf_retty: Ptree.pty;
  55     cf_mask: Ity.mask;
  56     cf_pat: Ptree.pattern;
  57     cf_spec: Ptree.spec;
  58     cf_attrs: Ptree.attr list;
  59     cf_locals: (bool * ident * Ptree.pty * Ptree.expr option) list;
  60     cf_block0: block;
  61     cf_blocks: (label * block) list;
  62   }
  63
  64 type cfg_decl =
  65   | Dmlw_decl of Ptree.decl
  66   | Dletcfg of cfg_fundef
  67   | Dreccfg of cfg_fundef list
  68   | Dscope of Loc.position * bool * ident * cfg_decl list
  69
  70 type cfg_file = (ident * cfg_decl list) list
  71   (** a list of modules containing lists of declarations *)