Commit 1824d063 authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

Removing assert

parent 2b2194c6
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "clause-step", "at": 30, "kind": "have",
"target": "let a_0 = Mptr_2[(shift_PTR o_0 i_0)] in\n(P_rvalid_int_mat_3_ Malloc_2 Mptr_2\n (havoc Mint_undef_0 Mint_13 (shift_sint32 a_0 0) l_0)\n [(shift_sint32 a_0 j_0)->v_0] b_0 n_0 l_0\n (to_sint32\n (\\truncate (\\sqrt (real_of_int (to_sint32 (2147483647 div n_0)))))))",
"target": "let a_0 = Mptr_0[(shift_PTR o_0 i_0)] in\n(P_rvalid_int_mat_3_ Malloc_0 Mptr_0\n (havoc Mint_undef_0 Mint_9 (shift_sint32 a_0 0) l_3)[(shift_sint32 a_0 j_0)\n ->v_0] b_0 n_0 l_3\n (to_sint32\n (\\truncate (\\sqrt (real_of_int (to_sint32 (2147483647 div n_0)))))))",
"pattern": "P_rvalid_int_mat_3_$Malloc$Mptr[=]" },
"children": { "Unfold 'P_rvalid_int_mat_3_'": [ { "header": "Definition",
"tactic": "Wp.unfold",
......@@ -8,7 +8,7 @@
"select": { "select": "clause-step",
"at": 31,
"kind": "have",
"target": "let a_1 = Mptr_2[(shift_PTR o_0 i_0)] in\n(P_rvalid_int_mat_3_ Malloc_2 Mptr_2\n (havoc Mint_undef_0 Mint_13 (shift_sint32 a_1 0) l_0)\n [(shift_sint32 a_1 j_0)->v_0] a_0 m_0 n_0\n (to_sint32\n (\\truncate (\\sqrt (real_of_int (to_sint32 (2147483647 div n_0)))))))",
"target": "let a_1 = Mptr_0[(shift_PTR o_0 i_0)] in\n(P_rvalid_int_mat_3_ Malloc_0 Mptr_0\n (havoc Mint_undef_0 Mint_9 (shift_sint32 a_1 0) l_3)[(shift_sint32 a_1 j_0)\n ->v_0] a_0 m_2 n_0\n (to_sint32\n (\\truncate (\\sqrt (real_of_int (to_sint32 (2147483647 div n_0)))))))",
"pattern": "P_rvalid_int_mat_3_$Malloc$Mptr[=]" },
"children": { "Unfold 'P_rvalid_int_mat_3_'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
......
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "clause-step", "at": 30, "kind": "have",
"target": "let a_0 = Mptr_2[(shift_PTR o_0 i_0)] in\n(P_rvalid_int_mat_3_ Malloc_2 Mptr_2\n (havoc Mint_undef_0 Mint_13 (shift_sint32 a_0 0) l_0)\n [(shift_sint32 a_0 j_0)->v_0] b_0 n_0 l_0\n (to_sint32\n (\\truncate (\\sqrt (real_of_int (to_sint32 (2147483647 div n_0)))))))",
"target": "let a_0 = Mptr_0[(shift_PTR o_0 i_0)] in\n(P_rvalid_int_mat_3_ Malloc_0 Mptr_0\n (havoc Mint_undef_0 Mint_9 (shift_sint32 a_0 0) l_3)[(shift_sint32 a_0 j_0)\n ->v_0] b_0 n_0 l_3\n (to_sint32\n (\\truncate (\\sqrt (real_of_int (to_sint32 (2147483647 div n_0)))))))",
"pattern": "P_rvalid_int_mat_3_$Malloc$Mptr[=]" },
"children": { "Unfold 'P_rvalid_int_mat_3_'": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
......
......@@ -1283,19 +1283,14 @@ static inline void int32_mat_mul(int32_t **o, int32_t **a, int32_t **b, int m, i
loop variant n - k;
*/
for (k = 0; k < n; k++) {
//@ assert rvalid_int_mat(a, m, n, SQRT_INTM_n);
//@ assert rvalid_int_mat(b, n, l, SQRT_INTM_n);
//@ assert -SQRT_INTM_n <= a[i][k] <= SQRT_INTM_n;
//@ assert -SQRT_INTM_n <= b[k][j] <= SQRT_INTM_n;
//@ assert -INT_MAX_n <= a[i][k] * b[k][j] <= INT_MAX_n;
//@ assert -k * INT_MAX_n <= o[i][j] <= k * INT_MAX_n;
//@ assert -(k+1) * INT_MAX_n <= o[i][j] + a[i][k] * b[k][j]<= (k+1) * INT_MAX_n;
//@ assert k < n;
//@ assert (k+1) * INT_MAX_n <= INT_MAX;
o[i][j] += a[i][k] * b[k][j];
//@ assert -(k+1) * INT_MAX_n <= o[i][j] <= (k+1) * INT_MAX_n;
//@ assert rvalid_int_mat(a, m, n, SQRT_INTM_n);
//@ assert rvalid_int_mat(b, n, l, SQRT_INTM_n);
// assert -(k+1) * INT_MAX_n <= o[i][j] <= (k+1) * INT_MAX_n;
}
}
}
......
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