Support for floating-point arithmetic added

acsl-parser/acsl.cf

@@ -222,19 +222,20 @@ TSetTerm. TSet ::= Term ;
 
 -- C Type Expressions (A.1) --------------------------------
 -- TODO: Missing a lot. 
-CTypeSpecifierVoid.     CTypeSpecifier ::= "void" ;
-CTypeSpecifierChar.     CTypeSpecifier ::= "char" ;
-CTypeSpecifierShort.    CTypeSpecifier ::= "short" ;
-CTypeSpecifierInt.      CTypeSpecifier ::= "int" ;
-CTypeSpecifierLong.     CTypeSpecifier ::= "long" ;
-CTypeSpecifierFloat.    CTypeSpecifier ::= "float" ;
-CTypeSpecifierDouble.   CTypeSpecifier ::= "double" ;
-CTypeSpecifierSigned.   CTypeSpecifier ::= "signed" ;
-CTypeSpecifierUnsigned. CTypeSpecifier ::= "unsigned" ;
-CTypeSpecifierStruct.   CTypeSpecifier ::= "struct" Id ;
-CTypeSpecifierUnion.    CTypeSpecifier ::= "union" Id ;
-CTypeSpecifierEnum.     CTypeSpecifier ::= "enum" Id ;
-CTypeSpecifierId.       CTypeSpecifier ::= Id ;
+CTypeSpecifierVoid.       CTypeSpecifier ::= "void" ;
+CTypeSpecifierChar.       CTypeSpecifier ::= "char" ;
+CTypeSpecifierShort.      CTypeSpecifier ::= "short" ;
+CTypeSpecifierInt.        CTypeSpecifier ::= "int" ;
+CTypeSpecifierLong.       CTypeSpecifier ::= "long" ;
+CTypeSpecifierFloat.      CTypeSpecifier ::= "float" ;
+CTypeSpecifierDouble.     CTypeSpecifier ::= "double" ;
+CTypeSpecifierLongDouble. CTypeSpecifier ::= "long double";
+CTypeSpecifierSigned.     CTypeSpecifier ::= "signed" ;
+CTypeSpecifierUnsigned.   CTypeSpecifier ::= "unsigned" ;
+CTypeSpecifierStruct.     CTypeSpecifier ::= "struct" Id ;
+CTypeSpecifierUnion.      CTypeSpecifier ::= "union" Id ;
+CTypeSpecifierEnum.       CTypeSpecifier ::= "enum" Id ;
+CTypeSpecifierId.         CTypeSpecifier ::= Id ;
 
 
 ---- Tokens ------------------------------------------------ 

build.sbt

@@ -17,6 +17,7 @@ lazy val commonSettings = Seq(
 
 // Jar files for the parsers
 
+
 lazy val parserSettings = Seq(
     publishArtifact in packageDoc := false,
     publishArtifact in packageSrc := false,

cc-parser/concurrentC.cf

@@ -304,8 +304,8 @@ token OctalLong '0'["01234567"]* ('l'|'L');
 
 token OctalUnsLong '0'["01234567"]* (('u''l')|('U''L'));
 
-token CDouble (((digit+ '.')|('.' digit+))(('e'|'E') ('-')? digit+)?)|
-              (digit+ ('e'|'E') ('-')? digit+)|(digit+ '.' digit+ 'E' ('-')? digit+);
+token CDouble (((digit+ '.' digit+)|(digit+ '.')|('.' digit+))(('e'|'E')('-')? digit+)?
+                                             )|((digit+ ('e'|'E')('-')? digit+));
 
 token CFloat (((digit+ '.' digit+)|(digit+ '.')|('.' digit+))(('e'|'E')('-')? digit+)?
                                ('f'|'F'))|((digit+ ('e'|'E')('-')? digit+)('f'|'F'));
@@ -354,7 +354,7 @@ Econst.      Exp17 ::= Constant;
 Estring.     Exp17 ::= String;
 Enondet.     Exp17 ::= "_";
 
-Efloat.        Constant ::= Double;
+Einf.          Constant ::= "INFINITY";
 Echar.         Constant ::= Char;
 Eunsigned.     Constant ::= Unsigned;
 Elong.         Constant ::= Long;
@@ -367,13 +367,10 @@ Eoctal.        Constant ::= Octal;
 Eoctalunsign.  Constant ::= OctalUnsigned;
 Eoctallong.    Constant ::= OctalLong;
 Eoctalunslong. Constant ::= OctalUnsLong;
-Ecdouble.      Constant ::= CDouble;
 Ecfloat.       Constant ::= CFloat;
+Ecdouble.      Constant ::= CDouble;
 Eclongdouble.  Constant ::= CLongDouble;
-Eint.          Constant ::= UnboundedInteger;  
-
--- internal Elonger. Constant ::= Integer;
--- internal Edouble. Constant ::= Double;
+Eint.          Constant ::= UnboundedInteger;
 
 Especial. Constant_expression ::= Exp3;
 

regression-tests/double/Answers

@@ -0,0 +1,42 @@
+
+add_1.c
+SAFE
+
+add_2.c
+UNSAFE
+
+add_3.c
+UNSAFE
+
+div_1.c
+SAFE
+
+div_2.c
+UNSAFE
+
+div_3.c
+SAFE
+
+init_1.c
+SAFE
+
+init_2.c
+SAFE
+
+mul_1.c
+SAFE
+
+mul_2.c
+UNSAFE
+
+loop_1.c
+SAFE
+
+loop_2.c
+UNSAFE
+
+sub_1.c
+SAFE
+
+sub_2.c
+UNSAFE

regression-tests/double/add_1.c

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

regression-tests/double/add_2.c

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

regression-tests/double/add_3.c

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

regression-tests/double/div_1.c

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

regression-tests/double/div_2.c

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

regression-tests/double/div_3.c

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

regression-tests/double/init_1.c

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

regression-tests/double/init_2.c

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

regression-tests/double/init_3.c

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

regression-tests/double/int_plus_float.c

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

regression-tests/double/leq_1.c

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

regression-tests/double/loop_1.c

@@ -0,0 +1,12 @@
+//SAFE
+void main(void) {
+  int i = 0;
+  double x = 0.5;
+  double y = x;
+  while (x < 3000.0) {
+    x = x*2.0;
+    y = x;
+    ++i;
+  }
+  assert(x==y);
+}

regression-tests/double/loop_2.c

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

regression-tests/double/mul_1.c

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

regression-tests/double/mul_2.c

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

regression-tests/double/nan.c

@@ -0,0 +1,8 @@
+//UNSAFE IF NAN IS INCLUDED OTHERWISE SAFE
+int main()
+{
+  double x = _;
+
+  assert(x==x);
+  return 0;
+}

regression-tests/double/nan_create.c

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

regression-tests/double/nan_range.c

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

regression-tests/double/nondet_1.c

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

regression-tests/double/nondet_2.c

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

regression-tests/double/runtests

@@ -0,0 +1,25 @@
+#!/bin/sh
+
+LAZABS=../../tri
+
+TESTS="add_1.c \
+       add_2.c \
+       add_3.c \
+       div_1.c \
+       div_2.c \
+       div_3.c \
+       init_1.c \
+       init_2.c \
+       mul_1.c \
+       mul_2.c \
+       loop_1.c \
+       loop_2.c \
+       sub_1.c \
+       sub_2.c "
+
+for name in $TESTS; do
+    echo
+    echo $name
+    $LAZABS "$@" $name 2>&1 | grep -v 'at '
+done
+

regression-tests/double/sub_1.c

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

regression-tests/double/sub_2.c

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

regression-tests/float/Answers

@@ -0,0 +1,39 @@
+
+add_1.c
+SAFE
+
+add_2.c
+SAFE
+
+add_3.c
+UNSAFE
+
+div_1.c
+SAFE
+
+div_2.c
+SAFE
+
+init_1.c
+SAFE
+
+init_2.c
+SAFE
+
+loop_1.c
+SAFE
+
+loop_2.c
+UNSAFE
+
+mul_1.c
+SAFE
+
+mul_2.c
+UNSAFE
+
+sub_1.c
+SAFE
+
+sub_2.c
+UNSAFE

regression-tests/float/add_1.c

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

regression-tests/float/add_2.c

@@ -0,0 +1,6 @@
+int main() {
+  float a = 3.0f;
+  float b = 0.5f;
+  assert(a+b == 3.5f);
+  return 0;
+}

regression-tests/float/add_3.c

@@ -0,0 +1,5 @@
+int main() {
+  float a = 2.0f;
+  float b = a + 0.5f;
+  assert(a + 0.4f == b);
+}