about summary refs log tree commit diff homepage
path: root/test/DeterministicAllocation/double-free.c
blob: 141427fac2cfbb8aa6ef53ab8185fa8040c33ebb (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
// RUN: %clang %s -emit-llvm -g -c -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee -kdalloc -kdalloc-quarantine=1 -output-dir=%t.klee-out %t.bc -exit-on-error >%t.output 2>&1
// RUN: FileCheck %s -input-file=%t.output

#include <stdlib.h>

int main() {
  void *ptr = malloc(8);
  free(ptr);

  // CHECK: double free
  free(ptr);

  return 0;
}