Advanced SMACK guide

[keram88]

Hello,

I have been exploring some new use cases for SMACK and encountered a need to create some uninterpreted functions at the C level, such as the following:

float fake_sqrtf(float x) {
  float ret = __VERIFIER_nondet_float();
  __SMACK_top_decl("function abst_sqrt(x: bvfloat) returns (bvfloat);");
  __SMACK_code("@f := abst_sqrt(@f);", ret, x);
  __VERIFIER_assume(!isnan(ret));
  return ret;
}

We could include documentation in the SMACK documents to detail how to do this and perhaps other advanced use cases.