Created
December 11, 2018 23:34
-
-
Save hyarion/1958059b008e2699430ed3fea46ef4dd to your computer and use it in GitHub Desktop.
[WIP] Frama-C 18.0 (Argon) + Why3 1.1.0
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
hyarion$ frama-c -wp -wp-prover=cvc4,z3-ce isqrt.c | |
[kernel] Parsing isqrt.c (with preprocessing) | |
[wp] Warning: Missing RTE guards | |
[wp] 61 goals scheduled | |
[wp] Proved goals: 61 / 61 | |
Qed: 41 (0.30ms-14ms-56ms) | |
cvc4: 2 (140ms) | |
z3-ce: 19 (30ms-221ms-1.8s) | |
hyarion$ why3 --version | |
Why3 platform, version 1.1.0 | |
hyarion$ frama-c -wp -wp-detect | |
[wp] Prover Known provers [Known:provers] | |
[wp] Prover Alt-Ergo 2.2.0 [Alt-Ergo:2.2.0] | |
[wp] Prover CVC4 1.6 [CVC4:1.6] | |
[wp] Prover CVC4 1.6 [CVC4:1.6] | |
[wp] Prover Gappa 1.3.2 [Gappa:1.3.2] | |
[wp] Prover Z3 4.8.3 [Z3:4.8.3] | |
[kernel] Warning: no input file. | |
[wp] 0 goal scheduled | |
[wp] Proved goals: 0 / 0 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment