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

Adding -wp-check-memory-model option

parent 5c094437
......@@ -92,6 +92,7 @@ the _preconditions_ specified in the contract of the function.
usage of cast in the code. Finally, the `ref` option is used to enable optimization for reference parameters.
- `-wp-prover alt-ergo,cvc4-strings-ce,z3,z3-ce,z3-nobv,tip`:
adds the different provers needed to verify the goals.
' `-wp-check-memory-model`: Insert memory model hypotheses in the function contracts. Necessary as we use the `ref` memory model.
- `-cpp-extra-args=-I../include`: adds the include directory of
Paparazzi.
- `-cpp-extra-args=-DFRAMA_C_ANALYSIS`: defines a C constant in order
......
......@@ -56,54 +56,39 @@
"pattern": "L_l_FloatQuat_of_RMat_2_max_1_{RealRMat_s}" },
"children":
{ "Unfold 'L_l_FloatQuat_of_RMat_2_max_1_'":
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 14.7875,
"steps": 280210 },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "clause-goal",
"target": "let a_0 = (L_l_RMat_of_FloatRMat Mf32_0 rm_0) in\nlet r_0 =\n (\\sqrt\n (1+a_0.F9_RealRMat_s_a22-a_0.F9_RealRMat_s_a00-a_0.F9_RealRMat_s_a11)) in\nlet r_1 = (2*r_0) in\n(EqS10_RealQuat_s\n {\n F10_RealQuat_s_qi =\n (a_0.F9_RealRMat_s_a01-a_0.F9_RealRMat_s_a10) div r_1 ;\n F10_RealQuat_s_qx =\n (a_0.F9_RealRMat_s_a02+a_0.F9_RealRMat_s_a20) div r_1 ;\n F10_RealQuat_s_qy =\n (a_0.F9_RealRMat_s_a12+a_0.F9_RealRMat_s_a21) div r_1 ;\n F10_RealQuat_s_qz = 1/2*r_0\n }\n {\n F10_RealQuat_s_qi = Mf32_0[(shiftfield_F4_FloatQuat_qi q_0)] ;\n F10_RealQuat_s_qx = Mf32_0[(shiftfield_F4_FloatQuat_qx q_0)] ;\n F10_RealQuat_s_qy = Mf32_0[(shiftfield_F4_FloatQuat_qy q_0)] ;\n F10_RealQuat_s_qz = Mf32_0[(shiftfield_F4_FloatQuat_qz q_0)]\n })",
"pattern": "EqS10_RealQuat_s{RealQuat_s}{RealQuat_s}" },
"children":
{ "Unfold 'EqS10_RealQuat_s'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
[ { "header": "Split",
"tactic": "Wp.split",
"params": {},
"select":
{ "select": "inside-goal",
"occur": 0,
"target": "(L_l_RMat_of_FloatRMat Mf32_0 rm_0)",
"pattern": "L_l_RMat_of_FloatRMat$Mf32$rm" },
{ "select": "clause-step",
"at": 13,
"kind": "branch",
"target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\n0<\n(Mf32_23[(shift_float32 a_0 0)]+Mf32_23[(shift_float32 a_0 4)]+\n Mf32_23[(shift_float32 a_0 8)])",
"pattern": "<0+[][][]$Mf32shift_float32$Mf32" },
"children":
{ "Unfold 'L_l_RMat_of_FloatRMat'":
{ "Then":
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 0.2864,
"steps": 2972 } ],
"Else":
[ { "header": "Split",
"tactic": "Wp.split",
"params": {},
"select":
{ "select": "clause-goal",
"target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\nlet r_0 =\n (\\sqrt\n (1+Mf32_0[(shift_float32 a_0 8)]-Mf32_0[(shift_float32 a_0 0)]-\n Mf32_0[(shift_float32 a_0 4)])) in\nlet r_1 = (2*r_0) in\n(Mf32_0[(shiftfield_F4_FloatQuat_qz q_0)]=(1/2*r_0))\n/\\ (Mf32_0[(shiftfield_F4_FloatQuat_qi q_0)]=\n ((Mf32_0[(shift_float32 a_0 1)]-Mf32_0[(shift_float32 a_0 3)]) div r_1))\n/\\ (Mf32_0[(shiftfield_F4_FloatQuat_qx q_0)]=\n ((Mf32_0[(shift_float32 a_0 2)]+Mf32_0[(shift_float32 a_0 6)]) div r_1))\n/\\ (Mf32_0[(shiftfield_F4_FloatQuat_qy q_0)]=\n ((Mf32_0[(shift_float32 a_0 5)]+Mf32_0[(shift_float32 a_0 7)]) div r_1))",
"pattern": "&====[]*[]/[]/[]/$Mf32shiftfield_F4_FloatQuat_qz" },
{ "select": "clause-step",
"at": 15,
"kind": "branch",
"target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\nMf32_22[(shift_float32 a_0 4)]<Mf32_22[(shift_float32 a_0 0)]",
"pattern": "<[][]$Mf32shift_float32$Mf32shift_float32" },
"children":
{ "Goal 1/4":
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 4.0255,
"steps": 752 } ],
"Goal 2/4":
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 4.6182,
"steps": 779 } ],
"Goal 3/4":
{ "Then":
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 4.7327,
"steps": 778 } ],
"Goal 4/4":
"time": 3.2286,
"steps": 69882 } ],
"Else":
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 3.5847,
"steps": 778 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 3.8577,
"steps": 80726 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
......@@ -5,6 +5,9 @@
"children": { "Unfold 'P_rvalid_int_mat_3_'": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 7.63 },
{ "prover": "Alt-Ergo:2.4.0",
"verdict": "timeout",
"time": 20. },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
......@@ -40,4 +43,4 @@
{ "Unfold 'P_rvalid_int_mat_2_'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 2.6 } ] } } ] } } ] } } ] } } ]
"time": 1.91 } ] } } ] } } ] } } ] } } ]
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "let x_0 =\n ((Mint_0[(shiftfield_F11_Int32Quat_qi a2c_0)]*\n Mint_0[(shiftfield_F11_Int32Quat_qi b2c_0)])+\n (Mint_0[(shiftfield_F11_Int32Quat_qx a2c_0)]*\n Mint_0[(shiftfield_F11_Int32Quat_qx b2c_0)])+\n (Mint_0[(shiftfield_F11_Int32Quat_qy a2c_0)]*\n Mint_0[(shiftfield_F11_Int32Quat_qy b2c_0)])+\n (Mint_0[(shiftfield_F11_Int32Quat_qz a2c_0)]*\n Mint_0[(shiftfield_F11_Int32Quat_qz b2c_0)])) in\n(-759267327<=x_0) /\\ (x_0<=759267327)",
"pattern": "&<=<=-759267327++759267327******" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid", "time": 6.508,
"steps": 15554 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid", "time": 6.5846,
"steps": 15554 } ] } } ]
......@@ -31,7 +31,7 @@
{ "Unfold 'EqS12_RealVect3_s'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 0.0181,
"time": 0.0063,
"steps": 8 },
{ "header": "Split",
"tactic": "Wp.split",
......
......@@ -3,8 +3,8 @@
"target": "(to_sint32 (2147483647 div n_0))",
"pattern": "to_sint32/2147483647$n" },
"children": { "In-Range": [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "time": 0.0135,
"verdict": "valid", "time": 0.0173,
"steps": 100 } ],
"No-Overflow": [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "time": 0.019,
"verdict": "valid", "time": 0.0198,
"steps": 28 } ] } } ]
......@@ -3,7 +3,7 @@
"target": "(to_sint32 (2147483647 div n_0))",
"pattern": "to_sint32/2147483647$n" },
"children": { "In-Range": [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "time": 0.0152,
"verdict": "valid", "time": 0.0196,
"steps": 85 } ],
"No-Overflow": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 0.09 } ] } } ]
......@@ -63,4 +63,4 @@
{ "Unfold 'EqS13_RealRMat_s'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 0.98 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 0.59 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
......@@ -33,4 +33,4 @@
"No-Overflow":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 0.14 } ] } } ] } } ] } } ]
"time": 0.15 } ] } } ] } } ] } } ]
......@@ -193,5 +193,5 @@
{ "Unfold 'L_add_RealVect3'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 3.1478,
"time": 3.7663,
"steps": 142 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
......@@ -25,7 +25,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+ref -wp-prover alt-ergo,cvc4-strings-ce,z3,z3-ce,z3-nobv,coq,tip -wp-timeout 20 -wp-log r:"$TMP_FILE_RES
WP_ARGS="-wp-cache update -wp-model real+Cast+ref -wp-prover alt-ergo,cvc4-strings-ce,z3,z3-ce,z3-nobv,coq,tip -wp-check-memory-model -wp-timeout 20 -wp-log r:"$TMP_FILE_RES
RTE="-rte -no-warn-left-shift-negative"
# Enable somke tests
......
......@@ -125,6 +125,12 @@ struct FloatMat33 {
&& \is_finite(q->qz);
*/
#define finite_FLOATQUAT(q) \
\is_finite(q->qi) \
&& \is_finite(q->qx) \
&& \is_finite(q->qy) \
&& \is_finite(q->qz) \
/*@
predicate rvalid_FloatQuat(struct FloatQuat *q) =
\valid_read(q) && finite_FloatQuat(q);
......@@ -696,7 +702,8 @@ static inline float float_quat_norm(struct FloatQuat *q)
}
/*@
requires valid_FloatQuat(q);
requires \valid(q);
requires finite_FLOATQUAT(q);
assigns *q;
*/
static inline void float_quat_normalize(struct FloatQuat *q)
......@@ -721,7 +728,8 @@ static inline void float_quat_invert(struct FloatQuat *qo, struct FloatQuat *qi)
}
/*@
requires valid_FloatQuat(q);
requires \valid(q);
requires finite_FLOATQUAT(q);
assigns *q;
*/
static inline void float_quat_wrap_shortest(struct FloatQuat *q)
......@@ -733,7 +741,6 @@ static inline void float_quat_wrap_shortest(struct FloatQuat *q)
#define FLOAT_QUAT_EXTRACT(_vo, _qi) QUAT_EXTRACT_Q(_vo, _qi)
/** Composition (multiplication) of two quaternions.
* a2c = a2b comp b2c , aka a2c = a2b * b2c
*/
......@@ -756,8 +763,11 @@ extern void float_quat_comp(struct FloatQuat *a2c, struct FloatQuat *a2b, struct
*/
/*@
requires \valid(a2b);
requires rvalid_FloatQuat(a2c);
requires rvalid_FloatQuat(b2c);
requires \valid_read(a2c);
requires finite_FLOATQUAT(a2c);
requires \valid_read(b2c);
requires finite_FLOATQUAT(b2c);
requires \separated(a2b, a2c) && \separated(a2b, b2c);
assigns *a2b;
*/
extern void float_quat_comp_inv(struct FloatQuat *a2b, struct FloatQuat *a2c, struct FloatQuat *b2c);
......@@ -767,8 +777,11 @@ extern void float_quat_comp_inv(struct FloatQuat *a2b, struct FloatQuat *a2c, st
*/
/*@
requires \valid(b2c);
requires rvalid_FloatQuat(a2b);
requires rvalid_FloatQuat(a2c);
requires \valid_read(a2b);
requires finite_FLOATQUAT(a2b);
requires \valid_read(a2c);
requires finite_FLOATQUAT(a2c);
requires \separated(b2c, a2b) && \separated(b2c, a2c);
assigns *b2c;
*/
extern void float_quat_inv_comp(struct FloatQuat *b2c, struct FloatQuat *a2b, struct FloatQuat *a2c);
......@@ -789,8 +802,11 @@ extern void float_quat_comp_norm_shortest(struct FloatQuat *a2c, struct FloatQua
*/
/*@
requires \valid(a2b);
requires rvalid_FloatQuat(a2c);
requires rvalid_FloatQuat(b2c);
requires \valid_read(a2c);
requires finite_FLOATQUAT(a2c);
requires \valid_read(b2c);
requires finite_FLOATQUAT(b2c);
requires \separated(a2b, a2c) && \separated(a2b, b2c);
assigns *a2b;
*/
extern void float_quat_comp_inv_norm_shortest(struct FloatQuat *a2b, struct FloatQuat *a2c, struct FloatQuat *b2c);
......@@ -800,8 +816,11 @@ extern void float_quat_comp_inv_norm_shortest(struct FloatQuat *a2b, struct Floa
*/
/*@
requires \valid(b2c);
requires rvalid_FloatQuat(a2b);
requires rvalid_FloatQuat(a2c);
requires \valid_read(a2b);
requires finite_FLOATQUAT(a2b);
requires \valid_read(a2c);
requires finite_FLOATQUAT(a2c);
requires \separated(b2c, a2b) && \separated(b2c, a2c);
assigns *b2c;
*/
extern void float_quat_inv_comp_norm_shortest(struct FloatQuat *b2c, struct FloatQuat *a2b, struct FloatQuat *a2c);
......
......@@ -141,6 +141,12 @@ struct Int32Quat {
int32_t qz;
};
#define bound_INT32QUAT(q, bound) \
-bound <= q->qi <= bound \
&& -bound <= q->qx <= bound \
&& -bound <= q->qy <= bound \
&& -bound <= q->qz <= bound \
/*@
predicate bound_Int32Quat(struct Int32Quat *q, integer bound) =
-bound <= q->qi <= bound
......@@ -731,7 +737,8 @@ static inline uint32_t int32_quat_norm(struct Int32Quat *q)
}
/*@
requires valid_bound_Int32Quat(q, INT_MAX);
requires \valid_read(q);
requires bound_INT32QUAT(q, INT_MAX);
ensures q->qi == \old(q->qi) || q->qi == -\old(q->qi);
ensures q->qx == \old(q->qx) || q->qx == -\old(q->qx);
ensures q->qy == \old(q->qy) || q->qy == -\old(q->qy);
......@@ -747,7 +754,8 @@ static inline void int32_quat_wrap_shortest(struct Int32Quat *q)
/** normalize a quaternion inplace */
/*@
requires valid_bound_Int32Quat(q, SQRT_INT_MAX4);
requires \valid_read(q);
requires bound_INT32QUAT(q, SQRT_INT_MAX4);
assigns *q;
*/
static inline void int32_quat_normalize(struct Int32Quat *q)
......@@ -769,9 +777,11 @@ static inline void int32_quat_normalize(struct Int32Quat *q)
*/
/*@
requires \valid(a2c);
requires \valid_read(a2b) && bound_Int32Quat(a2b, SQRT_INT_MAX4);
requires \valid_read(b2c) && bound_Int32Quat(b2c, SQRT_INT_MAX4);
requires \separated(a2c, a2b, b2c);
requires \valid_read(a2b);
requires bound_INT32QUAT(a2b, SQRT_INT_MAX4);
requires \valid_read(b2c);
requires bound_INT32QUAT(b2c, SQRT_INT_MAX4);
requires \separated(a2c, a2b) && \separated(a2c, b2c);
assigns *a2c;
behavior max_norm:
......@@ -798,9 +808,11 @@ extern void int32_quat_comp(struct Int32Quat *a2c, struct Int32Quat *a2b, struct
*/
/*@
requires \valid(a2b);
requires \valid_read(a2c) && bound_Int32Quat(a2c, SQRT_INT_MAX4);
requires \valid_read(b2c) && bound_Int32Quat(b2c, SQRT_INT_MAX4);
requires \separated(a2b, a2c, b2c);
requires \valid_read(a2c);
requires bound_INT32QUAT(a2c, SQRT_INT_MAX4);
requires \valid_read(b2c);
requires bound_INT32QUAT(b2c, SQRT_INT_MAX4);
requires \separated(a2b, a2c) && \separated(a2b, b2c);
assigns *a2b;
behavior max_norm:
......@@ -826,9 +838,11 @@ extern void int32_quat_comp_inv(struct Int32Quat *a2b, struct Int32Quat *a2c, st
*/
/*@
requires \valid(b2c);
requires \valid_read(a2b) && bound_Int32Quat(a2b, SQRT_INT_MAX4);
requires \valid_read(a2c) && bound_Int32Quat(a2c, SQRT_INT_MAX4);
requires \separated(b2c, a2b, a2c);
requires \valid_read(a2b);
requires bound_INT32QUAT(a2b, SQRT_INT_MAX4);
requires \valid_read(a2c);
requires bound_INT32QUAT(a2c, SQRT_INT_MAX4);
requires \separated(b2c, a2b) && \separated(b2c, a2c);
assigns *b2c;
behavior max_norm:
......
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