runtimeverification · automergerpr-permission-manager · Jun 22, 2026 · Jun 15, 2026 · Jun 15, 2026 · Jun 15, 2026
diff --git a/kmir/src/kmir/kast.py b/kmir/src/kmir/kast.py
@@ -286,6 +286,7 @@ def mk_call_terminator(target: int, arg_count: int) -> KInner:
                                     KApply(
                                         'constOperand(_,_,_)_BODY_ConstOperand_Span_MaybeUserTypeAnnotationIndex_MirConst',
                                         (
+                                            # synthetic span(0) sentinel (see note on the span below)
                                             KApply('span', token(0)),
                                             KApply('noUserTypeAnnotationIndex_BODY_MaybeUserTypeAnnotationIndex', ()),
                                             KApply(
@@ -312,6 +313,9 @@ def mk_call_terminator(target: int, arg_count: int) -> KInner:
                             KApply('UnwindAction::Continue', ()),
                         ),
                     ),
+                    # Synthetic call-site span for this generated entry/main-call terminator (no real source
+                    # location). Note this differs from the rt/configuration.md <currentSpan> default of
+                    # span(-1), which is the "no span yet" sentinel.
                     KApply('span', token(0)),
                 ),
             ),

diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md
@@ -84,11 +84,12 @@ blocks, or call another function).
 
   rule <k> #execStmts(.Statements) => .K  ... </k>
 
-  rule <k> #execStmts(STATEMENT:Statement STATEMENTS:Statements)
+  rule <k> #execStmts((statement(_, SPAN) #as STATEMENT) STATEMENTS:Statements)
          =>
            #execStmt(STATEMENT) ~> #execStmts(STATEMENTS)
          ...
        </k>
+       <currentSpan> _ => SPAN </currentSpan>
 ```
 
 `Statement` execution handles the different `StatementKind`s. Some of
@@ -158,10 +159,11 @@ function call, pushing a new stack frame and returning to a different
 block after the call returns.
 
 ```k
-  rule [termGoto]: <k> #execTerminator(terminator(terminatorKindGoto(I), _SPAN)) ~> _CONT
+  rule [termGoto]: <k> #execTerminator(terminator(terminatorKindGoto(I), SPAN)) ~> _CONT
          =>
            #execBlockIdx(I)
        </k>
+       <currentSpan> _ => SPAN </currentSpan>
 ```
 
 A `SwitchInt` terminator selects one of the blocks given as _targets_,
@@ -173,10 +175,11 @@ will be `129`.
 ```k
   syntax KItem ::= #selectBlock ( SwitchTargets , Evaluation ) [strict(2)]
 
-  rule [termSwitchInt]: <k> #execTerminator(terminator(terminatorKindSwitchInt(DISCR, TARGETS), _SPAN)) ~> _CONT
+  rule [termSwitchInt]: <k> #execTerminator(terminator(terminatorKindSwitchInt(DISCR, TARGETS), SPAN)) ~> _CONT
          =>
            #selectBlock(TARGETS, DISCR)
        </k>
+       <currentSpan> _ => SPAN </currentSpan>
 
   // These rules preserve definedness because all the same subterms show up on each side except:
   // - `branch(...)`, which is a constructor.
@@ -233,9 +236,10 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f
          <target> someBasicBlockIdx(TARGET) => NEWTARGET </target>
          <unwind> _ => UNWIND </unwind>
          <locals> ListItem(typedValue(VAL:Value, _, _)) _ => NEWLOCALS </locals>
+         <currentSpan> _ => NEWSPAN </currentSpan> // restore caller's call-site span
        //</currentFrame>
        // remaining call stack (without top frame)
-       <stack> ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK </stack>
+       <stack> ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS, NEWSPAN)) STACK => STACK </stack>
        <functions> FUNCSMAP </functions>
 
   // no value to return, skip writing
@@ -251,9 +255,10 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f
          <target> someBasicBlockIdx(TARGET) => NEWTARGET </target>
          <unwind> _ => UNWIND </unwind>
          <locals> ListItem(_:NewLocal) _ => NEWLOCALS </locals>
+         <currentSpan> _ => NEWSPAN </currentSpan> // restore caller's call-site span
        //</currentFrame>
        // remaining call stack (without top frame)
-       <stack> ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK </stack>
+       <stack> ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS, NEWSPAN)) STACK => STACK </stack>
        <functions> FUNCSMAP </functions>
 
 ```
@@ -329,13 +334,15 @@ where the returned result should go.
         => #execTerminatorCall(Ty, lookupFunction(FUNCSMAP, Ty), ARGS, DEST, TARGET, UNWIND, SPAN)
         ...
        </k>
+       <currentSpan> _ => SPAN </currentSpan>
        <functions> FUNCSMAP </functions>
 
   rule <k> #execTerminator(terminator(terminatorKindCall(operandMove(place(local(I), PROJS)), ARGS, DEST, TARGET, UNWIND), SPAN))
         => #execTerminatorCall({#projectedCallTy(TYPESMAP, I, PROJS, LOCALS)}:>Ty, lookupFunction(FUNCSMAP, {#projectedCallTy(TYPESMAP, I, PROJS, LOCALS)}:>Ty), ARGS, DEST, TARGET, UNWIND, SPAN)
         ...
        </k>
       <locals> LOCALS </locals>
+      <currentSpan> _ => SPAN </currentSpan>
       <functions> FUNCSMAP </functions>
       <types> TYPESMAP </types>
     requires isTy(#projectedCallTy(TYPESMAP, I, PROJS, LOCALS))
@@ -385,8 +392,9 @@ where the returned result should go.
          <target> OLDTARGET => TARGET </target>
          <unwind> OLDUNWIND => UNWIND </unwind>
          <locals> LOCALS </locals>
+         ... // leaves <currentSpan> unchanged: callee arg setup is related to the caller's call-site span
        </currentFrame>
-       <stack> STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK </stack>
+       <stack> STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS, SPAN)) STACK </stack>
     requires notBool isIntrinsicFunction(FUNC)
 
   // Filter check injected after every call: fires as a cut-point only when the function matches the break-on list
@@ -511,7 +519,7 @@ An operand may be a `Reference` (the only way a function could access another fu
            #setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef(getValue(CALLERLOCALS, I)))
         ...
        </k>
-       <stack> ListItem(StackFrame(_, _, _, _, CALLERLOCALS)) _:List </stack>
+       <stack> ListItem(StackFrame(_, _, _, _, CALLERLOCALS, _)) _:List </stack>
     requires 0 <=Int I
      andBool I <Int size(CALLERLOCALS)
      andBool isTypedValue(CALLERLOCALS[I])
@@ -523,7 +531,7 @@ An operand may be a `Reference` (the only way a function could access another fu
            #setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef(getValue(CALLERLOCALS, I)))
         ...
        </k>
-       <stack> (ListItem(StackFrame(_, _, _, _, CALLERLOCALS) #as CALLERFRAME => #updateStackLocal(CALLERFRAME, I, Moved))) _:List
+       <stack> (ListItem(StackFrame(_, _, _, _, CALLERLOCALS, _) #as CALLERFRAME => #updateStackLocal(CALLERFRAME, I, Moved))) _:List
         </stack>
     requires 0 <=Int I
      andBool I <Int size(CALLERLOCALS)
@@ -657,10 +665,11 @@ Otherwise the provided message is passed to a `panic!` call, ending the program
 ```k
   syntax MIRError ::= AssertError ( AssertMessage )
 
-  rule [termAssert]: <k> #execTerminator(terminator(assert(COND, EXPECTED, MSG, TARGET, _UNWIND), _SPAN)) ~> _CONT
+  rule [termAssert]: <k> #execTerminator(terminator(assert(COND, EXPECTED, MSG, TARGET, _UNWIND), SPAN)) ~> _CONT
          =>
            #expect(COND, EXPECTED, MSG) ~> #execBlockIdx(TARGET)
        </k>
+       <currentSpan> _ => SPAN </currentSpan>
 
   syntax KItem ::= #expect ( Evaluation, Bool, AssertMessage ) [strict(1)]
 
@@ -684,19 +693,21 @@ Other terminators that matter at the MIR level "Runtime" are `Drop` and `Unreach
 Drops are elaborated to Noops but still define the continuing control flow. Unreachable terminators lead to a program error.
 
 ```k
-  rule [termDrop]: <k> #execTerminator(terminator(terminatorKindDrop(_PLACE, TARGET, _UNWIND), _SPAN))
+  rule [termDrop]: <k> #execTerminator(terminator(terminatorKindDrop(_PLACE, TARGET, _UNWIND), SPAN))
          =>
            #execBlockIdx(TARGET)
         ...
        </k>
+       <currentSpan> _ => SPAN </currentSpan>
 
   syntax MIRError ::= "ReachedUnreachable"
 
-  rule [termUnreachable]: <k> #execTerminator(terminator(terminatorKindUnreachable, _SPAN))
+  rule [termUnreachable]: <k> #execTerminator(terminator(terminatorKindUnreachable, SPAN))
          =>
            ReachedUnreachable
         ...
        </k>
+       <currentSpan> _ => SPAN </currentSpan>
 ```
 
 ### Stopping on Program Errors

diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/configuration.md b/kmir/src/kmir/kdist/mir-semantics/rt/configuration.md
@@ -28,7 +28,8 @@ module KMIR-CONFIGURATION
                                    dest:Place,                // place to store return value
                                    target:MaybeBasicBlockIdx, // basic block to return to
                                    UnwindAction,              // action to perform on panic
-                                   locals:List)               // return val, args, local variables
+                                   locals:List,               // return val, args, local variables
+                                   span:Span)                 // call-site span of this frame
 
   configuration <kmir>
                   <k> $PGM:KItem </k>
@@ -42,6 +43,10 @@ module KMIR-CONFIGURATION
                     <target> noBasicBlockIdx </target>
                     <unwind> unwindActionUnreachable </unwind>
                     <locals> .List </locals>
+                    // span of the instruction currently executing in this frame.
+                    // span(-1) is the "no span yet" sentinel (a real Span is an interned, non-negative index).
+                    // Note: this is intentionally distinct from the span(0) synthetic entry/main-call span set in kast.py.
+                    <currentSpan> span(-1) </currentSpan>
                   </currentFrame>
                   // remaining call stack (without top frame)
                   <stack> .List </stack>

diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
@@ -365,8 +365,8 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr
 
   syntax StackFrame ::= #updateStackLocal ( StackFrame, Int, Value ) [function]
 
-  rule #updateStackLocal(StackFrame(CALLER, DEST, TARGET, UNWIND, LOCALS), I, VAL)
-      => StackFrame(CALLER, DEST, TARGET, UNWIND, LOCALS[I <- typedValue(VAL, tyOfLocal(getLocal(LOCALS, I)), mutabilityMut)])
+  rule #updateStackLocal(StackFrame(CALLER, DEST, TARGET, UNWIND, LOCALS, SPAN), I, VAL)
+      => StackFrame(CALLER, DEST, TARGET, UNWIND, LOCALS[I <- typedValue(VAL, tyOfLocal(getLocal(LOCALS, I)), mutabilityMut)], SPAN)
     requires 0 <=Int I
      andBool I <Int size(LOCALS)
      andBool isTypedLocal(LOCALS[I])

diff --git a/kmir/src/tests/integration/data/exec-smir/allocs/array_const_compare.state b/kmir/src/tests/integration/data/exec-smir/allocs/array_const_compare.state
@@ -45,9 +45,12 @@
       ListItem ( typedValue ( Moved , ty ( 30 ) , mutabilityMut ) )
       ListItem ( newLocal ( ty ( 68 ) , mutabilityMut ) )
     </locals>
+    <currentSpan>
+      span ( 278 )
+    </currentSpan>
   </currentFrame>
   <stack>
-    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
+    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List , span ( 0 ) ) )
   </stack>
   <functions>
     noMap

diff --git a/kmir/src/tests/integration/data/exec-smir/allocs/array_nest_compare.state b/kmir/src/tests/integration/data/exec-smir/allocs/array_nest_compare.state
@@ -61,9 +61,12 @@
       ListItem ( typedValue ( Moved , ty ( 30 ) , mutabilityMut ) )
       ListItem ( newLocal ( ty ( 84 ) , mutabilityMut ) )
     </locals>
+    <currentSpan>
+      span ( 266 )
+    </currentSpan>
   </currentFrame>
   <stack>
-    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
+    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List , span ( 0 ) ) )
   </stack>
   <functions>
     noMap

diff --git a/kmir/src/tests/integration/data/exec-smir/allocs/enum-two-refs-fail.state b/kmir/src/tests/integration/data/exec-smir/allocs/enum-two-refs-fail.state
@@ -48,6 +48,9 @@
       ListItem ( newLocal ( ty ( 25 ) , mutabilityMut ) )
       ListItem ( newLocal ( ty ( 25 ) , mutabilityMut ) )
     </locals>
+    <currentSpan>
+      span ( 145 )
+    </currentSpan>
   </currentFrame>
   <stack>
     ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( 0 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionContinue , ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) )
@@ -72,8 +75,8 @@
     ListItem ( newLocal ( ty ( 84 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 1 ) , mutabilityNot ) )
     ListItem ( newLocal ( ty ( 68 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 69 ) , mutabilityNot ) ) ) )
-    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
+    ListItem ( newLocal ( ty ( 69 ) , mutabilityNot ) ) , span ( 116 ) ) )
+    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List , span ( 0 ) ) )
   </stack>
   <functions>
     noMap

diff --git a/kmir/src/tests/integration/data/exec-smir/allocs/option_consts.state b/kmir/src/tests/integration/data/exec-smir/allocs/option_consts.state
@@ -108,9 +108,12 @@
       ListItem ( newLocal ( ty ( 84 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 86 ) , mutabilityMut ) )
     </locals>
+    <currentSpan>
+      span ( 374 )
+    </currentSpan>
   </currentFrame>
   <stack>
-    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
+    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List , span ( 0 ) ) )
   </stack>
   <functions>
     noMap

diff --git a/kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic-unchecked-runs.state b/kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic-unchecked-runs.state
@@ -50,9 +50,12 @@
       ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Moved )
       ListItem ( Moved ) ) , ty ( 36 ) , mutabilityMut ) )
     </locals>
+    <currentSpan>
+      span ( 116 )
+    </currentSpan>
   </currentFrame>
   <stack>
-    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
+    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List , span ( 0 ) ) )
   </stack>
   <functions>
     noMap

diff --git a/kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic.state b/kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic.state
@@ -63,9 +63,12 @@
       ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Moved )
       ListItem ( Moved ) ) , ty ( 29 ) , mutabilityMut ) )
     </locals>
+    <currentSpan>
+      span ( 67 )
+    </currentSpan>
   </currentFrame>
   <stack>
-    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
+    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List , span ( 0 ) ) )
   </stack>
   <functions>
     noMap

diff --git a/kmir/src/tests/integration/data/exec-smir/arithmetic/unary.state b/kmir/src/tests/integration/data/exec-smir/arithmetic/unary.state
@@ -37,9 +37,12 @@
       ListItem ( typedValue ( Integer ( -122 , 8 , true ) , ty ( 2 ) , mutabilityNot ) )
       ListItem ( typedValue ( Moved , ty ( 25 ) , mutabilityMut ) )
     </locals>
+    <currentSpan>
+      span ( 53 )
+    </currentSpan>
   </currentFrame>
   <stack>
-    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
+    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List , span ( 0 ) ) )
   </stack>
   <functions>
     noMap

diff --git a/kmir/src/tests/integration/data/exec-smir/arrays/array_indexing.state b/kmir/src/tests/integration/data/exec-smir/arrays/array_indexing.state
@@ -45,9 +45,12 @@
       ListItem ( typedValue ( Moved , ty ( 30 ) , mutabilityMut ) )
       ListItem ( newLocal ( ty ( 31 ) , mutabilityMut ) )
     </locals>
+    <currentSpan>
+      span ( 56 )
+    </currentSpan>
   </currentFrame>
   <stack>
-    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
+    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List , span ( 0 ) ) )
   </stack>
   <functions>
     noMap

diff --git a/kmir/src/tests/integration/data/exec-smir/arrays/array_inlined.state b/kmir/src/tests/integration/data/exec-smir/arrays/array_inlined.state
@@ -88,9 +88,12 @@
       ListItem ( newLocal ( ty ( 37 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 39 ) , mutabilityMut ) )
     </locals>
+    <currentSpan>
+      span ( 107 )
+    </currentSpan>
   </currentFrame>
   <stack>
-    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
+    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List , span ( 0 ) ) )
   </stack>
   <functions>
     noMap

diff --git a/kmir/src/tests/integration/data/exec-smir/arrays/array_write.state b/kmir/src/tests/integration/data/exec-smir/arrays/array_write.state
@@ -54,9 +54,12 @@
       ListItem ( typedValue ( Moved , ty ( 30 ) , mutabilityMut ) )
       ListItem ( newLocal ( ty ( 32 ) , mutabilityMut ) )
     </locals>
+    <currentSpan>
+      span ( 65 )
+    </currentSpan>
   </currentFrame>
   <stack>
-    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
+    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List , span ( 0 ) ) )
   </stack>
   <functions>
     noMap

diff --git a/kmir/src/tests/integration/data/exec-smir/assign-cast/assign-cast.state b/kmir/src/tests/integration/data/exec-smir/assign-cast/assign-cast.state
@@ -42,9 +42,12 @@
       ListItem ( typedValue ( Integer ( 128 , 8 , false ) , ty ( 9 ) , mutabilityNot ) )
       ListItem ( typedValue ( Integer ( 32896 , 32 , false ) , ty ( 28 ) , mutabilityNot ) )
     </locals>
+    <currentSpan>
+      span ( 65 )
+    </currentSpan>
   </currentFrame>
   <stack>
-    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
+    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List , span ( 0 ) ) )
   </stack>
   <functions>
     noMap

diff --git a/kmir/src/tests/integration/data/exec-smir/call-with-args/closure-call.state b/kmir/src/tests/integration/data/exec-smir/call-with-args/closure-call.state
@@ -44,9 +44,12 @@
       ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 32 , false ) )
       ListItem ( Integer ( 32 , 32 , false ) ) ) , ty ( 32 ) , mutabilityMut ) )
     </locals>
+    <currentSpan>
+      span ( 62 )
+    </currentSpan>
   </currentFrame>
   <stack>
-    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
+    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List , span ( 0 ) ) )
   </stack>
   <functions>
     noMap

diff --git a/kmir/src/tests/integration/data/exec-smir/call-with-args/main-a-b-with-int.state b/kmir/src/tests/integration/data/exec-smir/call-with-args/main-a-b-with-int.state
@@ -29,12 +29,15 @@
       ListItem ( typedValue ( Integer ( 10 , 64 , false ) , ty ( 26 ) , mutabilityNot ) )
       ListItem ( typedValue ( Integer ( 11 , 16 , true ) , ty ( 28 ) , mutabilityNot ) )
     </locals>
+    <currentSpan>
+      span ( 58 )
+    </currentSpan>
   </currentFrame>
   <stack>
     ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( 0 ) , projection: .ProjectionElems ) , someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwindActionContinue , ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) )
-    ListItem ( typedValue ( Integer ( 10 , 64 , false ) , ty ( 26 ) , mutabilityNot ) ) ) )
-    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( 0 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionContinue , ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) ) ) )
-    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
+    ListItem ( typedValue ( Integer ( 10 , 64 , false ) , ty ( 26 ) , mutabilityNot ) ) , span ( 58 ) ) )
+    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( 0 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionContinue , ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) ) , span ( 52 ) ) )
+    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List , span ( 0 ) ) )
   </stack>
   <functions>
     noMap