Use of uninitialized value in build_goto_trace.cpp

[mgudemann]

The enumeration assignment_typet in SSA_stept is not initialized. To check whether its value is read prior to initialization, I amended the enum with an explicit UNINIT and added assert where the value is read. This shows an uninitialized read in build_goto_trace.cpp:217

    // drop PHI and GUARD assignments altogether
    assert(SSA_step.assignment_type!=symex_targett::UNINIT);
    if(it->is_assignment() &&
       (SSA_step.assignment_type==symex_target_equationt::PHI ||
        SSA_step.assignment_type==symex_target_equationt::GUARD))
      continue;

I will look further where else this problem persists.

[mgudemann]

a second such read is further down at line 241

    assert(SSA_step.assignment_type!=symex_targett::UNINIT);
    goto_trace_step.assignment_type=
      (it->is_assignment()&&
       (SSA_step.assignment_type==symex_targett::VISIBLE_ACTUAL_PARAMETER ||
        SSA_step.assignment_type==symex_targett::HIDDEN_ACTUAL_PARAMETER))?
      goto_trace_stept::ACTUAL_PARAMETER:
      goto_trace_stept::STATE;

[NlightNFotis]

I have tried to reproduce this and I wasn't able to (the UNINIT enum element is no longer present in symex_targett::assignment_typet).

I will be closing this issue for now, but if you find that this is still a problem, please go ahead and reopen the issue and we will investigate further.