From 76751d4947cc013c5c439e9b79b9733b9676fc19 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Mon, 13 Nov 2023 17:59:28 +0100 Subject: [PATCH] Termination analysis: Insert only one increment statement, do not set assume no overflow. --- src/maingoblint.ml | 3 +-- src/util/terminationPreprocessing.ml | 8 +------- 2 files changed, 2 insertions(+), 9 deletions(-) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index c44a6d9360..3d9959ba6c 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -164,8 +164,7 @@ let check_arguments () = if List.mem "termination" @@ get_string_list "ana.activated" then ( if GobConfig.get_bool "incremental.load" || GobConfig.get_bool "incremental.save" then fail "termination analysis is not compatible with incremental analysis"; set_list "ana.activated" (GobConfig.get_list "ana.activated" @ [`String ("threadflag")]); - set_string "sem.int.signed_overflow" "assume_none"; - warn "termination analysis implicitly activates threadflag analysis and set sem.int.signed_overflow to assume_none" + warn "termination analysis implicitly activates threadflag analysis." ); if not (get_bool "ana.sv-comp.enabled") && get_bool "witness.graphml.enabled" then fail "witness.graphml.enabled: cannot generate GraphML witness without SV-COMP mode (ana.sv-comp.enabled)" diff --git a/src/util/terminationPreprocessing.ml b/src/util/terminationPreprocessing.ml index b6ffc12c14..eb950b1dbb 100644 --- a/src/util/terminationPreprocessing.ml +++ b/src/util/terminationPreprocessing.ml @@ -52,14 +52,8 @@ class loopCounterVisitor lc (fd : fundec) = object(self) 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, 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; - | ss -> - b.bstmts <- exit_stmt :: inc_stmt :: ss; - ); + b.bstmts <- exit_stmt :: inc_stmt :: b.bstmts; lc := VarToStmt.add (v: varinfo) (s: stmt) !lc; let nb = mkBlock [init_stmt; mkStmt s.skind] in s.skind <- Block nb;