Skip to content
Snippets Groups Projects
Commit e413f016 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Merge branch 'feature/wp/overview-api' into 'master' 

Provide an organized index for the WP API

Closes #1165

See merge request frama-c/frama-c!3911
parents 212e3da5 3a057a27
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Makefile
+ 7
− 3
View file @ e413f016
......@@ -109,16 +109,20 @@ PTEST_USE_WP_CACHE:=yes
include share/Makefile.testing
###############################################################################
# Server Documentation
# Linters
################################
include share/Makefile.serverdoc
###############################################################################
# Code prettyfication and lint
include share/Makefile.linting
###############################################################################
# Frama-C Documentation
################################
include share/Makefile.documentation
###############################################################################
# Local Variables:
# compile-command: "make"
......
share/Makefile.serverdoc → share/Makefile.documentation
+ 13
− 0
View file @ e413f016
......@@ -20,6 +20,19 @@
# #
##########################################################################
##########################################################################
# #
# Frama-C Documentation targets #
# #
##########################################################################
.PHONY: doc
doc:
dune build @doc
@echo "Generated Documentation:"
@echo " file:///$(PWD)/_build/default/_doc/_html/index.html"
##########################################################################
# #
# Generate Documentation for Server Requests and Protocols. #
......
src/plugins/wp/wp.ml
+ 199
− 43
View file @ e413f016
......@@ -20,64 +20,220 @@
(* *)
(**************************************************************************)
(** 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
module Ctypes = Ctypes
module Clabels = Clabels
module MemoryContext = MemoryContext
module LogicUsage = LogicUsage
module RefUsage = RefUsage
module NormatLabels = NormAtLabels
module WpPropId = WpPropId
module Mcfg = Mcfg
module Context = Context
module Warning = Warning
module Lang = Lang
(* -------------------------------------------------------------------------- *)
(** {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
module Passive = Passive
module Splitter = Splitter
module LogicBuiltins = LogicBuiltins
(** Low-Level Logic Terms and Predicates *)
module Lang = Lang
(** Generated Logic Definitions *)
module Definitions = Definitions
module Cint = Cint
(** 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 Vset = Vset
module Cmath = Cmath
module Cstring = Cstring
module Sigs = Sigs
(** {2 State Model} *)
module Sigma = Sigma
module Passive = Passive
module Mstate = Mstate
module Conditions = Conditions
module Filtering = Filtering
module Plang = Plang
module Pcfg = Pcfg
module Pcond = Pcond
(** {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 Sigma = Sigma
module MemVar = MemVar
module MemTyped = MemTyped
module CfgCompiler = CfgCompiler
module LogicUsage = LogicUsage
module StmtSemantics = StmtSemantics
module Factory = Factory
module Driver = Driver
module VCS = VCS
module Tactical = Tactical
module Strategy = Strategy
module Auto = Auto
module VC = VC
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 ProverTask = ProverTask
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 AssignsCompleteness = AssignsCompleteness
module ProverTask = ProverTask
module ProverWhy3 = ProverWhy3
(** {2 Script Engine} *)
(** For gui *)
module Script = Script
module Footprint = Footprint
module ProofEngine = ProofEngine
module ProofScript = ProofScript
module ProofSession = ProofSession
module ProverScript = ProverScript
module ProverSearch = ProverSearch
module WpRTE = WpRTE
module ProofSession = ProofSession
(** {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
(** {2 Error Management} *)
module Warning = Warning
module Wp_error = Wp_error
(** {2 Printers and Reporting} *)
module Pcfg = Pcfg
module Pcond = Pcond
module Plang = Plang
module Rformat = Rformat
module WpContext = WpContext
module Why3Provers = Why3Provers
module ProverWhy3 = ProverWhy3
module Cache = Cache
module WpTarget = WpTarget
module Stats = Stats
module WpReport = WpReport
(** {2 EVA Proxy} *)
module Wp_eva = Wp_eva
(* -------------------------------------------------------------------------- *)
src/plugins/wp/wprop.ml deleted 100644 → 0
+ 0
− 112
View file @ 212e3da5
(**************************************************************************)
(* *)
(* This file is part of WP plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2007-2022 *)
(* 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). *)
(* *)
(**************************************************************************)
(* -------------------------------------------------------------------------- *)
(* --- Indexed Interface --- *)
(* -------------------------------------------------------------------------- *)
type property =
| Later of Property.t
| Proxy of Property.t * Emitter.t * Property.t list
module type Info =
sig
include State_builder.Info_with_size
type key
val property : key -> property
end
module type Indexed =
sig
type key
val mem : key -> bool
val property : key -> Property.t
val add_hook : (key -> Property.t -> unit) -> unit
end
module type Indexed2 =
sig
type key1
type key2
val mem : key1 -> key2 -> bool
val property : key1 -> key2 -> Property.t
val add_hook : (key1 -> key2 -> Property.t -> unit) -> unit
end
(* -------------------------------------------------------------------------- *)
(* --- Index-1 Implementation --- *)
(* -------------------------------------------------------------------------- *)
module Indexed
(Key:Datatype.S_with_collections)
(Info:Info with type key = Key.t) =
struct
type key = Key.t
module H = State_builder.Hashtbl(Key.Hashtbl)(Property)(Info)
let hooks = ref []
let add_hook f = hooks := !hooks @ [f]
let mem = H.mem
let property (key:key) =
try H.find key
with Not_found ->
let ip =
match Info.property key with
| Later ip -> ip
| Proxy(ip,emitter,ips) ->
Property_status.logical_consequence emitter ip ips ; ip
in
List.iter (fun f -> f key ip) !hooks ;
H.add key ip ; ip
end
(* -------------------------------------------------------------------------- *)
(* --- Index-2 Wrapper --- *)
(* -------------------------------------------------------------------------- *)
module Indexed2
(Key1:Datatype.S_with_collections)
(Key2:Datatype.S_with_collections)
(Info:Info with type key = Key1.t * Key2.t) =
struct
module P = Datatype.Pair_with_collections(Key1)(Key2)
(struct
let module_name = Info.name
end)
module I = Indexed(P)(Info)
type key1 = Key1.t
type key2 = Key2.t
let mem a b = I.mem (a,b)
let property a b = I.property (a,b)
let add_hook f = I.add_hook (fun (a,b) -> f a b)
end
(* -------------------------------------------------------------------------- *)
src/plugins/wp/wprop.mli deleted 100644 → 0
+ 0
− 70
View file @ 212e3da5
(**************************************************************************)
(* *)
(* This file is part of WP plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2007-2022 *)
(* 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). *)
(* *)
(**************************************************************************)
(* ------------------------------------------------------------------------ *)
(**{2 Indexed API} *)
(* ------------------------------------------------------------------------ *)
type property =
| Later of Property.t
| Proxy of Property.t * Emitter.t * Property.t list
module type Info =
sig
include State_builder.Info_with_size
type key
val property : key -> property
end
module type Indexed =
sig
type key
val mem : key -> bool
val property : key -> Property.t
val add_hook : (key -> Property.t -> unit) -> unit
(** Hooks are executed once at property creation *)
end
module type Indexed2 =
sig
type key1
type key2
val mem : key1 -> key2 -> bool
val property : key1 -> key2 -> Property.t
val add_hook : (key1 -> key2 -> Property.t -> unit) -> unit
(** Hooks are executed once at property creation *)
end
(* ------------------------------------------------------------------------ *)
(**{2 Indexes} *)
(* ------------------------------------------------------------------------ *)
module Indexed
(Key:Datatype.S_with_collections)
(Info:Info with type key = Key.t) :
Indexed with type key = Key.t
module Indexed2
(Key1:Datatype.S_with_collections)
(Key2:Datatype.S_with_collections)
(Info:Info with type key = Key1.t * Key2.t) :
Indexed2 with type key1 = Key1.t and type key2 = Key2.t
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment