Merge pull request #1837 from goblint/termination-unflat

Remove unnecessary flat lifting in `LoopTermination`

Author: sim642

src/analyses/loopTermination.ml

@@ -17,11 +17,6 @@ let ask_bound man varinfo =
   | `Lifted v -> `Lifted v
   | `Bot -> failwith "Loop counter variable is Bot."
 
-(** We want to record termination information of loops and use the loop
- * statements for that. We use this lifting because we need to have a
- * lattice. *)
-module Statements = Lattice.Flat (CilType.Stmt)
-
 (** The termination analysis considering loops and gotos *)
 module Spec : Analyses.MCPSpec =
 struct
@@ -37,7 +32,9 @@ struct
     include UnitV
     let is_write_only _ = true
   end
-  module G = MapDomain.MapBot (Statements) (BoolDomain.MustBool)
+
+  (** We want to record termination information of loops and use the loop statements for that. *)
+  module G = MapDomain.MapBot (CilType.Stmt) (BoolDomain.MustBool)
 
   let startstate _ = ()
   let exitstate = startstate
@@ -52,7 +49,7 @@ struct
           | Some loop_statement ->
             let bound = ask_bound man loop_counter in
             let is_bounded = bound <> `Top in
-            man.sideg () (G.add (`Lifted loop_statement) is_bounded (man.global ()));
+            man.sideg () (G.add loop_statement is_bounded (man.global ()));
             let loc = M.Location.CilLocation (Cilfacade.get_stmtLoc loop_statement) in
             begin match bound with
               | `Top ->
@@ -75,7 +72,7 @@ struct
     | Queries.MustTermLoop loop_statement ->
       let multithreaded = man.ask Queries.IsEverMultiThreaded in
       (not multithreaded)
-      && (BatOption.default false (G.find_opt (`Lifted loop_statement) (man.global ())))
+      && (BatOption.default false (G.find_opt loop_statement (man.global ())))
     | Queries.MustTermAllLoops ->
       let multithreaded = man.ask Queries.IsEverMultiThreaded in
       if multithreaded then (