runtime/Intrinsic/klee_range.c


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
27
28
29
30
31
32
33
34

//===-- klee_range.c ------------------------------------------------------===//
//
//                     The KLEE Symbolic Virtual Machine
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//

#include <assert.h>
#include <klee/klee.h>

int klee_range(int start, int end, const char* name) {
  int x;

  if (start >= end)
    klee_report_error(__FILE__, __LINE__, "invalid range", "user");

  if (start+1==end) {
    return start;
  } else {
    klee_make_symbolic(&x, sizeof x, name); 

    /* Make nicer constraint when simple... */
    if (start==0) {
      klee_assume((unsigned) x < (unsigned) end);
    } else {
      klee_assume(start <= x);
      klee_assume(x < end);
    }

    return x;
  }
}