From 2ff979bb14dd41896e1ad3f2c3dff6f1af574241 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 10 Nov 2023 19:54:35 +0100 Subject: [PATCH] Simplify variable names --- src/util/terminationPreprocessing.ml | 26 ++++++++++---------------- 1 file changed, 10 insertions(+), 16 deletions(-) diff --git a/src/util/terminationPreprocessing.ml b/src/util/terminationPreprocessing.ml index 32a9468233..8070438943 100644 --- a/src/util/terminationPreprocessing.ml +++ b/src/util/terminationPreprocessing.ml @@ -2,22 +2,16 @@ open GoblintCil module VarToStmt = Map.Make(CilType.Varinfo) (* maps varinfos (= loop counter variable) to the statement of the corresponding loop*) -let extract_file_name s = (*There still may be a need to filter more chars*) - let ls = String.split_on_char '/' s in (*Assuming '/' as path seperator*) - let ls = List.rev ls in - let s' = List.nth ls 0 in - let ls = String.split_on_char '.' s' in - let s' = List.nth ls 0 in - let without_spaces = String.split_on_char ' ' s' in - let s' = String.concat "" without_spaces in - s' - -let show_location_id l = - string_of_int l.line ^ "_" ^ string_of_int l.column ^ "-file" ^ "_" ^ extract_file_name l.file - class loopCounterVisitor lc (fd : fundec) = object(self) inherit nopCilVisitor + (* Counter of variables inserted for termination *) + val mutable vcounter = ref 0 + + method! vfunc _ = + vcounter := 0; + DoChildren + method! vstmt s = let specialFunction name = @@ -36,9 +30,9 @@ class loopCounterVisitor lc (fd : fundec) = object(self) 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 vname = "term" ^ string_of_int loc.line ^ "_" ^ string_of_int loc.column ^ "-id" ^ (string_of_int !vcounter) in + incr vcounter; + let v = Cil.makeLocalVar fd vname Cil.intType in (*Not tested for incremental mode*) 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