about summary refs log tree commit diff homepage
path: root/runtime/Intrinsic/klee_choose.c
blob: 44e5cea2f23424120d45c760e302f9d03326a4b7 (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
/*===-- klee-choose.c -----------------------------------------------------===//
//
//                     The KLEE Symbolic Virtual Machine
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===*/

#include "klee/klee.h"

uintptr_t klee_choose(uintptr_t n) {
  uintptr_t x;
  klee_make_symbolic(&x, sizeof x, "klee_choose");

  /* NB: this will *not* work if they don't compare to n values. */
  if(x >= n)
    klee_silent_exit(0);
  return x;
}