Skip to content
Langston Barrett edited this page Sep 23, 2019 · 3 revisions

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\"";
Clone this wiki locally