Newer
Older
(**************************************************************************)
(* *)
(* This file is part of WP plug-in of Frama-C. *)
(* *)
6
7
8
9
10
11
12
13
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
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
(* CEA (Commissariat a l'energie atomique et aux energies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
(* -------------------------------------------------------------------------- *)
(* --- Compilation of ACSL Logic-Info --- *)
(* -------------------------------------------------------------------------- *)
open LogicUsage
open Cil_types
open Cil_datatype
open Clabels
open Lang
open Lang.F
open Sigs
open Definitions
type polarity = [ `Positive | `Negative | `NoPolarity ]
module Make( M : Sigs.Model ) :
sig
(** {3 Definitions} *)
type value = M.loc Sigs.value
type logic = M.loc Sigs.logic
type result = M.loc Sigs.result
type sigma = M.Sigma.t
type chunk = M.Chunk.t
(** {3 Frames} *)
type call
type frame
val pp_frame : Format.formatter -> frame -> unit
val local : descr:string -> frame
val frame : kernel_function -> frame
val call : ?result:M.loc -> kernel_function -> value list -> call
val call_pre : sigma -> call -> sigma -> frame
val call_post : sigma -> call -> sigma sequence -> frame
val mk_frame :
?kf:Cil_types.kernel_function ->
?result:result ->
?status:Lang.F.var ->
?formals:value Varinfo.Map.t ->
?labels:sigma Clabels.LabelMap.t ->
?descr:string ->
unit -> frame
val formal : varinfo -> value option
val return : unit -> typ
val result : unit -> result
val status : unit -> var
val trigger : trigger -> unit
val guards : frame -> pred list
val mem_frame : c_label -> sigma
val mem_at_frame : frame -> c_label -> sigma
val set_at_frame : frame -> c_label -> sigma -> unit
val in_frame : frame -> ('a -> 'b) -> 'a -> 'b
val get_frame : unit -> frame
(** {3 Environment} *)
type env
val mk_env : ?here:sigma -> ?lvars:Logic_var.t list -> unit -> env
val current : env -> sigma
val move_at : env -> sigma -> env
val env_at : env -> c_label -> env
val mem_at : env -> c_label -> sigma
val env_let : env -> logic_var -> logic -> env
val env_letp : env -> logic_var -> pred -> env
val env_letval : env -> logic_var -> value -> env
(** {3 Compiler} *)
val term : env -> Cil_types.term -> term
val pred : polarity -> env -> predicate -> pred
val logic : env -> Cil_types.term -> logic
val region : env -> unfold:bool -> Cil_types.term -> M.loc Sigs.region
(** When [~unfold:true], decompose compound regions field by field *)
val bootstrap_term : (env -> Cil_types.term -> term) -> unit
val bootstrap_pred : (polarity -> env -> predicate -> pred) -> unit
val bootstrap_logic : (env -> Cil_types.term -> logic) -> unit
val bootstrap_region :
(env -> unfold:bool -> Cil_types.term -> M.loc Sigs.region) -> unit
(** {3 Application} *)
val call_fun : env -> logic_info
-> logic_label list
-> F.term list -> F.term
val call_pred : env -> logic_info
-> logic_label list
-> F.term list -> F.pred
(** {3 Logic Variable and ACSL Constants} *)
val logic_var : env -> logic_var -> logic
val logic_info : env -> logic_info -> pred option
(** {3 Logic Lemmas} *)
val lemma : logic_lemma -> dlemma
end