From a44fc27c4a4b02ed570dd5567ff8d309b885e904 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Thu, 15 Oct 2020 11:33:47 +0100 Subject: [PATCH] Fix z3. --- 2020-frama-c/4500-range-size-2.term | 1 + 2020-frama-c/notes.txt | 13 +++++++++---- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/2020-frama-c/4500-range-size-2.term b/2020-frama-c/4500-range-size-2.term index 7c4b874..ecef5b8 100755 --- a/2020-frama-c/4500-range-size-2.term +++ b/2020-frama-c/4500-range-size-2.term @@ -8,5 +8,6 @@ export title="qemu’s range_size()" # History. remember 'cat snippets/range_size.c' remember 'frama-c -wp -wp-rte snippets/range_size.c' +remember 'frama-c -wp -wp-rte snippets/range_size.c -wp-prover alt-ergo,why3:z3-ce' terminal diff --git a/2020-frama-c/notes.txt b/2020-frama-c/notes.txt index 3dbe211..b7254f7 100644 --- a/2020-frama-c/notes.txt +++ b/2020-frama-c/notes.txt @@ -252,12 +252,17 @@ looks equally trivial and yet it cannot be proven. Why? One way to find the problem would be to find a COUNTEREXAMPLE. A counterexample is an instance of an input that satisfies all of the -preconditions, but makes the postcondition false. Now Frama-C has +preconditions, but makes the postcondition false. Frama-C has pluggable provers, and one prover called Z3, originally written by Microsoft, can be used with Frama-C and can sometimes find -counterexamples. However the version of Z3 in Fedora does not like to -work with the version of Frama-C in Fedora -(https://git.frama-c.com/pub/frama-c/-/issues/33). +counterexamples. + + $ frama-c -wp -wp-rte snippets/range_size.c -wp-prover alt-ergo,why3:z3-ce + +Unfortunately Z3 cannot find a counterexample in this case. I even +upped the timeout to run Z3 longer but it still couldn't find one. + +[Z3 model_compact issue: https://git.frama-c.com/pub/frama-c/-/issues/33] So this is the counterexample which I worked out myself: -- 1.8.3.1