Added intrinsics tests to prove show list.

mariaKt · mariaKt · commit 558c0c4ca99d · 2026-06-25T17:41:47.000-05:00
diff --git a/kmir/src/tests/integration/data/prove-rs/show/intrinsics.main.expected b/kmir/src/tests/integration/data/prove-rs/show/intrinsics.main.expected
@@ -0,0 +1,17 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (349 steps)
+├─ 3 (terminal)
+│   #EndProgram ~> .K
+│   function: main
+│
+┊  constraint: true
+┊  subst: ...
+└─ 2 (leaf, target, terminal)
+    #EndProgram ~> .K
+
+
+
diff --git a/kmir/src/tests/integration/data/prove-rs/show/intrinsics.test_bswap.expected b/kmir/src/tests/integration/data/prove-rs/show/intrinsics.test_bswap.expected
@@ -0,0 +1,16 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (56 steps)
+├─ 3 (terminal)
+│   #EndProgram ~> .K
+│
+┊  constraint: true
+┊  subst: ...
+└─ 2 (leaf, target, terminal)
+    #EndProgram ~> .K
+
+
+
diff --git a/kmir/src/tests/integration/data/prove-rs/show/intrinsics.test_ctlz_nonzero.expected b/kmir/src/tests/integration/data/prove-rs/show/intrinsics.test_ctlz_nonzero.expected
@@ -0,0 +1,16 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (41 steps)
+├─ 3 (terminal)
+│   #EndProgram ~> .K
+│
+┊  constraint: true
+┊  subst: ...
+└─ 2 (leaf, target, terminal)
+    #EndProgram ~> .K
+
+
+
diff --git a/kmir/src/tests/integration/data/prove-rs/show/intrinsics.test_ctpop.expected b/kmir/src/tests/integration/data/prove-rs/show/intrinsics.test_ctpop.expected
@@ -0,0 +1,16 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (56 steps)
+├─ 3 (terminal)
+│   #EndProgram ~> .K
+│
+┊  constraint: true
+┊  subst: ...
+└─ 2 (leaf, target, terminal)
+    #EndProgram ~> .K
+
+
+
diff --git a/kmir/src/tests/integration/data/prove-rs/show/intrinsics.test_rotate_left.expected b/kmir/src/tests/integration/data/prove-rs/show/intrinsics.test_rotate_left.expected
@@ -0,0 +1,16 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (69 steps)
+├─ 3 (terminal)
+│   #EndProgram ~> .K
+│
+┊  constraint: true
+┊  subst: ...
+└─ 2 (leaf, target, terminal)
+    #EndProgram ~> .K
+
+
+
diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py
@@ -43,6 +43,7 @@
     'spl-multisig-iter-eq-copied-next': ['repro'],
 }
 PROVE_SHOW_SPECS = [
+    'intrinsics',
     'local-raw-fail',
     'interior-mut-fail',
     'interior-mut3-fail',

Original file line number	Diff line number	Diff line change
`@@ -43,6 +43,7 @@`
`43`	`43`	`'spl-multisig-iter-eq-copied-next': ['repro'],`
`44`	`44`	`}`
`45`	`45`	`PROVE_SHOW_SPECS = [`
	`46`	`+ 'intrinsics',`
`46`	`47`	`'local-raw-fail',`
`47`	`48`	`'interior-mut-fail',`
`48`	`49`	`'interior-mut3-fail',`