Merge pull request #1 from dannem1337/presentation

Presentation

regression-tests/double/Answers

@@ -1,42 +1,41 @@
-
 regression-tests/double/add_1.c
 SAFE
 
 regression-tests/double/add_2.c
-SAFE
+UNSAFE
+
+regression-tests/double/add_3.c
+UNSAFE
 
 regression-tests/double/div_1.c
 SAFE
 
 regression-tests/double/div_2.c
-SAFE
+UNSAFE
 
-regression-tests/double/mul_1.c
+regression-tests/double/div_3.c
 SAFE
 
-regression-tests/double/mul_2.c
+regression-tests/double/init_1.c
 SAFE
 
-regression-tests/double/nan.c
-UNSAFE
-
-regression-tests/double/nan_range.c
+regression-tests/double/init_2.c
 SAFE
 
-regression-tests/double/sub_1.c
+regression-tests/double/mul_1.c
 SAFE
 
-regression-tests/double/sub_2.c
-SAFE
+regression-tests/double/mul_2.c
+UNSAFE
 
-regression-tests/double/int_plus_double.c
+regression-tests/double/loop_1.c
 SAFE
 
-regression-tests/double/init_1.c
-SAFE
+regression-tests/double/loop_2.c
+UNSAFE
 
-regression-tests/double/init_2.c
+regression-tests/double/sub_1.c
 SAFE
 
-regression-tests/double/init_3.c
+regression-tests/double/sub_2.c
 UNSAFE

regression-tests/double/add_1.c

@@ -1,6 +1,7 @@
+// SAFE
 int main () {
-  double a = 4.0f;
-  double b = 2.0f;
-  assert(a+b== 6.0f);
+  double a = 0.22;
+  double b = 0.1;
+  assert(a+b== 0.32);
   return 0;
 }

regression-tests/double/add_2.c

@@ -1,6 +1,7 @@
+//UNSAFE
 int main() {
-  double a = 3.0f;
-  double b = 0.5f;
-  assert(a+b == 3.5f);
+  double a = 3.0;
+  double b = 0.5;
+  assert(a+b == 3.501);
   return 0;
 }

regression-tests/double/add_3.c

@@ -1,5 +1,6 @@
+//UNSAFE
 int main() {
-  double a = 2.0f;
-  double b = a + 0.5f;
-  assert(a + 0.4f == b);
+  double a = 2.0;
+  double b = a + 0.5;
+  assert(a + 0.4 == b);
 }

regression-tests/double/div_1.c

@@ -1,6 +1,7 @@
+//SAFE
 int main () {
-  double a = 4.0f;
-  double b = 2.0f;
-  assert(a/b== 2.0f);
+  double a = 4.0;
+  double b = 0.5;
+  assert(a/b== 8.0);
   return 0;
 }

regression-tests/double/div_2.c

@@ -1,6 +1,7 @@
+//UNSAFE
 int main () {
-  double a = 4.0f;
-  double b = 0.5f;
-  assert(a/b== 8.0f);
+  double a = 4.0;
+  double b = 0.5;
+  assert(a/b== 8.01);
   return 0;
 }

regression-tests/double/div_3.c

@@ -1,7 +1,7 @@
-//SAFE (WILL BE UNSAFE DUE TO APPROXIMATIONS FROM FRACTION)
 int main () {
   double a = 4.0;
   double b = 0.1;
-  assert(a/b== 40.0);
+  assert(a/b <= 40.00001);
+  assert(a/b >= 39.99999);
   return 0;
 }

regression-tests/double/init_1.c

@@ -1,6 +1,7 @@
+//SAFE
 int main() {
-  double a = 0.0f;
-  assert(a == 0.0f);
+  double a = 0.0;
+  assert(a == 0.0);
   return 0;
 
 }

regression-tests/double/init_2.c

@@ -1,5 +1,6 @@
+//SAFE
 int main() {
-  double a = 4.24242f;
-  assert(a == 4.24242f);
+  double a = 4.24242;
+  assert(a == 4.24242);
   return 0;
 }

regression-tests/double/init_3.c

@@ -1,6 +1,7 @@
+//UNSAFE
 int main() {
-  double a = 4.24242f;
-  assert(a == 4.24241f);
+  double a = 4.24242;
+  assert(a == 4.24241);
   return 0;
 
 }

regression-tests/double/int_plus_float.c

@@ -1,7 +1,7 @@
-int main ()
-{
-  double a = 2.0f;
+//SAFE
+int main () {
+  double a = 2.0;
   int b = 1;
-  assert(a+b == 3.0f);
+  assert(a+b == 3.0);
   return 0;
 }

regression-tests/double/leq_1.c

@@ -1,5 +1,6 @@
+//SAFE
 int main() {
-  double a = 2.3f;
-  double b = 2.25f;;
+  double a = 2.3;
+  double b = 2.25;;
   assert(b <= a);
 }

regression-tests/double/loop_1.c

@@ -1,11 +1,10 @@
-int N = _;
-
+//SAFE
 void main(void) {
   int i = 0;
   double x = 0.5;
   double y = x;
-  while (i < N) {
-    x = x*2.0f;
+  while (x < 3000.0) {
+    x = x*2.0;
     y = x;
     ++i;
   }

regression-tests/double/loop_2.c

@@ -1,13 +1,15 @@
+//UNSAFE
 int N = _;
 
 void main(void) {
   int i = 0;
   double x = 0.5;
   double y = x;
   while (i < N) {
-    x = x*2.0f;
-    y = x;
+    if(x == y) {
+        x = x+2.25;
+    }
     ++i;
   }
-  assert(x==y+1.0f);
+  assert(x==y);
 }

regression-tests/double/mul_1.c

@@ -1,6 +1,7 @@
+//SAFE
 int main () {
-  double a = 4.0f;
-  double b = 2.0f;
-  assert(a*b== 8.0f);
+  double a = 0.5;
+  double b = 0.5;
+  assert(a*b== 0.25);
   return 0;
 }

regression-tests/double/mul_2.c

@@ -1,6 +1,6 @@
 int main () {
-  double a = 4.0f;
-  double b = 0.5f;
-  assert(a*b== 2.0f);
+  double a = 0.5;
+  double b = 0.5;
+  assert(a*b== 0.251);
   return 0;
 }

regression-tests/double/nan.c

@@ -1,3 +1,4 @@
+//UNSAFE IF NAN IS INCLUDED OTHERWISE SAFE
 int main()
 {
   double x = _;

regression-tests/double/nan_create.c

@@ -1,3 +1,4 @@
+//UNSAFE
 int main() {
   double nan = 0/0;
   assert(nan == 2);

regression-tests/double/nan_range.c

@@ -1,8 +1,8 @@
-int main()
-{
+// SAFE
+int main() {
   double x = _;
 
-  if (x >= -0.00001f && x <= -0.00001f) {
+  if (x >= -0.00001 && x <= -0.00001) {
     assert(x==x); 
   }
   return 0;

regression-tests/double/nondet_1.c

@@ -1,6 +1,7 @@
+// SAFE
 int main() {
   double x = _;
-  double y = x + 1.0f;
+  double y = x + 1.0;
   assert(y>x);
 
 }

regression-tests/double/nondet_2.c

@@ -1,5 +1,6 @@
+// UNSAFE
 int main() {
   double x = _;
-  double y = x + 1.0f;
+  double y = x + 1.0;
   assert(y<x);
 }

regression-tests/double/runtests

@@ -4,18 +4,18 @@ LAZABS=./tri
 
 TESTS="regression-tests/double/add_1.c \
        regression-tests/double/add_2.c \
+       regression-tests/double/add_3.c \
        regression-tests/double/div_1.c \
        regression-tests/double/div_2.c \
+       regression-tests/double/div_3.c \
+       regression-tests/double/init_1.c \
+       regression-tests/double/init_2.c \
        regression-tests/double/mul_1.c \
        regression-tests/double/mul_2.c \
-       regression-tests/double/nan.c \
-       regression-tests/double/nan_range.c \
+       regression-tests/double/loop_1.c \
+       regression-tests/double/loop_2.c \
        regression-tests/double/sub_1.c \
-       regression-tests/double/sub_2.c \
-       regression-tests/double/int_plus_double.c \
-       regression-tests/double/init_1.c \
-       regression-tests/double/init_2.c \
-       regression-tests/double/init_3.c"
+       regression-tests/double/sub_2.c "
 
 for name in $TESTS; do
     echo

regression-tests/double/sub_1.c

@@ -1,7 +1,8 @@
+//SAFE
 int main() {
-  double a = 4.0f;
-  double b = 2.0f;
-  assert(a-b== 2.0f);
+  double a = 1.5;
+  double b = 0.5;
+  assert(a-b== 1.0);
   return 0;
 
 }

regression-tests/double/sub_2.c

@@ -1,6 +1,7 @@
+// UNSAFE
 int main() {
-  double a = 3.0f;
-  double b = 0.5f;
-  assert(a-b == 2.5f);
+  double a = 0.22;
+  double b = 0.1;
+  assert(a-b == 0.1);
   return 0;
 }

regression-tests/float/Answers

@@ -1,42 +1,38 @@
-
 regression-tests/float/add_1.c
 SAFE
 
 regression-tests/float/add_2.c
 SAFE
 
+regression-tests/float/add_3.c
+UNSAFE
+
 regression-tests/float/div_1.c
 SAFE
 
 regression-tests/float/div_2.c
 SAFE
 
-regression-tests/float/mul_1.c
-SAFE
-
-regression-tests/float/mul_2.c
+regression-tests/float/init_1.c
 SAFE
 
-regression-tests/float/nan.c
-UNSAFE
-
-regression-tests/float/nan_range.c
+regression-tests/float/init_2.c
 SAFE
 
-regression-tests/float/sub_1.c
+regression-tests/float/loop_1.c
 SAFE
 
-regression-tests/float/sub_2.c
-SAFE
+regression-tests/float/loop_2.c
+UNSAFE
 
-regression-tests/float/int_plus_float.c
+regression-tests/float/mul_1.c
 SAFE
 
-regression-tests/float/init_1.c
-SAFE
+regression-tests/float/mul_2.c
+UNSAFE
 
-regression-tests/float/init_2.c
+regression-tests/float/sub_1.c
 SAFE
 
-regression-tests/float/init_3.c
+regression-tests/float/sub_2.c
 UNSAFE

regression-tests/float/add_1.c

@@ -1,6 +1,6 @@
 int main () {
-  float a = 4.0f;
-  float b = 2.0f;
-  assert(a+b== 6.0f);
+  float a = 0.5f;
+  float b = 0.75f;
+  assert(a+b== 1.25f);
   return 0;
 }

regression-tests/float/div_1.c

@@ -1,6 +1,7 @@
 int main () {
   float a = 4.0f;
-  float b = 2.0f;
-  assert(a/b== 2.0f);
+  float b = 0.1f;
+  assert(a/b <= 40.00001f);
+  assert(a/b >= 39.99999f);
   return 0;
 }