blob: 9d80ef7d56c2c4ff13d05d68b1617dd7b03a6c22 (
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
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
|
// REQUIRES: lt-llvm-11.0
// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// NOTE: Have to pass `--optimize=false` to avoid vector operations being
// constant folded away.
// RUN: %klee --output-dir=%t.klee-out --optimize=false %t1.bc > %t.stdout.log 2> %t.stderr.log
// RUN: FileCheck -input-file=%t.stderr.log %s
#include "klee/klee.h"
#include <assert.h>
#include <stdint.h>
#include <stdio.h>
typedef uint32_t v4ui __attribute__((vector_size(16)));
int main() {
v4ui f = {1, 2, 3, 4};
int k = klee_range(0, 10, "k");
if (k == 0) {
// CHECK-DAG: [[@LINE+1]]: Out of bounds write when inserting element
f[4] = 255; // Out of bounds write
}
if (k == 1) {
// CHECK-DAG: [[@LINE+1]]: Out of bounds read when extracting element
printf("f[4] = %u\n", f[5]); // Out of bounds
}
if (k > 6) {
// Performing read should be ExtractElement instruction.
// For now this is an expected limitation.
// CHECK-DAG: [[@LINE+1]]: ExtractElement, support for symbolic index not implemented
uint32_t readValue = f[k];
}
else {
// Performing write should be InsertElement instructions.
// For now this is an expected limitation.
// CHECK-DAG: [[@LINE+1]]: InsertElement, support for symbolic index not implemented
f[k] = 255;
}
return 0;
}
|
