Approximately check if result of addition is subnormal with KLEE

test_subnormal_result_implies_exact_result.c

#include "klee/klee.h"
#include <assert.h>
#include <math.h>
#include <stdio.h>

int is_subnormal(float f) {
  return fpclassify(f) == FP_SUBNORMAL;
}

int main() {
  float a = 0.0;
  float b = 0.0;

  klee_make_symbolic(&a, sizeof(a), "a");
  klee_make_symbolic(&b, sizeof(b), "b");

  float result = a + b;
  if (!is_subnormal(result))
    return 0;

  printf("Have subnormal result\n");

  // Approximately check the addition
  // was exact. Not sure how good this
  // approximation is.
  assert( (result -b) == a);
}