Verification of the conversion quat to rmat

.gitignore

@@ -196,8 +196,8 @@ tests/results/*
 *.kate-swp
 
 # Frama-C
-**/.frama-c
 !sw/airborne/.frama-c/wp/script
 **/.lia.cache
 **/tmp_wp_analysis.txt
-sw/airborne/.frama-c/wp/cache
\ No newline at end of file
+sw/airborne/.frama-c/wp/cache
+sw/airborne/.frama-c/frama_c_journal.ml

.vscode/settings.json

@@ -8,4 +8,9 @@
     "[python]": {
         "editor.tabSize": 4,
     },
+    "files.associations": {
+        "array": "cpp",
+        "string_view": "cpp",
+        "type_traits": "cpp"
+    },
 }
\ No newline at end of file

sw/airborne/frama-c-analysis.sh

@@ -24,7 +24,7 @@ FRAMAC=$FRAMAC_PREFIX"frama-c"
 FRAMACGUI=$FRAMAC_PREFIX"frama-c-gui"
 EVA="-eva -lib-entry -main"
 WP="-wp-fct"
-WP_ARGS="-wp-cache update -wp-model real+Cast -wp-prover alt-ergo,cvc4-strings-ce,tip -wp-log r:"$TMP_FILE_RES
+WP_ARGS="-wp-cache update -wp-model real+Cast -wp-prover alt-ergo,cvc4-strings-ce,z3,z3-ce,z3-nobv,tip -wp-log r:"$TMP_FILE_RES
 RTE="-rte -no-warn-left-shift-negative"
 
 # To stop de script with ctrl+C

sw/airborne/math/pprz_algebra_float.c

@@ -235,6 +235,7 @@ void float_rmat_of_eulers_312(struct FloatRMat *rm, struct FloatEulers *e)
 /* C n->b rotation matrix */
 void float_rmat_of_quat(struct FloatRMat *rm, struct FloatQuat *q)
 {
+#ifndef FRAMA_C_ANALYSIS
   const float _a = M_SQRT2 * q->qi;
   const float _b = M_SQRT2 * q->qx;
   const float _c = M_SQRT2 * q->qy;
@@ -255,6 +256,32 @@ void float_rmat_of_quat(struct FloatRMat *rm, struct FloatQuat *q)
   RMAT_ELMT(*rm, 2, 0) = bd + ac;
   RMAT_ELMT(*rm, 2, 1) = cd - ab;
   RMAT_ELMT(*rm, 2, 2) = a2_1 + _d * _d;
+#else 
+  const float _a = q->qi;
+  const float _b = q->qx;
+  const float _c = q->qy;
+  const float _d = q->qz;
+  const float a2_1 = 2 * _a * _a - 1;
+  const float ab = 2 * _a * _b;
+  const float ac = 2 * _a * _c;
+  const float ad = 2 * _a * _d;
+  const float bc = 2 * _b * _c;
+  const float bd = 2 * _b * _d;
+  const float cd = 2 * _c * _d;
+  RMAT_ELMT(*rm, 0, 0) = a2_1 + 2 * _b * _b;
+  RMAT_ELMT(*rm, 0, 1) = bc + ad;
+  RMAT_ELMT(*rm, 0, 2) = bd - ac;
+  RMAT_ELMT(*rm, 1, 0) = bc - ad;
+  RMAT_ELMT(*rm, 1, 1) = a2_1 + 2 * _c * _c;
+  RMAT_ELMT(*rm, 1, 2) = cd + ab;
+  RMAT_ELMT(*rm, 2, 0) = bd + ac;
+  RMAT_ELMT(*rm, 2, 1) = cd - ab;
+  RMAT_ELMT(*rm, 2, 2) = a2_1 + 2 * _d * _d;
+  //@assert \at(q->qi, Pre) == q->qi;
+  //@assert \at(q->qx, Pre) == q->qx;
+  //@assert \at(q->qy, Pre) == q->qy;
+  //@assert \at(q->qz, Pre) == q->qz;
+#endif
 }
 
 /** in place first order integration of a rotation matrix */
@@ -619,6 +646,15 @@ void float_quat_of_rmat(struct FloatQuat *q, struct FloatRMat *rm)
       /*printf("m22 largest\n");*/
     }
   }
+  //@ assert \at(rm->m[0], Pre) == rm->m[0];
+  //@ assert \at(rm->m[1], Pre) == rm->m[1];
+  //@ assert \at(rm->m[2], Pre) == rm->m[2];
+  //@ assert \at(rm->m[3], Pre) == rm->m[3];
+  //@ assert \at(rm->m[4], Pre) == rm->m[4];
+  //@ assert \at(rm->m[5], Pre) == rm->m[5];
+  //@ assert \at(rm->m[6], Pre) == rm->m[6];
+  //@ assert \at(rm->m[7], Pre) == rm->m[7];
+  //@ assert \at(rm->m[8], Pre) == rm->m[8];
 }
 
 

sw/airborne/math/pprz_algebra_float.h

@@ -242,6 +242,8 @@ struct FloatRates {
     while (_a < -M_PI) _a += (2.*M_PI);             \
   }
 
+#include "pprz_algebra_float_convert_rmat_frama_c.h"
+
 /*
  * Returns the real part of the log of v in base of n
  */
@@ -598,9 +600,14 @@ extern void float_rmat_of_eulers_312(struct FloatRMat *rm, struct FloatEulers *e
 /*@
   requires valid_FloatRMat(rm);
   requires rvalid_FloatQuat(q);
+  requires unary_quaterion(q);
+  requires \separated(rm, q);
+  ensures transpose(l_RMat_of_FloatRMat(rm)) ==  l_RMat_of_FloatQuat(q);
+  ensures rotation_matrix(l_RMat_of_FloatRMat(rm));
   assigns *rm;
 */
 extern void float_rmat_of_quat(struct FloatRMat *rm, struct FloatQuat *q);
+
 /** in place first order integration of a rotation matrix */
 /*@
   requires valid_FloatRMat(rm);
@@ -871,9 +878,13 @@ extern void float_quat_of_axis_angle(struct FloatQuat *q, const struct FloatVect
 extern void float_quat_of_orientation_vect(struct FloatQuat *q, const struct FloatVect3 *ov);
 
 /// Quaternion from rotation matrix.
-/*@
+/*
   requires valid_FloatQuat(q);
   requires rvalid_FloatRMat(rm);
+  requires rotation_matrix(l_RMat_of_FloatRMat(rm));
+  requires \separated(rm, q);
+  ensures unary_quaterion(q);
+  ensures transpose(l_RMat_of_FloatRMat(rm)) ==  l_RMat_of_FloatQuat(q);
   assigns *q;
 */
 extern void float_quat_of_rmat(struct FloatQuat *q, struct FloatRMat *rm);

sw/airborne/math/pprz_algebra_float_frama_c.h

-#ifndef PPRZ_ALGEBRA_FLOAT_FRAM_C_H
-#define PPRZ_ALGEBRA_FLOAT_FRAM_C_H
+#ifndef PPRZ_ALGEBRA_FLOAT_FRAMA_C_H
+#define PPRZ_ALGEBRA_FLOAT_FRAMA_C_H
 
 #ifdef __cplusplus
 extern "C" {

sw/airborne/output-frama-c-analysis.py

@@ -36,7 +36,7 @@ if __name__ == '__main__':
     proved_goals, nb_goals = get_result_from_file(output_file)
 
     if (proved_goals != nb_goals):
-        print("Function {} in {} file not proved ({}/{})".format(function_name, analysed_file, proved_goals, nb_goals))
+        print("\033[31;01m[File Not Proved]\033[00m Function {} in {} file is not proved ({}/{})".format(function_name, analysed_file, proved_goals, nb_goals))
 
     # Get previous result
     f = open(res_file, "r")