tutorial contains C code with errors

[Smattr]

CBMC version: e1ecf26
Operating system: N/A
Exact command line resulting in the issue: N/A
What behaviour did you expect: Conforming C code in docs
What happened instead: Typo?

I'm not sure if this is intentional or not, but the CBMC tutorial contains two C examples that look incorrect to me. The first is in Verifying Modules:

int array[10];
int sum() {
  unsigned i, sum;

  sum=0;
  for(i=0; i<10; i++)
    sum+=array[i];
}

Shouldn't this function be returning sum at the end?

The second instance is in Unbounded Loops:

_Bool nondet_bool();
_Bool LOCK = 0;

_Bool lock()
{
  if(nondet_bool())
  {
    assert(!LOCK);
    LOCK = 1;
    return 1;
  }

  return 0;
}

void unlock()
{
  assert(LOCK);
  LOCK = 0;
}

int main()
{
  unsigned got_lock = 0;
  int times;

  while(times > 0)
  {
    if(lock())
    {
      got_lock++;
      /* critical section */
    }

    if(got_lock != 0)
      unlock();

    got_lock--;
    times--;
  }
}

This code reads from the uninitialized variable times which is undefined behavior in C.

Am I misunderstanding something? Maybe these examples are intentionally like this? It caught me by surprise when running through the tutorial.

[kroening]

Many thanks -- I've opened PR #3696 to fix both problems.

[tautschnig]

Fixed via #3696.