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
|
// RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out -function-alias=printf:highlight_prefix_printf %t.bc 2>&1 | FileCheck --check-prefix=CHECK-HIGHLIGHT %s
// RUN: rm -rf %t.klee-out
// RUN: not %klee --output-dir=%t.klee-out -function-alias=printf:printf_format_only %t.bc 2>&1 | FileCheck --check-prefix=CHECK-VA-FAIL %s
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out -function-alias=printf:printf_format_only_with_varargs %t.bc 2>&1 | FileCheck --check-prefix=CHECK-VA-SUCCESS %s
#include <stdarg.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
// CHECK-HIGHLIGHT: KLEE: function-alias: replaced @printf with @highlight_prefix_printf
int highlight_prefix_printf(const char *format, ...) {
va_list args;
int result;
const char *bold_start = "*+*";
const char *bold_end = "*+*";
va_start(args, format);
const char *prefix = va_arg(args, const char *);
const char *prefixless_format = strstr(format, "%s") + 2;
size_t new_length = strlen(bold_start) + strlen(prefix) + strlen(bold_end) + strlen(prefixless_format) + 1;
char *new_format = (char *)malloc(new_length);
memset(new_format, 0, new_length);
strcat(new_format, bold_start);
strcat(new_format, prefix);
strcat(new_format, bold_end);
strcat(new_format, prefixless_format);
result = vfprintf(stdout, new_format, args);
va_end(args);
free(new_format);
return result;
}
// CHECK-VA-FAIL: KLEE: WARNING: function-alias: @printf could not be replaced with @printf_format_only: one has varargs while the other does not
int printf_format_only(const char *format) {
int result;
result = puts(format);
return result;
}
// CHECK-VA-SUCCESS: KLEE: function-alias: replaced @printf with @printf_format_only_with_varargs
int printf_format_only_with_varargs(const char *format, ...) {
int result;
result = puts(format);
return result;
}
int main() {
int i = 42;
// CHECK: KLEE: some warning about 42
// CHECK-HIGHLIGHT: *+*KLEE*+*
// CHECK-VA-SUCCESS: %s: some warning about %d
printf("%s: some warning about %d\n", "KLEE", i);
}
|
