Libraries: Folly

SAW and Folly

Folly has a function folly::usingJEMalloc which is problematic for SAW. Here's how to override it's behavior (assuming you didn't link Folly with JEMalloc):

// The mangled function name:
let follyUsingJEMallocName = "_ZZN5folly13usingJEMallocEvENKUlvE_clEv";
// The spec: always return false
let follyUsingJEMalloc_spec = do {
    // %"class.std::__1::allocator" = type { i8 }
    p <- crucible_fresh_pointer (llvm_type "{ i8 }");
    crucible_execute_func [];
    crucible_return (crucible_term {{ 0 : [1] }});
};
usingJEMalloc <-
  crucible_llvm_unsafe_assume_spec m follyUsingJEMallocName follyUsingJEMalloc_spec;