about summary refs log tree commit diff homepage
path: root/test/Feature/CheckMemoryAccess.c
blob: dd6e8745f4aca421732be7fabdf0734e7dc97361 (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
// RUN: %llvmgcc -g -c %s -o %t.bc
// RUN: %klee %t.bc > %t.log
// RUN: grep -q "good" %t.log
// RUN: not grep -q "bad" %t.log

#include <assert.h>
#include <stdlib.h>
#include <stdio.h>

int main() {
  char buf[4];

  klee_check_memory_access(&buf, 1);
  printf("good\n");
  if (klee_range(0, 2, "range1")) {
    klee_check_memory_access(0, 1);
    printf("null pointer deref: bad\n");
  }

  if (klee_range(0, 2, "range2")) {
    klee_check_memory_access(buf, 5);
    printf("oversize access: bad\n");
  }

  return 0;
}