Merge pull request #1053 from mrstanb/add-docs-for-transfer-functions

Add documentation about Goblint's transfer functions

docs/developer-guide/firstanalysis.md

@@ -69,6 +69,7 @@ There is no need to implement the transfer functions for branching for this exam
 The assignment relies on the function `eval`, which is almost there. It just needs you to fix the evaluation of constants! Unless you jumped straight to this line, it should not be too complicated to fix this.
 With this in place, we should have sufficient information to tell Goblint that the assertion does hold.
 
+For more information on the signature of the individual transfer functions, please check out `module type Spec` documentation in [`src/framework/analyses.ml`](https://github.com/goblint/analyzer/blob/master/src/framework/analyses.ml).
 
 ## Extending the domain
 

src/framework/analyses.ml

@@ -383,16 +383,42 @@ sig
 
   val sync  : (D.t, G.t, C.t, V.t) ctx -> [`Normal | `Join | `Return] -> D.t
   val query : (D.t, G.t, C.t, V.t) ctx -> 'a Queries.t -> 'a Queries.result
+
+  (** A transfer function which handles the assignment of a rval to a lval, i.e.,
+      it handles program points of the form "lval = rval;" *)
   val assign: (D.t, G.t, C.t, V.t) ctx -> lval -> exp -> D.t
+
+  (** A transfer function used for declaring local variables.
+      By default only for variable-length arrays (VLAs). *)
   val vdecl : (D.t, G.t, C.t, V.t) ctx -> varinfo -> D.t
+
+  (** A transfer function which handles conditional branching yielding the
+      truth value passed as a boolean argument *)
   val branch: (D.t, G.t, C.t, V.t) ctx -> exp -> bool -> D.t
+
+  (** A transfer function which handles going from the start node of a function (fundec) into
+      its function body. Meant to handle, e.g., initialization of local variables *)
   val body  : (D.t, G.t, C.t, V.t) ctx -> fundec -> D.t
+
+  (** A transfer function which handles the return statement, i.e.,
+      "return exp" or "return" in the passed function (fundec) *)
   val return: (D.t, G.t, C.t, V.t) ctx -> exp option  -> fundec -> D.t
+
+  (** A transfer function meant to handle inline assembler program points *)
   val asm   : (D.t, G.t, C.t, V.t) ctx -> D.t
-  val skip  : (D.t, G.t, C.t, V.t) ctx -> D.t
 
+  (** A transfer function which works as the identity function, i.e., it skips and does nothing.
+      Used for empty loops. *)
+  val skip  : (D.t, G.t, C.t, V.t) ctx -> D.t
 
+  (** A transfer function which, for a call to a {e special} function f "lval = f(args)" or "f(args)",
+      computes the caller state after the function call *)
   val special : (D.t, G.t, C.t, V.t) ctx -> lval option -> varinfo -> exp list -> D.t
+
+  (** For a function call "lval = f(args)" or "f(args)",
+      [enter] returns a caller state, and the initial state of the callee.
+      In [enter], the caller state can usually be returned unchanged, as [combine_env] and [combine_assign] (below)
+      will compute the caller state after the function call, given the return state of the callee *)
   val enter   : (D.t, G.t, C.t, V.t) ctx -> lval option -> fundec -> exp list -> (D.t * D.t) list
 
   (* Combine is split into two steps: *)