diff --git a/src/framework/control.ml b/src/framework/control.ml index a2fb7c01e9..1d0ebb869b 100644 --- a/src/framework/control.ml +++ b/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; diff --git a/src/lifters/longjmpLifter.ml b/src/lifters/longjmpLifter.ml index 1150bc1bca..1a28085abe 100644 --- a/src/lifters/longjmpLifter.ml +++ b/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 diff --git a/src/lifters/longjmpLifter.mli b/src/lifters/longjmpLifter.mli new file mode 100644 index 0000000000..5fd74907bc --- /dev/null +++ b/src/lifters/longjmpLifter.mli @@ -0,0 +1,3 @@ +(** Analysis lifter for [longjmp] and [setjmp] support. *) + +module Lifter: Analyses.Spec2Spec diff --git a/src/lifters/recursionTermLifter.ml b/src/lifters/recursionTermLifter.ml index 3de3810569..2d9f45de60 100644 --- a/src/lifters/recursionTermLifter.ml +++ b/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 = diff --git a/src/lifters/recursionTermLifter.mli b/src/lifters/recursionTermLifter.mli new file mode 100644 index 0000000000..059cea658f --- /dev/null +++ b/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 diff --git a/src/lifters/specLifters.ml b/src/lifters/specLifters.ml index 3286721bf0..4ce158b8ac 100644 --- a/src/lifters/specLifters.ml +++ b/src/lifters/specLifters.ml @@ -1,3 +1,5 @@ +(** Various simple and old analysis lifters. *) + open Batteries open GoblintCil open Analyses