Make type of variables used for loop termination analysis more easily…

… exchangable.
goblint · Nov 9, 2023 · 704a8f1 · 704a8f1
1 parent f024fd9
commit 704a8f1
Showing 1 changed file with 17 additions and 7 deletions.
diff --git a/src/util/terminationPreprocessing.ml b/src/util/terminationPreprocessing.ml
@@ -15,13 +15,18 @@ let extract_file_name s =                    (*There still may be a need to filt
 let show_location_id l =
   string_of_int l.line ^ "_" ^ string_of_int l.column ^ "-file" ^ "_" ^  extract_file_name l.file
 
+let counter_ikind = IInt
+let counter_typ = TInt (counter_ikind, [])
+let min_int_exp = Const(CInt(Cilint.zero_cilint, counter_ikind, None))
+let min_int_exp = Const(CInt(Cilint.shift_left_cilint Cilint.mone_cilint ((bytesSizeOfInt counter_ikind)*8-1), IInt, None))
+
 class loopCounterVisitor lc (fd : fundec) = object(self)
   inherit nopCilVisitor
 
   method! vstmt s =
 
     let specialFunction name =
-      { svar  = makeGlobalVar name (TFun(voidType, Some [("exp", intType, [])], false,[]));
+      { svar  = makeGlobalVar name (TFun(voidType, Some [("exp", counter_typ, [])], false,[]));
         smaxid = 0;
         slocals = [];
         sformals = [];
@@ -30,19 +35,24 @@ class loopCounterVisitor lc (fd : fundec) = object(self)
         sallstmts = [];
       } in
 
-    let min_int_exp = Const(CInt(Cilint.shift_left_cilint Cilint.mone_cilint ((bytesSizeOfInt IInt)*8-1), IInt, None)) in
+
+    let increment_expression lval =
+      let et = typeOf lval in
+      let bop = PlusA in
+      let one = Const (CInt (Cilint.one_cilint, counter_ikind, None)) in
+      constFold false (BinOp(bop, lval, one, et))  in
 
     let f_bounded  = Lval (var (specialFunction "__goblint_bounded").svar) in
 
     let action s = match s.skind with
       | Loop (b, loc, eloc, _, _) ->
         let name = "term"^show_location_id loc in
-        let typ = Cil.intType in
-        let v = (Cil.makeLocalVar fd name typ) in (*Not tested for incremental mode*)
+        let v = (Cil.makeLocalVar fd name counter_typ) in (*Not tested for incremental mode*)
+        let lval = Lval (Var v, NoOffset) in
         let init_stmt = mkStmtOneInstr @@ Set (var v, min_int_exp, loc, eloc) in
-        let inc_stmt = mkStmtOneInstr @@ Set (var v, increm (Lval (var v)) 1, loc, eloc) in
-        let inc_stmt2 = mkStmtOneInstr @@ Set (var v, increm (Lval (var v)) 1, loc, eloc) in
-        let exit_stmt = mkStmtOneInstr @@ Call (None, f_bounded, [Lval (var v)], loc, locUnknown) in
+        let inc_stmt = mkStmtOneInstr @@ Set (var v, increment_expression lval, loc, eloc) in
+        let inc_stmt2 = mkStmtOneInstr @@ Set (var v, increment_expression lval, loc, eloc) in
+        let exit_stmt = mkStmtOneInstr @@ Call (None, f_bounded, [lval], loc, locUnknown) in
         (match b.bstmts with
          | s :: ss ->   (*duplicate increment statement here to fix inconsistencies in nested loops*)
            b.bstmts <- exit_stmt :: inc_stmt :: s :: inc_stmt2 :: ss;