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.ForwardsTransfer.html | 88 ++++++++++++++++++++++++++++++ 1 file changed, 88 insertions(+) create mode 100644 cil/doc/api/Dataflow.ForwardsTransfer.html (limited to 'cil/doc/api/Dataflow.ForwardsTransfer.html') diff --git a/cil/doc/api/Dataflow.ForwardsTransfer.html b/cil/doc/api/Dataflow.ForwardsTransfer.html new file mode 100644 index 00000000..dbefaa03 --- /dev/null +++ b/cil/doc/api/Dataflow.ForwardsTransfer.html @@ -0,0 +1,88 @@ + + + + + + + + + + + + + + + + + + + + + + + + +CIL API Documentation (version 1.3.5) : Dataflow.ForwardsTransfer + + +
 Up + Next +
+

Module type Dataflow.ForwardsTransfer

+
+
module type ForwardsTransfer = 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. May be + imperative.
+
+ +
val copy : t -> t
+Make a deep copy of the data
+
+
val stmtStartData : t Inthash.t
+For each statement id, the data at the start. Not found in the hash + table means nothing is known about the state at this point. At the end + of the analysis this means that the block is not reachable.
+
+
val pretty : unit -> t -> Pretty.doc
+Pretty-print the state
+
+
val computeFirstPredecessor : Cil.stmt -> t -> t
+Give the first value for a predecessors, compute the value to be set + for the block
+
+
val combinePredecessors : Cil.stmt ->
       old:t ->
       t -> t option
+Take some old data for the start of a statement, and some new data for + the same point. Return None if the combination is identical to the old + data. Otherwise, compute the combination, and return it.
+
+
val doInstr : Cil.instr ->
       t -> t Dataflow.action
+The (forwards) transfer function for an instruction. The + Cil.currentLoc is set before calling this. The default action is to + continue with the state unchanged.
+
+
val doStmt : Cil.stmt ->
       t ->
       t Dataflow.stmtaction
+The (forwards) transfer function for a statement. The Cil.currentLoc + is set before calling this. The default action is to do the instructions + in this statement, if applicable, and continue with the successors.
+
+
val doGuard : Cil.exp ->
       t ->
       t Dataflow.guardaction
+Generate the successor to an If statement assuming the given expression + is nonzero. Analyses that don't need guard information can return + GDefault; this is equivalent to returning GUse of the input. + A return value of GUnreachable indicates that this half of the branch + will not be taken and should not be explored. This will be called + twice per If, once for "then" and once for "else".
+
+
val filterStmt : Cil.stmt -> bool
+Whether to put this statement in the worklist. This is called when a + block would normally be put in the worklist.
+
+ \ No newline at end of file -- cgit