Document context gas lifter

goblint · Sep 22, 2024 · 7112baf · 7112baf
1 parent 426ec69
commit 7112baf
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/src/framework/contextGasLifter.ml b/src/framework/contextGasLifter.ml
@@ -1,3 +1,6 @@
+(** Lifts a [Spec] with the context gas variable. The gas variable limits the number of context-sensitively analyzed function calls in a call stack.
+    For every function call the gas is reduced. If the gas is zero, the remaining function calls are analyzed without context-information *)
+
 open Batteries
 open GoblintCil
 open MyCFG
@@ -17,8 +20,6 @@ module type Gas = sig
   val thread_gas: varinfo -> M.t -> M.t
 end
 
-(** Lifts a [Spec] with the context gas variable. The gas variable limits the number of context-sensitively analyzed function calls in a call stack.
-    For every function call the gas is reduced. If the gas is zero, the remaining function calls are analyzed without context-information *)
 module ContextGasLifter (Gas:Gas) (S:Spec)
   : Spec with module D = Lattice.Prod (S.D) (Gas.M)
           and module C = Printable.Option (S.C) (NoContext)

diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml
@@ -26,6 +26,7 @@ module Constraints = Constraints
 module AnalysisState = AnalysisState
 module AnalysisStateUtil = AnalysisStateUtil
 module ControlSpecC = ControlSpecC
+module ContextGasLifter = ContextGasLifter
 
 (** Master control program (MCP) is the analysis specification for the dynamic product of activated analyses. *)