Stephen Gaito's comments on the Tutorial

[stephengaito]

This (single?) issue will contain my evolving comments and issues with this (wonderful!) tutorial.
I intend to keep an expanding task list of items I think need addressing. (Feel free to strikethrough any tasks which are out of scope).

• an Appendix describing the WP interactive proof editor (all in one place) which is more detailed than the WP user document's coverage. (created issue Interactive proof editor #47)

  • discussion of how to exit the proof editor and return to the list of WP goals.
  • discussion of what "verified (but has dependencies with Unknown status)" means.... how do I find these dependencies? (I now see that these dependencies are highlighted if I know what to look for.... indeed I now even see a right-click-menu-item devoted to dependencies... however a discussion of what they are and how to find then would be welcome)

• Exercise 3.1.3.3 Alphabet Letter: the provided answer takes longer than the frama-c-gui's default timeout of 10ms(?) -- you might want to add some comments about the possible need to up/change the default timeout? (using this answer with frama-c on the command line succeeds, so your regression tests probably do not show this issue).

... more to come...

See also

• Mathematics of indirect assignment (C-pointers) #48

Contextual information

• Frama-C, Why3, Alt-Ergo installation mode: all via Opam
• Frama-C version: 25.0-beta (Manganese)
• Plug-in used: WP
• Why3 version: Why3 platform, version 1.5.0
• Alt-Ergo version: 2.4.1
• OS name: Ubuntu
• OS version: 21.10 (Impish)
• Number of CPU's: 2
• CPU speed: 2.80GHz
• RAM: 16Gb

[AllanBlanchard]

About exercise 3.1.3.3, which version of Alt-Ergo do you use ? (the timeout is expressed in seconds).

[stephengaito]

@AllanBlanchard As requested I have supplied more context information above.... alas I suspect there may be two problems...

Firstly My machine is rather elderly so 10 seconds of elapsed time might not allow Alt-Ergo enough time ;-(

So an explicit gentle reminder to increase timeouts on older machines would be welcome.... but in hindsight you have implicitly essentially suggested as much.... I was just being a "human of very little brain" and did not notice.

Secondly I have observed that one or other of Frama-C-Gui and/or WP (or even possibly Alt-Ergo) are not clearing their internal state... after a number of attempts at checking something I notice that VCs start to fail which I know should succeed... once I fully restart Frama-C-Gui all of the VCs succeed in the first attempt. Alas there is no repeatable set of actions which exhibit this ... so there is very little way I could raise a meaningful issue on Frama-C/WP.

SO, my problems with exercise 3.1.3.3 might have come from working on an old Frama-C-Gui / WP state... I have just checked that your answer to exercise 3.1.3.3 on my machine fails with 10 seconds timeout but succeeds when run a second time with a 20 second timeout.

When I try your answer with a fresh startup of Frama-C-Gui/WP and 20 seconds timeout, it fails the first time and succeeds on the second attempt...

SO there is some issue with the underlying internal state of Frama-C-Gui/WP/Why3/Alt-Ergo (I note that I still have 9525 MiB of free memory -- so running out of RAM is not the issue) ;-(

I guess I should raise this as an issue with Frama-C-Gui/WP ;-(

I discovered this (mild) "instability" of the Frama-C-Gui while trying to use Frama-C in a way similar to Dafny.... unfortunately rapid editing and re-view of VCs successes are limited by this "instability".... I can not fully trust that VC failures are true failures...

[AllanBlanchard]

On my machine, the proof is produced by Alt-Ergo 2.4.1 in 5 ms. So even if you have an old machine 10 seconds should be enough (there are examples where a bigger timeout is needed, or where I have identified regressions between Alt-Ergo 2.4.0 and 2.4.1).

Let us eliminate some sources of nondeterminism, and check whether the example is proved:

• remove .frama-c directory if there is any in the directory where you run the frama-c command,
• remove ~/.why3.conf and then rerun why3 config detect so that Why3 really has the current Alt-Ergo in its configuration,

First, try running:

frama-c  ex-3-alphabet-answer.c -wp -wp-cache none

Then:

frama-c-gui  ex-3-alphabet-answer.c -wp -wp-cache none

Then:

frama-c-gui  ex-3-alphabet-answer.c

And start the proof via the GUI.

If all of these succeeds, that probably means that there are even more problem with the GUI than we had before and that the reparse button should not be used anymore (so I have to remove it from the tutorial until Ivette is ready).

[stephengaito]

I have removed all .frama-c directories that I could find in and above the directory I am using.

I have removed ~.why3.conf and then run why3 config detect (and then removed all partial_prover entries except the one corresponding to alt-ergo.

code/function-contract/contract$ frama-c ex-3-alphabet-answer.c -wp -wp-cache none
[kernel] Parsing ex-3-alphabet-answer.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 8 goals scheduled
[wp] Proved goals:    8 / 8
  Qed:               7  (0.60ms-8ms-55ms)
  Alt-Ergo 2.4.1:    1  (13ms) (19)
[wp:pedantic-assigns] ex-3-alphabet-answer.c:10: Warning: 
  No 'assigns' specification for function 'main'.
  Callers assumptions might be imprecise.

The command:

code/function-contract/contract$ frama-c-gui ex-3-alphabet-answer.c -wp -wp-cache none

results in:

The command:

code/function-contract/contract$ frama-c-gui ex-3-alphabet-answer.c

results in:

Alas, it looks like on my machine I can not reliably use the reparse button.... taking me even further from Dafny.... hey ho!

[AllanBlanchard]

Stranger and stranger. In the first GUI command, the "Messages" tab indicates 3 messages. Can you show me the messages (and also the content of the console)?

[stephengaito]

While I have re-removed the .frama-c directory and run the frama-c command, the frama-c-gui command:

code/function-contract/contract$ frama-c-gui ex-3-alphabet-answer.c -wp -wp-cache none

Now only gives me two messages:

The console contains:

[kernel] Parsing ex-3-alphabet-answer.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 8 goals scheduled
[wp] [Qed] Goal typed_alphabet_letter_assigns_part3 : Valid (1ms)
[wp] [Qed] Goal typed_alphabet_letter_assigns_part2 : Valid (1ms)
[wp] [Qed] Goal typed_alphabet_letter_assigns_part1 : Valid (1ms)
[wp] [Qed] Goal typed_main_assert_2 : Valid (1ms)
[wp] [Qed] Goal typed_main_assert : Valid (0.99ms)
[wp] [Qed] Goal typed_alphabet_letter_assigns_part4 : Valid (44ms)
[wp] [Qed] Goal typed_main_assert_3 : Valid (4ms)
[wp] [Alt-Ergo 2.4.1] Goal typed_alphabet_letter_ensures : Valid (Qed:61ms) (13ms) (19)
[wp] Proved goals:    8 / 8
  Qed:               7  (0.99ms-14ms-61ms)
  Alt-Ergo 2.4.1:    1  (13ms) (19)
[wp:pedantic-assigns] ex-3-alphabet-answer.c:10: Warning: 
  No 'assigns' specification for function 'main'.
  Callers assumptions might be imprecise.

[AllanBlanchard]

Ok 🤔 . And what are the messages indicated with the third way to start the verification? So:

frama-c-gui  ex-3-alphabet-answer.c

And start the proof via the GUI.

[stephengaito]

@AllanBlanchard Sorry I got distracted :$

code/function-contract/contract$ frama-c-gui ex-3-alphabet-answer.c 

gives:

and in the console:

[kernel] Parsing ex-3-alphabet-answer.c (with preprocessing)
[wp:pedantic-assigns] ex-3-alphabet-answer.c:10: Warning: 
  No 'assigns' specification for function 'main'.
  Callers assumptions might be imprecise.
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
[wp] Proved goals:    0 / 3
[wp] Updated session with 1 new valid script.
[wp] [Qed] Goal typed_main_assert_3 : Valid (64ms)
[wp] [Qed] Goal typed_main_assert_2 : Valid (48ms)
[wp] [Qed] Goal typed_main_assert : Valid (Qed:171ms)
[wp] 5 goals scheduled
[wp] Proved goals:    0 / 5
  Qed:               2  (48ms-94ms-171ms)
  Alt-Ergo 2.4.1:    1
[wp] [Qed] Goal typed_alphabet_letter_assigns_part3 : Valid (9ms)
[wp] [Qed] Goal typed_alphabet_letter_assigns_part2 : Valid (2ms)
[wp] [Qed] Goal typed_alphabet_letter_assigns_part1 : Valid (96ms)
[wp] [Qed] Goal typed_alphabet_letter_assigns_part4 : Valid (6ms)
[wp] No updated script.
[wp] [Alt-Ergo 2.4.1] Goal typed_alphabet_letter_ensures : Timeout (Qed:526ms) (10s)

[AllanBlanchard]

Ok, that's really strange, I'll try to reproduce in VM with your settings.