Document Spec lifter modules

src/framework/control.ml

@@ -40,8 +40,8 @@ let spec_module: (module Spec) Lazy.t = lazy (
       (* Widening tokens must be outside of hashcons, because widening token domain ignores token sets for identity, so hashcons doesn't allow adding tokens.
          Also must be outside of deadcode, because deadcode splits (like mutex lock event) don't pass on tokens. *)
       |> lift (get_bool "ana.widen.tokens") (module WideningTokens.Lifter)
-      |> lift true (module LongjmpLifter.LongjmpLifter)
-      |> lift termination_enabled (module RecursionTermLifter.RecursionTermLifter) (* Always activate the recursion termination analysis, when the loop termination analysis is activated*)
+      |> lift true (module LongjmpLifter.Lifter)
+      |> lift termination_enabled (module RecursionTermLifter.Lifter) (* Always activate the recursion termination analysis, when the loop termination analysis is activated*)
     )
   in
   GobConfig.building_spec := false;

src/lifters/longjmpLifter.ml

@@ -3,7 +3,7 @@ open Analyses
 open GobConfig
 
 
-module LongjmpLifter (S: Spec): Spec =
+module Lifter (S: Spec): Spec =
 struct
   include S
 

src/lifters/longjmpLifter.mli

@@ -0,0 +1,3 @@
+(** Analysis lifter for [longjmp] and [setjmp] support. *)
+
+module Lifter: Analyses.Spec2Spec

src/lifters/recursionTermLifter.ml

@@ -2,8 +2,7 @@ open GoblintCil
 open Analyses
 
 
-(** Add cycle detection in the context-sensitive dynamic function call graph to an analysis *)
-module RecursionTermLifter (S: Spec)
+module Lifter (S: Spec)
   : Spec with module D = S.D
           and module C = S.C
 =

src/lifters/recursionTermLifter.mli

@@ -0,0 +1,3 @@
+(** Cycle detection in the context-sensitive dynamic function call graph of an analysis. *)
+
+module Lifter: Analyses.Spec2Spec

src/lifters/specLifters.ml

@@ -1,3 +1,5 @@
+(** Various simple and old analysis lifters. *)
+
 open Batteries
 open GoblintCil
 open Analyses