From a5f03d96eee482cd84861fc8cefff9eb451c0cad Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 29 Mar 2009 09:47:11 +0000 Subject: Cleaned up configure script. Distribution of CIL as an expanded source tree with changes applied (instead of original .tar.gz + patches to be applied at config time). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1020 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cil/doc/api/Dataflow.BackwardsTransfer.html | 83 +++++++++++++++++++++++++++++ 1 file changed, 83 insertions(+) create mode 100644 cil/doc/api/Dataflow.BackwardsTransfer.html (limited to 'cil/doc/api/Dataflow.BackwardsTransfer.html') diff --git a/cil/doc/api/Dataflow.BackwardsTransfer.html b/cil/doc/api/Dataflow.BackwardsTransfer.html new file mode 100644 index 00000000..0ff812df --- /dev/null +++ b/cil/doc/api/Dataflow.BackwardsTransfer.html @@ -0,0 +1,83 @@ + + + + + + + + + + + + + + + + + + + + + + + + +CIL API Documentation (version 1.3.5) : Dataflow.BackwardsTransfer + + +
Previous + Up + 
+

Module type Dataflow.BackwardsTransfer

+
+
module type BackwardsTransfer = sig .. end
+
val name : string
+For debugging purposes, the name of the analysis
+
+
val debug : bool Pervasives.ref
+Whether to turn on debugging
+
+
type t
+
+The type of the data we compute for each block start. In many + presentations of backwards data flow analysis we maintain the + data at the block end. This is not easy to do with JVML because + a block has many exceptional ends. So we maintain the data for + the statement start.
+
+ +
val pretty : unit -> t -> Pretty.doc
+Pretty-print the state
+
+
val stmtStartData : t Inthash.t
+For each block id, the data at the start. This data structure must be + initialized with the initial data for each block
+
+
val combineStmtStartData : Cil.stmt ->
       old:t ->
       t -> t option
+When the analysis reaches the start of a block, combine the old data + with the one we have just computed. Return None if the combination is + the same as the old data, otherwise return the combination. In the + latter case, the predecessors of the statement are put on the working + list.
+
+
val combineSuccessors : t ->
       t -> t
+Take the data from two successors and combine it
+
+
val doStmt : Cil.stmt -> t Dataflow.action
+The (backwards) transfer function for a branch. The Cil.currentLoc is + set before calling this. If it returns None, then we have some default + handling. Otherwise, the returned data is the data before the branch + (not considering the exception handlers)
+
+
val doInstr : Cil.instr ->
       t -> t Dataflow.action
+The (backwards) transfer function for an instruction. The + Cil.currentLoc is set before calling this. If it returns None, then we + have some default handling. Otherwise, the returned data is the data + before the branch (not considering the exception handlers)
+
+
val filterStmt : Cil.stmt -> Cil.stmt -> bool
+Whether to put this predecessor block in the worklist. We give the + predecessor and the block whose predecessor we are (and whose data has + changed)
+
+ \ No newline at end of file -- cgit