Adding initial script and properties

.gitignore

@@ -194,3 +194,6 @@ tests/results/*
 
 # K-develop
 *.kate-swp
+
+# Frama-C
+**/.frama-c
\ No newline at end of file

.vscode/c_cpp_properties.json

@@ -9,7 +9,8 @@
                 "limitSymbolsToIncludedHeaders": true
             },
             "includePath": [
-                "${workspaceFolder}"
+                "${workspaceFolder}",
+                "${workspaceFolder}/sw/include"
             ],
             "defines": [],
             "compilerPath": "/usr/bin/arm-none-eabi-gcc",

sw/airborne/math/pprz_algebra_double.c

@@ -26,18 +26,88 @@
 
 #include "pprz_algebra_double.h"
 
+/*@
+  predicate finite_DoubleEuler(struct DoubleEulers *e) =
+   \is_finite(e->phi)
+   && \is_finite(e->theta)
+   && \is_finite(e->psi);
+*/
+
+/*@
+  predicate rvalid_DoubleEuler(struct DoubleEulers *e) =
+   \valid_read(e) && finite_DoubleEuler(e);
+*/
+
+/*@
+  predicate valid_DoubleEuler(struct DoubleEulers *e) =
+    \valid(e) && finite_DoubleEuler(e);
+*/
+
+/*@
+  predicate in_interval(double x, real x1, real x2) =
+    \le_double((double) x1, x) && \le_double(x, (double) x2);
+*/
+
+/*
+  lemma mul_double_bounded:
+    \forall double x, y ;
+        in_interval(x, -1.0, 1.0) && in_interval(y, -1.0, 1.0)
+          ==>  in_interval(\mul_double(x, y), -1.0, 1.0);
+*/
+
+/*@
+  lemma mul_double_bounded_full:
+    \forall double x, y ;
+        \is_finite(x) && \is_finite(y) && \le_double((double) -1.0, x) && \le_double(x, (double) 1.0) 
+    && \le_double((double) -1.0, y) && \le_double(y, (double) 1.0) 
+          ==>  \le_double((double) -1.0, \mul_double(x, y)) && \le_double(\mul_double(x, y), (double) 1.0) ;
+*/
+
+/*@
+  lemma sub_double_finite:
+    \forall double x, y ;
+    in_interval(x, -1.0, 1.0) && in_interval(y, -1.0, 1.0) 
+          ==> \is_finite(\sub_double(x, y));
+*/
+
+/*@
+  lemma add_double_finite:
+    \forall double x, y ;
+    in_interval(x, -1.0, 1.0) && in_interval(y, -1.0, 1.0) 
+          ==> \is_finite(\add_double(x, y));
+*/
+
+/*@
+ lemma bounded_is_finite:
+  \forall double x;
+    in_interval(x, -1.0, 1.0) ==> \is_finite(x);
+*/
+
+/*@
+  requires \valid(rm);
+  requires rvalid_DoubleEuler(e);
+  assigns *rm;
+*/
 void double_rmat_of_eulers_321(struct DoubleRMat *rm, struct DoubleEulers *e)
 {
   const double sphi   = sin(e->phi);
+  /*@ assert bound: -1 <= sphi <= 1; */
   const double cphi   = cos(e->phi);
+  /*@ assert bound: -1 <= cphi <= 1; */
   const double stheta = sin(e->theta);
+  /*@ assert bound: -1 <= stheta <= 1; */
   const double ctheta = cos(e->theta);
+  /*@ assert bound: -1 <= ctheta <= 1; */
   const double spsi   = sin(e->psi);
+  /*@ assert bound: -1 <= spsi <= 1; */
   const double cpsi   = cos(e->psi);
+  /*@ assert bound: -1 <= cpsi <= 1; */
 
   RMAT_ELMT(*rm, 0, 0) = ctheta * cpsi;
   RMAT_ELMT(*rm, 0, 1) = ctheta * spsi;
   RMAT_ELMT(*rm, 0, 2) = -stheta;
+  /*@ assert -1 <= cphi <= 1; */
+  /*@ assert -1 <= spsi <= 1; */
   RMAT_ELMT(*rm, 1, 0) = sphi * stheta * cpsi - cphi * spsi;
   RMAT_ELMT(*rm, 1, 1) = sphi * stheta * spsi + cphi * cpsi;
   RMAT_ELMT(*rm, 1, 2) = sphi * ctheta;

sw/airborne/math/pprz_algebra_float.h

@@ -736,22 +736,22 @@ static inline void float_mat_mul(float **o, float **a, float **b, int m, int n,
  * of the input matrices when this function is used, which is useful for consecutive multiplications
  * (e.g. when doing matrix exponentiation), at the cost of some copy overhead.
  */
-static inline void float_mat_mul_copy(float **o, float **a, float **b, int m, int n, int l)
-{
-  float temp[m][l];
-  int i, j, k;
-  for (i = 0; i < m; i++) {
-    for (j = 0; j < l; j++) {
-      temp[i][j] = 0.;
-      for (k = 0; k < n; k++) {
-        temp[i][j] += a[i][k] * b[k][j];
-      }
-    }
-  }
-  MAKE_MATRIX_PTR(_o,  o,  m);
-  MAKE_MATRIX_PTR(_temp,  temp,  m);
-  float_mat_copy(_o, _temp, m, l);
-}
+// static inline void float_mat_mul_copy(float **o, float **a, float **b, int m, int n, int l)
+// {
+//   float temp[m][l];
+//   int i, j, k;
+//   for (i = 0; i < m; i++) {
+//     for (j = 0; j < l; j++) {
+//       temp[i][j] = 0.;
+//       for (k = 0; k < n; k++) {
+//         temp[i][j] += a[i][k] * b[k][j];
+//       }
+//     }
+//   }
+//   MAKE_MATRIX_PTR(_o,  o,  m);
+//   MAKE_MATRIX_PTR(_temp,  temp,  m);
+//   float_mat_copy(_o, _temp, m, l);
+// }
 
 
 /** o = a * b

sw/airborne/wp-analysis.sh

+#!/bin/bash
+
+# FILES="math/pprz_algebra_int.c \
+#        math/pprz_algebra_float.c \
+#        math/pprz_algebra_double.c"
+
+# for FILE in $FILES
+# do
+#     frama-c -wp -rte $FILE -cpp-extra-args=-I../include -kernel-msg-key pp
+# done
+
+
+# Double
+GUI=false
+POSITIONAL=()
+while [[ $# -gt 0 ]]
+do
+key="$1"
+
+case $key in
+    -g | --gui)
+    GUI=true
+    shift
+    ;;
+    # -e|--extension)
+    # EXTENSION="$2"
+    # shift # past argument
+    # shift # past value
+    # ;;
+    # -s|--searchpath)
+    # SEARCHPATH="$2"
+    # shift # past argument
+    # shift # past value
+    # ;;
+    # -l|--lib)
+    # LIBPATH="$2"
+    # shift # past argument
+    # shift # past value
+    # ;;
+    # --default)
+    # DEFAULT=YES
+    # shift # past argument
+    # ;;
+    *)    # unknown option
+    POSITIONAL+=("$1") # save it in an array for later
+    shift # past argument
+    ;;
+esac
+done
+set -- "${POSITIONAL[@]}" # restore positional parameters
+
+FUNCTIONS="double_rmat_of_eulers_321"
+
+for FUNCTION in $FUNCTIONS
+do
+    if [[ "$GUI" = true ]]; then 
+        CMD="frama-c-gui"
+    else
+        CMD="frama-c"
+    fi
+    ARGS="-wp-fct $FUNCTION -wp-prover alt-ergo,cvc4-ce,z3-ce,native:coq -rte math/pprz_algebra_double.c -cpp-extra-args=-I../include -kernel-msg-key pp"
+
+    echo $CMD $ARGS
+    $CMD $ARGS
+done