Use of uninitialized variable causes an error

[robby-phd]

For the following code:

#include <stdint.h>
#include <stdio.h>

uint8_t foo(uint8_t x) {
  return 0;
}

int main() {
  uint8_t x;
  printf("foo(x): %d\n", foo(x));
}

SAW gives the following error message:

Simulation error: Invalid load address (lss__alloc1)
  at #0:@main:%0.0:1
...

(Attached is a zip file to easily reduplicate the issue; just uncompress and run run.sh):

In cases like these, it'd probably good to either:

1. give a helpful error message indicating there is use of uninit var and stop the verification process; or
2. continue the verification process by using a fresh symbolic value/free variable, but also outputs a warning to indicate a potential issue in the code (use of uninit var).

saw-uninit-var.zip