Demo C program with subtle bugs for ESBMC Claude Code plugin verification

demo.c

#include <stdlib.h>

// Bug 1: off-by-one in the loop bound — writes past the end of buf[]
// Bug 2: missing NULL check after malloc — dereferences a potentially NULL pointer

int main() {
    int buf[10];

    for (int i = 0; i <= 10; i++)
        buf[i] = i * 2;

    int *p = malloc(sizeof(int));
    *p = buf[9] + 1;

    int total = 0;
    for (int i = 0; i < 10; i++)
        total += buf[i];

    free(p);
    return total;
}