I'm noticing that DSA graphs are not created for library functions like "puts". The bytecode file runs with lli, so I think I did my linking okay. Is this normal, or does it mean I'm somehow not giving the algorithm the complete program information it needs?
Not that I know of. For KLEE we did it for uclibc and used that as our
libc without too much trouble. It should be much easier now that we
have wider availability of LTO, in theory compiling with llvm-gcc and
-flto will produce bitcode versions of the libraries out-of-the-box.
In practice, libc implementations use various "interesting" techniques
to get their work done, IIRC glibc doesn't currently build with
llvm-gcc, for example.