Skip to content

Instantly share code, notes, and snippets.

@hyarion
Created December 11, 2018 23:34
Show Gist options
  • Save hyarion/1958059b008e2699430ed3fea46ef4dd to your computer and use it in GitHub Desktop.
Save hyarion/1958059b008e2699430ed3fea46ef4dd to your computer and use it in GitHub Desktop.
[WIP] Frama-C 18.0 (Argon) + Why3 1.1.0
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