Source location missing from array initialization in error trace

[markrtuttle]

CBMC version: 5.60.0
Operating system: MacOS

Define the file test.c

int main() {
  char str[] = "ab";
  assert(0);
}

Run the command

cbmc test.c --trace --xml-ui > trace.xml 

Examine the file trace.xml and notice that the allocation of str has a source location but the assignments of the initial values to the array components to their initial values are missing their source locations.

    <assignment assignment_type="state" base_name="str" display_name="main::1::str" hidden="true" identifier="main::1::str" mode="C" step_nr="21" thread="0">                                    
      <location file="test.c" function="main" line="2" working-directory="/private/tmp"/>                                                                                                        
      <full_lhs_type>char [3l]</full_lhs_type>                                                                                                                                                   
      <full_lhs>str</full_lhs>                                                                                                                                                                   
      <full_lhs_value>{ 0, 0, 0 }</full_lhs_value>                                                                                                                                               
    </assignment>                                                                                                                                                                                
    <assignment assignment_type="state" base_name="str" display_name="main::1::str" hidden="false" identifier="main::1::str" mode="C" step_nr="22" thread="0">                                   
      <full_lhs_type>char [3l]</full_lhs_type>                                                                                                                                                   
      <full_lhs>str</full_lhs>                                                                                                                                                                   
      <full_lhs_value>{ 'a', 'b', 0 }</full_lhs_value>                                                                                                                                           
    </assignment>                                                                                                                                                                                
    <assignment assignment_type="state" base_name="str" display_name="main::1::str" hidden="false" identifier="main::1::str" mode="C" step_nr="23" thread="0">                                   
      <full_lhs_type>char</full_lhs_type>                                                                                                                                                        
      <full_lhs>str[0l]</full_lhs>                                                                                                                                                               
      <full_lhs_value binary="01100001">'a'</full_lhs_value>                                                                                                                                     
    </assignment>                                                                                                                                                                                
    <assignment assignment_type="state" base_name="str" display_name="main::1::str" hidden="false" identifier="main::1::str" mode="C" step_nr="24" thread="0">                                   
      <full_lhs_type>char</full_lhs_type>                                                                                                                                                        
      <full_lhs>str[1l]</full_lhs>                                                                                                                                                               
      <full_lhs_value binary="01100010">'b'</full_lhs_value>                                                                                                                                     
    </assignment>                                                                                                                                                                                
    <assignment assignment_type="state" base_name="str" display_name="main::1::str" hidden="false" identifier="main::1::str" mode="C" step_nr="25" thread="0">
      <full_lhs_type>char</full_lhs_type>
      <full_lhs>str[2l]</full_lhs>
      <full_lhs_value binary="00000000">0</full_lhs_value>
    </assignment>