about summary refs log tree commit diff homepage
path: root/test/Feature/DefineFixedObject.c
blob: 36822434aa173d65bda3ef5af84168487260e9e3 (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
// RUN: %llvmgcc -c -o %t1.bc %s
// RUN: %klee --exit-on-error %t1.bc

#include <stdio.h>

#define ADDRESS ((int*) 0x0080)

int main() {
  klee_define_fixed_object(ADDRESS, 4);
  
  int *p = ADDRESS;

  *p = 10;
  printf("*p: %d\n", *p);

  return 0;
}