Commit 98f69811 authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

Update wp-analysis script

parent ed5a1338
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 0.05 }
{ "prover": "Alt-Ergo:2.3.3", "verdict": "valid", "time": 0.0079,
"steps": 8 }
......@@ -77,15 +77,6 @@ float float_rmat_norm(struct FloatRMat *rm)
*/
void float_rmat_comp(struct FloatRMat *m_a2c, struct FloatRMat *m_a2b, struct FloatRMat *m_b2c)
{
/*@
assert valid_matric: \valid_read(m_a2c->m + (0..8));
*/
/*@
assert valid_matric: \valid_read(m_a2b->m + (0..8));
*/
/*@
assert valid_matric: \valid_read(m_b2c->m + (0..8));
*/
m_a2c->m[0] = m_b2c->m[0] * m_a2b->m[0] + m_b2c->m[1] * m_a2b->m[3] + m_b2c->m[2] * m_a2b->m[6];
m_a2c->m[1] = m_b2c->m[0] * m_a2b->m[1] + m_b2c->m[1] * m_a2b->m[4] + m_b2c->m[2] * m_a2b->m[7];
m_a2c->m[2] = m_b2c->m[0] * m_a2b->m[2] + m_b2c->m[1] * m_a2b->m[5] + m_b2c->m[2] * m_a2b->m[8];
......@@ -297,17 +288,6 @@ static inline float renorm_factor(float n)
float float_rmat_reorthogonalize(struct FloatRMat *rm)
{
/*@
assert valid_matric: \valid(&rm->m[0])
&& \valid(&rm->m[1])
&& \valid(&rm->m[2])
&& \valid(&rm->m[3])
&& \valid(&rm->m[4])
&& \valid(&rm->m[5])
&& \valid(&rm->m[6])
&& \valid(&rm->m[7])
&& \valid(&rm->m[8]);
*/
const struct FloatVect3 r0 = {RMAT_ELMT(*rm, 0, 0),
RMAT_ELMT(*rm, 0, 1),
RMAT_ELMT(*rm, 0, 2)
......@@ -387,12 +367,6 @@ void float_quat_inv_comp_norm_shortest(struct FloatQuat *b2c, struct FloatQuat *
void float_quat_differential(struct FloatQuat *q_out, struct FloatRates *w, float dt)
{
/*@
assert valid_subterms: \valid(&q_out->qi)
&& \valid(&q_out->qx)
&& \valid(&q_out->qy)
&& \valid(&q_out->qz);
*/
const float v_norm = sqrtf(w->p * w->p + w->q * w->q + w->r * w->r);
const float c2 = cos(dt * v_norm / 2.0);
const float s2 = sin(dt * v_norm / 2.0);
......@@ -428,18 +402,6 @@ void float_quat_integrate_fi(struct FloatQuat *q, struct FloatRates *omega, floa
/** in place quaternion integration with constant rotational velocity */
void float_quat_integrate(struct FloatQuat *q, struct FloatRates *omega, float dt)
{
/*@
assert valid_subterms: \valid(&q->qi)
&& \valid(&q->qx)
&& \valid(&q->qy)
&& \valid(&q->qz);
*/
/*@
assert valid_subterms: \valid_read(&q->qi)
&& \valid_read(&q->qx)
&& \valid_read(&q->qy)
&& \valid_read(&q->qz);
*/
const float no = FLOAT_RATES_NORM(*omega);
if (no > FLT_MIN) {
const float a = 0.5 * no * dt;
......@@ -600,12 +562,6 @@ void float_quat_of_axis_angle(struct FloatQuat *q, const struct FloatVect3 *uv,
void float_quat_of_orientation_vect(struct FloatQuat *q, const struct FloatVect3 *ov)
{
/*@
assert valid_subterms: \valid(&q->qi)
&& \valid(&q->qx)
&& \valid(&q->qy)
&& \valid(&q->qz);
*/
const float ov_norm = sqrtf(ov->x * ov->x + ov->y * ov->y + ov->z * ov->z);
if (ov_norm < 1e-8) {
q->qi = 1;
......@@ -623,23 +579,6 @@ void float_quat_of_orientation_vect(struct FloatQuat *q, const struct FloatVect3
void float_quat_of_rmat(struct FloatQuat *q, struct FloatRMat *rm)
{
/*@
assert valid_subterms: \valid(&q->qi)
&& \valid(&q->qx)
&& \valid(&q->qy)
&& \valid(&q->qz);
*/
/*@
assert valid_matric: \valid_read(&rm->m[0])
&& \valid_read(&rm->m[1])
&& \valid_read(&rm->m[2])
&& \valid_read(&rm->m[3])
&& \valid_read(&rm->m[4])
&& \valid_read(&rm->m[5])
&& \valid_read(&rm->m[6])
&& \valid_read(&rm->m[7])
&& \valid_read(&rm->m[8]);
*/
const float tr = RMAT_TRACE(*rm);
if (tr > 0) {
const float two_qi = sqrtf(1. + tr);
......@@ -1078,11 +1017,6 @@ float float_mat_norm_li(float **a, int m, int n)
/* Scale a 3D vector to within a 2D bound */
void vect_bound_in_2d(struct FloatVect3 *vect3, float bound) {
/*@
assert valid_subterms: \valid(&vect3->x)
&& \valid(&vect3->y)
&& \valid(&vect3->z);
*/
float norm = FLOAT_VECT2_NORM(*vect3);
if(norm>bound) {
float scale = bound/norm;
......@@ -1093,11 +1027,6 @@ void vect_bound_in_2d(struct FloatVect3 *vect3, float bound) {
/* Scale a 3D vector to a certain length in 2D */
void vect_scale(struct FloatVect3 *vect3, float norm_des) {
/*@
assert valid_subterms: \valid(&vect3->x)
&& \valid(&vect3->y)
&& \valid(&vect3->z);
*/
float norm = FLOAT_VECT2_NORM(*vect3);
if(norm>0.1) {
float scale = norm_des/norm;
......
......@@ -1182,8 +1182,11 @@ static inline float float_vect_dot_product(const float *a, const float *b, const
for (__i = 0; __i < _rows; __i++) { _ptr[__i] = &_mat[__i][0]; } \
}
/* Ignoring functions that are not supported by frama-c */
#ifndef FRAMA_C_ANALYSIS
extern void float_mat_invert(float **o, float **mat, int n);
extern void float_mat_exp(float **a, float **o, int n);
#endif
/*@
requires rvalid_float_mat(o, m, n);
assigns \nothing;
......
......@@ -5,6 +5,7 @@ import sys
output_file = sys.argv[1]
analysed_file = sys.argv[2]
function_name = sys.argv[3]
res_file = sys.argv[4]
def get_result_from_file(file):
"""
......@@ -27,10 +28,27 @@ def get_result_from_file(file):
if tab_el[i] == "/":
return int(tab_el[i-1]), int(tab_el[i+1])
raise ValueError("Number of proved goals not found ! \n Verify that the file name is correct and that frama-c has not changed his output format for the result.")
raise ValueError("Number of proved goals not found ({}, {})! \n Verify that the file name is correct and that frama-c has not changed his output format for the result.".format(analysed_file, function_name))
f.close()
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))
\ No newline at end of file
print("Function {} in {} file not proved ({}/{})".format(function_name, analysed_file, proved_goals, nb_goals))
# Get previous result
f = open(res_file, "r")
values = f.readline().split(" ")
assert(values[1] == "/")
proved_goals += int(values[0])
nb_goals += int(values[2])
f.close()
# Write new result
f = open(res_file, "w")
f.write("{} / {}\n".format(proved_goals, nb_goals))
f.close()
\ No newline at end of file
#!/bin/bash
# Temporary folder
TMP_FOLDER=".tmp_wp_analysis"
mkdir -p $TMP_FOLDER
# Temporary file for frama-c result
TMP_FILE_RES="$TMP_FOLDER/tmp_wp_analysis.txt "
# 2 temporary file to compute the list of functions to analyse
TMP1="$TMP_FOLDER/tmp_header_functions.txt"
TMP2="$TMP_FOLDER/tmp_preprocess_functions.txt"
# Temporary file for preprocessed header file
TMP_HEADER="$TMP_FOLDER/tmp_preprocess.h"
# Temporary res of all result
TMP_RES_GOALS="$TMP_FOLDER/tmp_res_goals.txt"
# All Frama-c variables
#FRAMAC_PREFIXE=""
FRAMAC_PREFIX="/opt/frama-c/bin/"
TMP_FILE="tmp_wp_analysis.txt "
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
WP_ARGS="-wp-cache update -wp-model real+Cast -wp-prover alt-ergo,cvc4-strings-ce,tip -wp-log r:"$TMP_FILE_RES
RTE="-rte -no-warn-left-shift-negative"
FLAGS="-cpp-extra-args=-I../include -cpp-extra-args=-DFRAMA_C_ANALYSIS"
#Variables for pprz
INCLUDE="-I../include"
DEFINE="-DFRAMA_C_ANALYSIS"
FLAGS="-cpp-extra-args=$INCLUDE -cpp-extra-args=$DEFINE"
# Files currently supported
#FILES="math/pprz_algebra_double.c \
# math/pprz_algebra_float.c \
# math/pprz_algebra_int.c"
FILES="math/pprz_algebra_double.c \
math/pprz_algebra_float.c \
math/pprz_algebra_int.c"
FILES="math/pprz_algebra_int.c"
#FILES="math/pprz_algebra_int.c"
# Get all the functions name in $1 file.
# The result is written in $2 file.
get_function_names () {
ctags -x --declaration --no-members $1 | grep -v -e "#define" -e "struct" | cut -f -1 -d " " > $2
}
for FILE in $FILES
do
# Reset nb of goals
echo "0 / 0" > $TMP_RES_GOALS
# Get header file name
HEADER=$(echo $FILE | sed 's/.$//')"h"
FUNCTIONS=$(ctags -x --declaration --no-members $HEADER | grep -v -e "#define" -e "struct" | cut -f -1 -d " ")
# Get all functions declare in header file
get_function_names $HEADER $TMP1
# Pre-process the header and get all the function name
gcc -E $INCLUDE -I. $DEFINE $HEADER > $TMP_HEADER
get_function_names $TMP_HEADER $TMP2
# Get all the functions by removing functions suppressed by
# the preprocessing. The Goals is to ignore function that can
# not be verified by frama-c.
FUNCTIONS=$(grep -Fxf $TMP1 $TMP2)
for FUNCTION in $FUNCTIONS
do
echo -n "Analysing $FILE:$FUNCTION... "
echo -n "Analysing $FILE:$FUNCTION..."
$FRAMAC $RTE $EVA $FUNCTION $WP $FUNCTION $WP_ARGS $FILE $FLAGS > /tmp/wp_analysis.txt 2>> /tmp/wp_analysis_error.txt
echo -n -e "\\r\033[1K"
./wp-analysis.py $TMP_FILE $FILE $FUNCTION
echo -n -e "\\r\033[2K"
./wp-analysis.py $TMP_FILE_RES $FILE $FUNCTION $TMP_RES_GOALS
done
echo -n "WP analysis of $FILE : "
cat $TMP_RES_GOALS
done
rm -f $TMP_FILE
rm -rf $TMP_FOLDER
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment