about summary refs log tree commit diff homepage
path: root/test/Feature/Float.c
blob: dce082c673cf2f960173d8c4fc3876e9f7ba4748 (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
// RUN: %llvmgcc -emit-llvm -g -c %s -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out %t.bc > %t.log
// RUN: grep "3.30* -1.10* 2.420*" %t.log

#include <stdio.h>

float fadd(float a, float b) {
  return a + b;
}

float fsub(float a, float b) {
  return a - b;
}

float fmul(float a, float b) {
  return a * b;
}

int main() {
  printf("%f %f %f\n", fadd(1.1, 2.2), fsub(1.1, 2.2), fmul(1.1, 2.2));
  return 0;
}