Added test for size_of_val (showing it is stuck)

Author: mariaKt

kmir/src/tests/integration/data/prove-rs/intrinsics.rs

@@ -59,3 +59,10 @@ pub fn test_ctlz_nonzero() {
     let r = unsafe { intrinsics::ctlz_nonzero(x) };
     assert!(r == 31);
 }
+
+#[no_mangle]
+pub fn test_size_of_val() {
+    let x: u32 = 0;
+    let r = unsafe { intrinsics::size_of_val(&x as *const u32) };
+    assert!(r == 4);
+}

kmir/src/tests/integration/data/prove-rs/show/intrinsics.test_size_of_val.expected

@@ -0,0 +1,15 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (32 steps)
+└─ 3 (stuck, leaf)
+    #execIntrinsic ( IntrinsicFunction ( symbol ( "size_of_val" ) ) , operandMove (
+    span: 232
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram ~> .K
+
+

kmir/src/tests/integration/test_integration.py

@@ -28,7 +28,7 @@
 PROVE_DIR = (Path(__file__).parent / 'data' / 'prove-rs').resolve(strict=True)
 PROVE_FILES = list(PROVE_DIR.glob('*.*'))
 PROVE_START_SYMBOLS = {
-    'intrinsics': ['main', 'test_rotate_left', 'test_bswap', 'test_ctpop', 'test_ctlz_nonzero'],
+    'intrinsics': ['main', 'test_rotate_left', 'test_bswap', 'test_ctpop', 'test_ctlz_nonzero', 'test_size_of_val'],
     'symbolic-args-fail': ['main', 'eats_all_args'],
     'symbolic-structs-fail': ['eats_struct_args'],
     'unchecked_arithmetic': ['unchecked_add_i32', 'unchecked_sub_usize', 'unchecked_mul_isize'],