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
0edd19ed
Commit
0edd19ed
authored
May 11, 2021
by
POLLIEN Baptiste
Browse files
Increase timeout
parent
29360726
Changes
7
Hide whitespace changes
Inline
Side-by-side
Showing
7 changed files
with
10 additions
and
10 deletions
+10
-10
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_assert_8.json
...borne/.frama-c/wp/script/float_rmat_of_quat_assert_8.json
+3
-3
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_ensures_2.json
...orne/.frama-c/wp/script/float_rmat_of_quat_ensures_2.json
+1
-1
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_ensures_3.json
...orne/.frama-c/wp/script/float_rmat_of_quat_ensures_3.json
+1
-1
sw/airborne/.frama-c/wp/script/lemma_anticomm_cross_product.json
...orne/.frama-c/wp/script/lemma_anticomm_cross_product.json
+1
-1
sw/airborne/.frama-c/wp/script/lemma_quat_of_rmat_ortho.json
sw/airborne/.frama-c/wp/script/lemma_quat_of_rmat_ortho.json
+1
-1
sw/airborne/.frama-c/wp/script/lemma_verify_rmat_of_quat_formula.json
....frama-c/wp/script/lemma_verify_rmat_of_quat_formula.json
+1
-1
sw/airborne/frama-c-analysis.sh
sw/airborne/frama-c-analysis.sh
+2
-2
No files found.
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_assert_8.json
View file @
0edd19ed
...
...
@@ -3,9 +3,9 @@
"target"
:
"(separated rm_0 9 q_0 4)"
,
"pattern"
:
"separated$rm9$q4"
},
"children"
:
{
"WrongBase"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
2.
16
}
],
"verdict"
:
"valid"
,
"time"
:
2.
05
}
],
"OnLeft"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
4.2
8
}
],
"verdict"
:
"valid"
,
"time"
:
4.2
2
}
],
"OnRight"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
4.3
}
],
"verdict"
:
"valid"
,
"time"
:
4.3
1
}
],
"OverLap"
:
[
{
"prover"
:
"qed"
,
"verdict"
:
"valid"
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_ensures_2.json
View file @
0edd19ed
...
...
@@ -63,5 +63,5 @@
{
"Unfold 'P_unary_quaternion_1_'"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
8.
0048
,
"time"
:
8.
7116
,
"steps"
:
144
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_ensures_3.json
View file @
0edd19ed
...
...
@@ -33,5 +33,5 @@
{
"Unfold 'P_unary_quaternion_1_'"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
2.
9
,
"time"
:
2.
7335
,
"steps"
:
28
}
]
}
}
]
}
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/lemma_anticomm_cross_product.json
View file @
0edd19ed
...
...
@@ -31,7 +31,7 @@
{
"Unfold 'EqS12_RealVect3_s'"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
0.003
8
,
"time"
:
0.003
7
,
"steps"
:
8
},
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
...
...
sw/airborne/.frama-c/wp/script/lemma_quat_of_rmat_ortho.json
View file @
0edd19ed
...
...
@@ -63,5 +63,5 @@
{
"Unfold 'EqS13_RealRMat_s'"
:
[
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
0.0
2
,
"time"
:
0.0
4
,
"steps"
:
51791
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/lemma_verify_rmat_of_quat_formula.json
View file @
0edd19ed
...
...
@@ -193,5 +193,5 @@
{
"Unfold 'L_add_RealVect3'"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
2.9623
,
"time"
:
3.4797
,
"steps"
:
142
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
sw/airborne/frama-c-analysis.sh
View file @
0edd19ed
...
...
@@ -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 -wp-prover alt-ergo,cvc4-strings-ce,z3,z3-ce,z3-nobv,coq,tip -wp-timeout
15
-wp-log r:"
$TMP_FILE_RES
WP_ARGS
=
"-wp-cache update -wp-model real+Cast -wp-prover alt-ergo,cvc4-strings-ce,z3,z3-ce,z3-nobv,coq,tip -wp-timeout
20
-wp-log r:"
$TMP_FILE_RES
RTE
=
"-rte -no-warn-left-shift-negative"
# Enable somke tests
...
...
@@ -97,4 +97,4 @@ do
cat
$TMP_RES_GOALS
done
rm
-rf
$TMP_FOLDER
\ No newline at end of file
rm
-rf
$TMP_FOLDER
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