blob: f95e2a52b3648292303e836aa1a96af69a47d564 (
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
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
|
// // Test for 32-bit
// RUN: %llvmgcc %s -emit-llvm -m32 -g -std=c99 -c -o %t_32.bc
// RUN: rm -rf %t.klee-out_32
// RUN: %klee --output-dir=%t.klee-out_32 --svcomp-runtime %t_32.bc > %t.kleeoutput.32.log 2>&1
// RUN: FileCheck -check-prefix=first-CHECK -input-file=%t.kleeoutput.32.log %s
// RUN: FileCheck -check-prefix=second-CHECK -input-file=%t.kleeoutput.32.log %s
// RUN: not test -f %t.klee-out_32/test*.err
// Test again for 64-bit
// RUN: %llvmgcc %s -emit-llvm -m64 -g -std=c99 -c -o %t_64.bc
// RUN: rm -rf %t.klee-out_64
// RUN: %klee --output-dir=%t.klee-out_64 --svcomp-runtime %t_64.bc > %t.kleeoutput.64.log 2>&1
// RUN: FileCheck -check-prefix=first-CHECK -input-file=%t.kleeoutput.64.log %s
// RUN: FileCheck -check-prefix=second-CHECK -input-file=%t.kleeoutput.64.log %s
// RUN: not test -f %t.klee-out_64/test*.err
// first-CHECK: completed paths = 1
// second-CHECK-NOT: ERROR
// second-CHECK-NOT: abort
#include "klee/klee.h"
#include "klee/klee_svcomp.h"
#define test_call_D(NAME,T) \
{ \
T initialValue = __VERIFIER_nondet_ ## NAME(); \
if (!klee_is_symbolic(initialValue)) { \
klee_warning("Failed to get symbolic value for type " # T); \
klee_abort(); \
} \
}
#define test_call_ptr_D(NAME,T) \
{ \
T initialValue = __VERIFIER_nondet_ ## NAME(); \
if (!klee_is_symbolic((uintptr_t) initialValue)) { \
klee_warning("Failed to get symbolic value for type " # T); \
klee_abort(); \
} \
}
#define test_call(NAME) test_call_D(NAME,NAME)
#define test_call_ptr(NAME) test_call_ptr_D(NAME,NAME)
int main() {
test_call_D(bool,_Bool);
test_call(char);
{
float initialValue = __VERIFIER_nondet_float();
if (klee_is_symbolic(initialValue)) {
klee_warning("Did not expect float to be symbolic");
klee_abort();
}
}
test_call(int)
test_call(long)
test_call(loff_t)
test_call_ptr_D(pointer,void*)
test_call_ptr_D(pchar,char*)
{
pthread_t initialValue = __VERIFIER_nondet_pthread_t();
if (!klee_is_symbolic(initialValue.id)) {
klee_warning("Failed to get symbolic value for id field");
klee_abort();
}
}
test_call(sector_t)
test_call(short)
test_call(size_t)
test_call_D(u32, uint32_t)
test_call_D(uchar,unsigned char)
test_call_D(uint, unsigned int)
test_call_D(ulong, unsigned long)
test_call(unsigned)
test_call_D(ushort, unsigned short)
return 0;
}
|
