1

When I run the WP example, there is an error, and i don't know what it is.

/*@ requires \valid(a) && \valid(b);
  @ ensures A: *a == \old(*b) ;
  @ ensures B: *b == \old(*a) ;
  @ assigns *a,*b ;
@*/
void swap(int *a, int *b){
    int tmp = *a;
    *a = *b;
    *b = tmp;
    // int tmp = *b;
    // *b = *a;
    // *a = tmp;
}

this is the error in console of frama-c-gui

[wp] No updated script.
[wp] [Alt-Ergo 2.3.1] Goal typed_swap_ensures_A : Failed
  Unknown error

the output after executing " frama-c -wp -wp-rte swap.c"

[kernel] Parsing swap.c (with preprocessing)
[rte] annotating function swap
[wp] 8 goals scheduled
[wp] [Alt-Ergo 2.0.0] Goal typed_swap_assert_rte_mem_access : Failed
  Unknown error
[wp] [Alt-Ergo 2.0.0] Goal typed_swap_ensures_A : Failed
  Unknown error
[wp] [Alt-Ergo 2.0.0] Goal typed_swap_assert_rte_mem_access_3 : Failed
  Unknown error
[wp] Proved goals:    5 / 8
  Qed:               5  (16ms)
  Alt-Ergo 2.0.0:    0  (failed: 3)

Thank you very much if you can help me

Jens
  • 69,818
  • 15
  • 125
  • 179
王少鹏
  • 11
  • 2

1 Answers1

0

Which frama-c version do you have ?

With Alt-Ergo 2.3.3 and frama-c 21.1 (Scandium)

[bash] frama-c -wp -wp-rte ex.c
[kernel] Parsing ex.c (with preprocessing)
[rte] annotating function swap
[wp] 8 goals scheduled
[wp] Proved goals:    8 / 8
  Qed:               5  (1ms-3ms-6ms)
  Alt-Ergo 2.3.3:    3  (8ms-12ms) (50)

With Alt-Ergo 2.0.0 and frama-c 21.1, I get an error but it's different from yours:

frama-c -wp -wp-rte ex.c
[kernel] Parsing ex.c (with preprocessing)
[rte] annotating function swap
[wp] 8 goals scheduled
[wp] [Alt-Ergo 2.3.3] Goal typed_swap_assert_rte_mem_access : Failed
  Failure : File generation error :  syntax error
[wp] [Alt-Ergo 2.3.3] Goal typed_swap_ensures_A : Failed
  Failure : File generation error :  syntax error
[wp] [Alt-Ergo 2.3.3] Goal typed_swap_assert_rte_mem_access_3 : Failed
  Failure : File generation error :  syntax error
[wp] Proved goals:    5 / 8
  Qed:               5  (1ms-2ms-5ms)
  Alt-Ergo 2.3.3:    0  (failed: 3)
iguerNL
  • 464
  • 2
  • 8
  • Did you refresh the Why3 configuration between the two trials? (Frama-C 21: `rm ~/.why3.conf ; why3 config --full-config`, Frama-C 22: `rm ~/.why3.conf ; why3 config --detect`). – Ksass'Peuk Dec 14 '20 at 07:16
  • When I use the command:**why3 config --detect**,the result is **Prover Alt-Ergo version 2.3.3 is not known to be supported. Known versions for this prover: 2.3.1, 2.3.0. Known old versions for this prover: . 1 prover(s) added (including 1 prover(s) with an unrecognized version) Save config to /home/charles/.why3.conf**. So my version of Alt-Ergo is 2.3.0 – 王少鹏 Dec 14 '20 at 09:06
  • And what version of Frama-C do you use? – Ksass'Peuk Dec 14 '20 at 10:19
  • The version of Frama-C is 21.1 – 王少鹏 Dec 14 '20 at 10:49
  • With Frama-C 21.1 you should do: `rm ~/.why3.conf ; why3 config --full-config` . (And for Frama-C 22+, `rm ~/.why3.conf ; why3 config --detect`). Note that the fact that a prover is not supported by Why3 does not necessarily means that it won't work, just that it has not been tested so far. – Ksass'Peuk Dec 14 '20 at 11:15
  • I had downgraded the version of Alt-Ergo to 2.3.1，and do: `rm ~/.why3.conf ; why3 config --full-config`.But it didn't work.The output is `[wp] [Alt-Ergo 2.3.1] Goal typed_swap_ensures_A : Failed [wp] [Cache] found:1` – 王少鹏 Dec 15 '20 at 14:03
  • do: `frama-c -wp swap.c`. The output is:`[kernel] Parsing swap.c (with preprocessing) [wp] Warning: Missing RTE guards [wp] 2 goals scheduled [wp] [Alt-Ergo 2.3.1] Goal typed_swap_ensures_A : Failed [wp] [Cache] found:1 [wp] Proved goals: 1 / 2 Qed: 1 Alt-Ergo 2.3.1: 0 (cached: 1) (failed: 1)` – 王少鹏 Dec 15 '20 at 14:04
  • Try removing the existing cache entries `rm .frama-c` in the directory where you run the proof. It seems that WP does a cache hit on the failed PO. – Ksass'Peuk Jan 05 '21 at 14:45