Addifing first GDB tests

runtimeverification · Nov 14, 2023 · a87860c · a87860c
1 parent 29bb01e
commit a87860c
Show file tree

Hide file tree

Showing 5 changed files with 2,226 additions and 0 deletions.
diff --git a/test/debugger/commands/simple.gdb b/test/debugger/commands/simple.gdb
@@ -0,0 +1,4 @@
+k start
+k step
+k step 99
+k step
diff --git a/test/debugger/inputs/simple.in.kore b/test/debugger/inputs/simple.in.kore
@@ -0,0 +1 @@
+LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}("$PGM")),inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("0")))))
diff --git a/test/debugger/k-files/simple.k b/test/debugger/k-files/simple.k
@@ -0,0 +1,6 @@
+module SIMPLE
+  imports INT
+
+  rule I => I +Int 1
+    requires I <Int 100
+endmodule
diff --git a/test/debugger/outputs/simple.out.diff.kore b/test/debugger/outputs/simple.out.diff.kore
@@ -0,0 +1 @@
+Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("100")),dotk{}())),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("100")),dotk{}())),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))