package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file wp.ml

1
2
3
4
5
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
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    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).            *)
(*                                                                        *)
(**************************************************************************)

(** This the API of the WP plug-in *)

(* -------------------------------------------------------------------------- *)
(** {1 High-Level External API}

    The following modules are the recommanded entry points for using WP
    programmatically. They are meant to be relatively stable over time.

*)
(* -------------------------------------------------------------------------- *)

(** WP Proof Obligation Generator and Management *)
module VC = VC

(** Provers and Proof Obligations Results *)
module VCS = VCS

(** WP Plugin Interface *)
module Wp_parameters = Wp_parameters

(* -------------------------------------------------------------------------- *)
(** {1 Advanced Usage API}

    The following modules entry points for using WP advanced features,
    such as proof obligation manipulation, tactics and strategies.
    These modules might expose internal features of WP that are subject
    to change. Developpers using this API are encouraged to contact us
    for a roadmap information and further collaboration.
*)
(* -------------------------------------------------------------------------- *)

(** High-Level Term Representation *)
module Repr = Repr

(** Low-Level Logic Terms and Predicates *)
module Lang = Lang

(** Generated Logic Definitions *)
module Definitions = Definitions

(** Proof Task and Simplifiers *)
module Conditions = Conditions

(** Tactics Entry Points *)
module Tactical = Tactical

(** Strategies Entry Points *)
module Strategy = Strategy

(** WP Proof Obligation Generator *)
module Generator = Generator

(** Command Line Processing *)
module Register = Register

(* -------------------------------------------------------------------------- *)
(** {1 Low-Level Internal API}

    The following modules are _not_ intended to be used externally. The target
    audience is WP plug-in developpers. However, developpers interested in
    such low-level features are encouraged to contact us for more informations.
*)
(* -------------------------------------------------------------------------- *)

(** {2 Model Registration} *)

module Factory = Factory
module WpContext = WpContext

(** {2 Memory Models} *)

module MemDebug = MemDebug
module MemEmpty = MemEmpty
module MemLoader = MemLoader
module MemMemory = MemMemory
module MemRegion = MemRegion
module MemTyped = MemTyped
module MemVal = MemVal
module MemVar = MemVar
module MemZeroAlias = MemZeroAlias

(** {2 Other Models} *)

module Cint = Cint
module Cfloat = Cfloat
module Cmath = Cmath
module Cstring = Cstring

(** {2 State Model} *)

module Sigma = Sigma
module Passive = Passive
module Mstate = Mstate

(** {2 Model Hypotheses}*)

module MemoryContext = MemoryContext
module RefUsage = RefUsage
module WpTarget = WpTarget
module AssignsCompleteness = AssignsCompleteness

(** {2 Region Analysis} *)

module Region = Region
module Layout = Layout
module RegionAccess = RegionAccess
module RegionAnalysis = RegionAnalysis
module RegionAnnot = RegionAnnot
module RegionDump = RegionDump

(** {2 Compilers} *)

module Sigs = Sigs
module Driver = Driver
module Context = Context
module Ctypes = Ctypes
module Cvalues = Cvalues
module Clabels = Clabels
module CodeSemantics = CodeSemantics
module LogicAssigns = LogicAssigns
module LogicBuiltins = LogicBuiltins
module LogicCompiler = LogicCompiler
module LogicSemantics = LogicSemantics
module LogicUsage = LogicUsage
module StmtSemantics = StmtSemantics
module Dyncall = Dyncall
module Matrix = Matrix
module NormAtLabels = NormAtLabels

(** {2 Core Engine} *)

module CfgAnnot = CfgAnnot
module CfgCalculus = CfgCalculus
module CfgCompiler = CfgCompiler
module CfgDump = CfgDump
module CfgGenerator = CfgGenerator
module CfgInfos = CfgInfos
module CfgInit = CfgInit
module CfgWP = CfgWP
module WpReached = WpReached
module WpPropId = WpPropId
module WpRTE = WpRTE

(** {2 Proof Engine} *)

module Wpo = Wpo
module Auto = Auto
module Cache = Cache
module Cleaning = Cleaning
module Letify = Letify
module Splitter = Splitter
module Filtering = Filtering

(** {2 Prover Interface} *)

module Why3Provers = Why3Provers
module Filter_axioms = Filter_axioms
module Prover = Prover
module ProverTask = ProverTask
module ProverWhy3 = ProverWhy3

(** {2 Script Engine} *)

module Script = Script
module Footprint = Footprint
module ProofEngine = ProofEngine
module ProofScript = ProofScript
module ProverScript = ProverScript
module ProverSearch = ProverSearch
module ProofSession = ProofSession
module ProofStrategy = ProofStrategy

(** {2 Tactics} *)

module WpTac = WpTac
module TacArray = TacArray
module TacBitrange = TacBitrange
module TacBittest = TacBittest
module TacBitwised = TacBitwised
module TacChoice = TacChoice
module TacClear = TacClear
module TacCompound = TacCompound
module TacCongruence = TacCongruence
module TacCut = TacCut
module TacFilter = TacFilter
module TacHavoc = TacHavoc
module TacInduction = TacInduction
module TacInstance = TacInstance
module TacLemma = TacLemma
module TacModMask = TacModMask
module TacNormalForm = TacNormalForm
module TacOverflow = TacOverflow
module TacRange = TacRange
module TacRewrite = TacRewrite
module TacSequence = TacSequence
module TacShift = TacShift
module TacSplit = TacSplit
module TacUnfold = TacUnfold
module TacCompute = TacCompute

(** {2 Error Management} *)

module Warning = Warning
module Wp_error = Wp_error

(** {2 Printers and Reporting} *)

module Plang = Plang
module Pcfg = Pcfg
module Pcond = Pcond
module Ptip = Ptip
module Rformat = Rformat
module Stats = Stats
module WpReport = WpReport

(** {2 EVA Proxy} *)

module Wp_eva = Wp_eva

(* -------------------------------------------------------------------------- *)
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct