Commit bec4f317 authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

Finished script to launch frama-c

parent e3ada618
#!/bin/bash
# Temporary folder
TMP_FOLDER=".tmp_wp_analysis"
TMP_FOLDER=".tmp_frama_c_analysis"
mkdir -p $TMP_FOLDER
# Temporary file for frama-c result
TMP_FILE_RES="$TMP_FOLDER/tmp_wp_analysis.txt "
TMP_FILE_RES="$TMP_FOLDER/tmp_frama_c_analysis.txt "
# 2 temporary file to compute the list of functions to analyse
TMP1="$TMP_FOLDER/tmp_header_functions.txt"
......@@ -27,6 +27,9 @@ 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
RTE="-rte -no-warn-left-shift-negative"
# To stop de script with ctrl+C
STOP_FC=0
#Variables for pprz
INCLUDE="-I../include"
DEFINE="-DFRAMA_C_ANALYSIS"
......@@ -68,16 +71,23 @@ do
for FUNCTION in $FUNCTIONS
do
# Reset to 0 and set to 1 after frama-c command
# to detect ctrl+c
STOP_FC=0
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
$FRAMAC $RTE $EVA $FUNCTION $WP $FUNCTION $WP_ARGS $FILE $FLAGS > /tmp/wp_analysis.txt 2>> /tmp/wp_analysis_error.txt || break
STOP_FC=1
echo -n -e "\\r\033[2K"
./wp-analysis.py $TMP_FILE_RES $FILE $FUNCTION $TMP_RES_GOALS
./output-frama-c-analysis.py $TMP_FILE_RES $FILE $FUNCTION $TMP_RES_GOALS
done
if [ $STOP_FC -eq 0 ]; then
echo -e "\nFrama-c analysis stopped"
break
fi
echo -n "WP analysis of $FILE : "
cat $TMP_RES_GOALS
done
rm -rf $TMP_FOLDER
rm -rf $TMP_FOLDER
\ No newline at end of file
......@@ -1239,6 +1239,32 @@ static inline bool int32_vect_find(const int32_t *a, const int32_t s, int *loc,
//
//
/*
lemma square_sqrt:
\forall int a, b, n;
n > 0
&& -\sqrt(INT_MAX/n) <= a <= \sqrt(INT_MAX/n)
&& -\sqrt(INT_MAX/n) <= b <= \sqrt(INT_MAX/n)
==> -\sqrt(INT_MAX/n)*\sqrt(INT_MAX/n) <= a * b <= \sqrt(INT_MAX/n) * \sqrt(INT_MAX/n);
*/
/*
lemma square_sqrt_1:
\forall int a, b, n;
n > 0
&& -\sqrt(INT_MAX/n) <= a <= \sqrt(INT_MAX/n)
&& -\sqrt(INT_MAX/n) <= b <= \sqrt(INT_MAX/n)
==> -INT_MAX/n <= a * b <= INT_MAX/n;
*/
/*
lemma square_sqrt_2:
\forall int a, b, n;
n > 0
==> \sqrt(INT_MAX/n) * \sqrt(INT_MAX/n) == INT_MAX/n;
*/
/** o = a * b
*
* a: [m x n]
......@@ -1247,8 +1273,12 @@ static inline bool int32_vect_find(const int32_t *a, const int32_t s, int *loc,
*/
/*@
requires valid_int_mat(o, m, l);
requires rvalid_int_mat(a, m, n);
requires rvalid_int_mat(b, n, l);
requires rvalid_int_mat(a, m, n, (int) \sqrt(INT_MAX/n));
requires rvalid_int_mat(b, n, l, (int) \sqrt(INT_MAX/n));
requires \separated(&(o[0..m-1][0..l-1]), &(a[0..m-1][0..n-1]), &(b[0..n-1][0..l-1]));
requires l > 0;
requires m > 0;
requires n > 0;
assigns o[0..m-1][0..l-1];
*/
static inline void int32_mat_mul(int32_t **o, int32_t **a, int32_t **b, int m, int n, int l)
......@@ -1256,12 +1286,16 @@ static inline void int32_mat_mul(int32_t **o, int32_t **a, int32_t **b, int m, i
int i, j, k;
/*@
loop invariant 0 <= i <= m;
loop invariant rvalid_int_mat(a, m, n, (int) \sqrt(INT_MAX/n));
loop invariant rvalid_int_mat(b, n, l, (int) \sqrt(INT_MAX/n));
loop assigns o[0..m-1][0..l-1], i, j, k;
loop variant m - i;
*/
for (i = 0; i < m; i++) {
/*@
loop invariant 0 <= j <= l;
loop invariant rvalid_int_mat(a, m, n, (int) \sqrt(INT_MAX/n));
loop invariant rvalid_int_mat(b, n, l, (int) \sqrt(INT_MAX/n));
loop assigns o[i][0..l-1], j, k;
loop variant l - j;
*/
......@@ -1269,11 +1303,22 @@ static inline void int32_mat_mul(int32_t **o, int32_t **a, int32_t **b, int m, i
o[i][j] = 0;
/*@
loop invariant 0 <= k <= n;
loop invariant rvalid_int_mat(a, m, n, (int) \sqrt(INT_MAX/n));
loop invariant rvalid_int_mat(b, n, l, (int) \sqrt(INT_MAX/n));
loop invariant -k * INT_MAX / n <= o[i][j];
loop invariant o[i][j] <= k * INT_MAX / n;
loop assigns o[i][j], k;
loop variant n - k;
*/
for (k = 0; k < n; k++) {
//@ assert rvalid_int_mat(a, m, n, (int) \sqrt(INT_MAX/n));
//@ assert rvalid_int_mat(b, n, l, (int) \sqrt(INT_MAX/n));
//@ assert (int) -\sqrt(INT_MAX/n) <= a[i][k] <= \sqrt(INT_MAX/n);
//@ assert (int) -\sqrt(INT_MAX/n) <= b[k][j] <= \sqrt(INT_MAX/n);
//@assert -INT_MAX/n <= a[i][k] * b[k][j] <= INT_MAX/n;
o[i][j] += a[i][k] * b[k][j];
//@ assert rvalid_int_mat(a, m, n, (int) \sqrt(INT_MAX/n));
//@ assert rvalid_int_mat(b, n, l, (int) \sqrt(INT_MAX/n));
}
}
}
......
......@@ -223,9 +223,9 @@ extern "C" {
/*@
predicate mat_int_bound(int **a, int m, int n, integer bound) =
\forall int i;
0 <= i < n
==> vect_int_bound(a[i], n, bound);
\forall int i, j;
0 <= i < m && 0 <= j < n
==> -bound <= a[i][j] <= bound;
*/
/*@
......
......@@ -2,11 +2,6 @@
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):
"""
Read the output file of the WP result
......@@ -32,23 +27,29 @@ def get_result_from_file(file):
f.close()
proved_goals, nb_goals = get_result_from_file(output_file)
if __name__ == '__main__':
output_file = sys.argv[1]
analysed_file = sys.argv[2]
function_name = sys.argv[3]
res_file = sys.argv[4]
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))
if (proved_goals != nb_goals):
print("Function {} in {} file not proved ({}/{})".format(function_name, analysed_file, proved_goals, nb_goals))
# Get previous result
f = open(res_file, "r")
# Get previous result
f = open(res_file, "r")
values = f.readline().split(" ")
values = f.readline().split(" ")
assert(values[1] == "/")
proved_goals += int(values[0])
nb_goals += int(values[2])
assert(values[1] == "/")
proved_goals += int(values[0])
nb_goals += int(values[2])
f.close()
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
# Write new result
f = open(res_file, "w")
f.write("{} / {}\n".format(proved_goals, nb_goals))
f.close()
\ No newline at end of file
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