From fdca5289223f059fde2a433888e697ea08754035 Mon Sep 17 00:00:00 2001 From: Alan Jowett Date: Tue, 22 Oct 2024 19:11:06 -0700 Subject: [PATCH] PR feedback Signed-off-by: Alan Jowett --- test-data/loop.yaml | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/test-data/loop.yaml b/test-data/loop.yaml index 18a922b0e..0bfc83c45 100644 --- a/test-data/loop.yaml +++ b/test-data/loop.yaml @@ -395,3 +395,22 @@ post: - "r0.uvalue=100001" messages: - "exit: Could not prove termination." + +--- +test-case: possible infinite loop +options: ["termination"] + +pre: [r0.type=number] +code: + : | + if r0 > 0 goto + exit + +post: + - "pc[0]=[1, +oo]" + - "r0.svalue=0" + - "r0.uvalue=0" + - "r0.type=number" + +messages: + - "exit: Could not prove termination."