25 lines
559 B
C
25 lines
559 B
C
// Optional KLEE confirmation fixture for Fold's future DAST lane.
|
|
// Build/run with tests/confirmation/klee/run_klee_smoke.sh when KLEE is installed.
|
|
#include <stddef.h>
|
|
|
|
#ifdef KLEE
|
|
#include <klee/klee.h>
|
|
#endif
|
|
|
|
int vulnerable_copy(unsigned idx) {
|
|
char buf[8] = {0};
|
|
if (idx >= 16)
|
|
return 0;
|
|
buf[idx] = 'X'; // idx in [8,15] is an out-of-bounds write.
|
|
return buf[0];
|
|
}
|
|
|
|
int main(void) {
|
|
unsigned idx = 0;
|
|
#ifdef KLEE
|
|
klee_make_symbolic(&idx, sizeof(idx), "idx");
|
|
#else
|
|
idx = 9;
|
|
#endif
|
|
return vulnerable_copy(idx);
|
|
}
|