Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Open sidebar
POLLIEN Baptiste
paparazzi-frama-c
Commits
59aaa4f1
Commit
59aaa4f1
authored
Apr 14, 2021
by
POLLIEN Baptiste
Browse files
Update WP script
parent
d9707758
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
with
4 additions
and
19 deletions
+4
-19
sw/airborne/.frama-c/wp/script/int32_mat_mul_assert_rte_mem_access_5.json
...ma-c/wp/script/int32_mat_mul_assert_rte_mem_access_5.json
+2
-8
sw/airborne/.frama-c/wp/script/int32_mat_mul_assert_rte_mem_access_6.json
...ma-c/wp/script/int32_mat_mul_assert_rte_mem_access_6.json
+1
-7
sw/airborne/.frama-c/wp/script/int32_mat_mul_assert_rte_mem_access_7.json
...ma-c/wp/script/int32_mat_mul_assert_rte_mem_access_7.json
+1
-4
No files found.
sw/airborne/.frama-c/wp/script/int32_mat_mul_assert_rte_mem_access_5.json
View file @
59aaa4f1
...
...
@@ -2,12 +2,6 @@
"select"
:
{
"select"
:
"clause-step"
,
"at"
:
31
,
"kind"
:
"have"
,
"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"
:
"Z3:4.8.6"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"children"
:
{
"Unfold 'P_rvalid_int_mat_3_'"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
7.28
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
}
]
}
}
]
"time"
:
7.28
}
]
}
}
]
sw/airborne/.frama-c/wp/script/int32_mat_mul_assert_rte_mem_access_6.json
View file @
59aaa4f1
...
...
@@ -5,10 +5,4 @@
"children"
:
{
"Unfold 'P_rvalid_int_mat_3_'"
:
[
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"valid"
,
"time"
:
0.87
,
"steps"
:
2170940
},
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
}
]
}
}
]
"steps"
:
2170940
}
]
}
}
]
sw/airborne/.frama-c/wp/script/int32_mat_mul_assert_rte_mem_access_7.json
View file @
59aaa4f1
...
...
@@ -2,10 +2,7 @@
"select"
:
{
"select"
:
"clause-step"
,
"at"
:
31
,
"kind"
:
"have"
,
"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"
,
"verdict"
:
"timeout"
,
"time"
:
12
.
},
{
"header"
:
"Definition"
,
"children"
:
{
"Unfold 'P_rvalid_int_mat_3_'"
:
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-step"
,
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment