CXX and SAW - GaloisInc/saw-script GitHub Wiki

SAW can be used on some C++ code. Some things to keep in mind:

• Always compile C and C++ code with -O1 and -g
• You will have to compile libc++ (or another C++ standard library) to bitcode and link it with your application with llvm-link
• You should compile with -fno-threadsafe-statics to avoid unnecessary inclusion of pthreads material
• You will likely have to initialize several globals
• The functions you're trying to verify will probably have mangled names
• You have to construct all objects "by hand" with e.g. crucible_alloc, crucible_points_to, etc. There is no support for calling constructors in specifications.
• Functions and types that appear in namespaces will often have names in quotes. For example, if this type appears in your LLVM code, you can refer to it in SAW like this:

%"class.quux::Foo" = type { i32, i32 }

let foo_type = llvm_type "%\"class.quux::Foo\"";