Zile seems to be expecting the `stdscr` symbol to be available. It is likely this is provided by the ncurses library which you probably didn't link zile.bc with.
* You need to build a LLVM bitcode version of ncurses and then link zile.bc with that OR * Implement a model of the ncurses library within KLEE as a runtime library. This would probably be a lot of work. Hope that helps. Thanks, Dan. On 28 December 2013 14:57, Wang Shuai <[email protected]> wrote: > Hi everyone, > > I have been trying to test GNU Zile by klee. After zile.bc generated, I > run klee with following command: > > klee --libc=uclibc --posix-runtime ./zile.bc --help > > Instead of test cases, what I got are error info: > > KLEE: WARNING: undefined reference to variable: COLS > KLEE: WARNING: undefined reference to variable: LINES > KLEE: WARNING: undefined reference to function: __xstat64 > KLEE: WARNING: undefined reference to function: beep > KLEE: WARNING: undefined reference to function: endwin > KLEE: WARNING: undefined reference to function: initscr > KLEE: WARNING: undefined reference to function: intrflush > KLEE: WARNING: undefined reference to function: keypad > KLEE: WARNING: undefined reference to function: meta > KLEE: WARNING: undefined reference to function: noecho > KLEE: WARNING: undefined reference to function: nonl > KLEE: WARNING: undefined reference to function: raw > KLEE: WARNING: undefined reference to variable: stdscr > KLEE: WARNING: undefined reference to function: waddch > KLEE: WARNING: undefined reference to function: wclear > KLEE: WARNING: undefined reference to function: wclrtoeol > KLEE: WARNING: undefined reference to function: wgetch > KLEE: WARNING: undefined reference to function: wmove > KLEE: WARNING: undefined reference to function: wrefresh > KLEE: WARNING: undefined reference to function: wtimeout > KLEE: WARNING: executable has module level assembly (ignoring) > KLEE: ERROR: unable to load symbol(stdscr) while initializing globals. > > As I know, these functions are in curses.h which zile use to build GUI. > But I can't come up with an effective solution. > I hope there will be someone could help me out. Thank you very much! > > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
