1 (**************************************************************************)
3 (* This file is part of WP plug-in of Frama-C. *)
5 (* Copyright (C) 2007-2011 *)
6 (* CEA (Commissariat a l'énergie atomique et aux énergies *)
9 (* you can redistribute it and/or modify it under the terms of the GNU *)
10 (* Lesser General Public License as published by the Free Software *)
11 (* Foundation, version 2.1. *)
13 (* It is distributed in the hope that it will be useful, *)
14 (* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
15 (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
16 (* GNU Lesser General Public License for more details. *)
18 (* See the GNU Lesser General Public License version 2.1 *)
19 (* for more details (enclosed in the file licenses/LGPLv2.1). *)
21 (**************************************************************************)
27 val labels_empty : label_mapping
28 val labels_fct_pre : label_mapping
29 val labels_fct_post : label_mapping
30 val labels_fct_assigns : label_mapping
31 val labels_assert_before : stmt -> label_mapping
32 val labels_assert_after : stmt -> logic_label option -> label_mapping
33 val labels_loop_inv : stmt -> label_mapping
34 val labels_loop_assigns : stmt -> label_mapping
35 val labels_stmt_pre : stmt -> label_mapping
36 val labels_stmt_post : stmt -> logic_label option -> label_mapping
37 val labels_stmt_assigns : stmt -> logic_label option -> label_mapping
38 val labels_predicate : (logic_label * logic_label) list -> label_mapping
39 val labels_axiom : label_mapping
41 val preproc_annot : label_mapping -> predicate named -> predicate named
42 val preproc_annot_term : label_mapping -> term -> term
45 label_mapping -> identified_term from list -> identified_term from list
47 val preproc_label : label_mapping -> logic_label -> logic_label
49 (** from clabels.mli *)
50 (** create a virtual label to a statement (it can have no label) *)
51 val mk_logic_label : Cil_types.stmt -> Cil_types.logic_label