unexpected text 'ite'

[b-pc]

With Frama-C 20.0-beta, the cvc4-ce prover outputs strange and disturbing messages. Here is a small and stupid demonstration :

$ frama-c -version 20.0-beta (Calcium)%

$ why3 --list-provers Known provers: Alt-Ergo 2.3.0 CVC4 1.6 CVC4 1.6 (counterexamples) Z3 4.8.6 Z3 4.8.6 (counterexamples) Z3 4.8.6 (noBV)

$ echo "/@ ensures 1 == 2; / void fo(){}" > bar.c

$ frama-c -wp -wp-prover cvc4 bar.c
[kernel] Parsing bar.c (with preprocessing) [wp] Warning: Missing RTE guards [wp] 1 goal scheduled [wp] [CVC4 1.6] Goal typed_foo_ensures : Timeout (10s) [wp] Proved goals: 0 / 1 CVC4 1.6: 0 (interrupted: 1)

$ frama-c -wp -wp-prover cvc4-ce bar.c
[kernel] Parsing bar.c (with preprocessing) [wp] Warning: Missing RTE guards [wp] 1 goal scheduled [wp] Waiting provers...File "Model string returned from the prover", line 1, characters 971-971: warning: Error during parsing of smtlib model: unexpected text 'ite' [wp] [CVC4 1.6 (counterexamples)] Goal typed_foo_ensures : Timeout (10s) [wp] Proved goals: 0 / 1 CVC4 1.6 (counterexamples): 0 (interrupted: 1)

[vprevosto]

This looks like a why3 message, indicating that it is unable to understand the counter example provided by CVC4. From a Frama-C point of view, this does not change anything, though: the prover does not validate the proof obligation, and WP does not currently try to interpret the counter-example anyways.

NB: with why3 1.2.0, I don't see any warning from why3. What is your version?

[b-pc]

$ why3 --version Why3 platform, version 1.2.1

I have just tried with why3 1.2.0 and the strange message is still here.

BTW, Even when cvc4-ce validates everything, it still outputs tons of these unexpected message.

[vprevosto]

OK, I'm now able to see the message as well. I don't know what happened with my previous attempts.

I can confirm that the message comes from why3 and that it is merely an issue in trying to interpret the output of CVC4 as a model, without any impact on the verdict itself. I don't know the cvc4-ce driver of Why3 in detail, but it is possible that it tries to find a model regardless of the validity verdict emitted by the prover.

In any case, there is no advantage in using cvc4-ce over cvc4 from WP, since WP will not be able to take advantage of a model, even if Why3 is able to correctly interpret it.

[b-pc]

I must respectfully disagree : cvc4-ce allows WP to prove my code, but cvc4 does not. Idem with z3-ce / z3. Anyway, I'm happy that you have been able to reproduce the message !

[vprevosto]

It's quite weird, as the distinction between plain cvc4/z3 and its -ce variant is supposed to be purely restricted to generating the model. However, upon closer look in the Why3 config, it appears that the command differs slightly: instead of giving a global timeout, in the case of the -ce variant, the prover is given a bound per query. It might be the case that increasing timeout in WP will let you succeed with the plain prover as well.

[b-pc]

I already use quite long timeouts. Here are extracts from my logs.

With cvc4 : [wp] [CVC4 1.6] Goal typed_pmsm_del_pg_ensures_3 : Timeout (Qed:310ms) (20') [wp] [CVC4 1.6] Goal typed_pmsm_del_pt_ensures_3 : Timeout (Qed:652ms) (20') [wp] [CVC4 1.6] Goal typed_pmsm_zap_pg_ensures_2 : Timeout (Qed:77ms) (20') [wp] Proved goals: 696 / 699 Qed: 440 (0.87ms-79ms-2.4s) CVC4 1.6: 256 (60ms-1.5s-1'24s) (interrupted: 3)

With cvc4-ce: File "Model string returned from the prover", line 1, characters 971-971: warning: Error during parsing of smtlib model: unexpected text 'ite' [wp] [CVC4 1.6 (counterexamples)] Goal typed_pmsm_add_pg_ensures_5 : Valid (Qed:489ms) (3'35s) [wp] Proved goals: 699 / 699 Qed: 440 (0.81ms-85ms-2.4s) CVC4 1.6 (counterexamples): 259 (50ms-2.4s-3'35s)

Bizarre...vous avez dit bizarre ?

[vprevosto]

Yep, I'm saying bizarre. Unfortunately, as mentioned in #31 , the move in 20.0 to use Why3 API instead of launching why3 on the command line on a generated file resulted in the fact that there's currently no easy way to observe what is going on between why3 and cvc4, which would help in understanding the issue at hand. The possibility to generate Why3 files will be restored in the future, though, making the problem easier to investigate.

[maroneze]

Due to Frama-C's migration to Gitlab, and inactivity related to this issue, it will be closed and assumed to be fixed/outdated. Please feel free to reopen it on our Gitlab issues page, or leave a comment here if the issue is still relevant, in which case we will migrate it to our Gitlab.