search

smackers / smack

SMACK Software Verifier and Verification Toolchain
http://smackers.github.io
Other
427 stars 82 forks source link

Advanced SMACK guide #798

Open keram88 opened 1 year ago

keram88 commented 1 year ago

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.