The C bounded model checker: criminally underused(philipzucker.com)

   $ cc -Wall -Werror bar.c
   bar.c:5:11: error: variable 'x' is uninitialized when used here [-Werror,-Wuninitialized]
      if (x <= 42){
          ^
   bar.c:4:12: note: initialize the variable 'x' to silence this warning
      int x;
           ^
            = 0

   $ cc --version
   clang version 16.0.6

   $ gcc -Wall -Werror bar.c
   bar.c: In function 'main':
   bar.c:5:10: error: 'x' is used uninitialized [-Werror=uninitialized]
    5 |       if (x <= 42){
      |          ^
   bar.c:4:11: note: 'x' was declared here
    4 |       int x;
      |           ^
   cc1: all warnings being treated as errors

   $ gcc --version
   gcc 12.2.0

    MODULE Example;

    FROM InOut IMPORT WriteString, Write, WriteLn;

    PROCEDURE get(buffer : ARRAY OF CHAR): CHAR;
    BEGIN
      RETURN buffer[10]; (* This will boom unless compiled with bounds checking disabled, in which case who knows *)
    END get;

    VAR
      buffer : ARRAY [0..9] OF CHAR;

    BEGIN
        WriteString('The out of bounds character is');
        Write(get(buffer));
        WriteLn;
    END Example.