Make error for heap

[mgudemann]

Hi,

when I try to redo the proofs using the provided Makefile, I get the following error

~/s/g/H/V/a/StandardAlgorithms (master|✔) $ why3 config --full-config
Found prover CVC4 version 1.7 (alternative: counterexamples)
Found prover CVC4 version 1.7, OK.
Found prover CVC3 version 2.4.1, OK.
Found prover Z3 version 4.8.6 (alternative: counterexamples)
Found prover Z3 version 4.8.6, OK.
Found prover Z3 version 4.8.6 (alternative: noBV)
Found prover Coq version 8.10.2, OK.
Prover Alt-Ergo version 2.3.2 is not known to be supported.
Known versions for this prover: 2.3.1, 2.3.0.
Known old versions for this prover: .
8 prover(s) added (including 1 prover(s) with an unrecognized version)
Generating strategies:
  Prover Z3 4.8.6 will be used in Auto level >= 1
  Prover CVC4 1.7 will be used in Auto level >= 1
Save config to /home/guedemann/.why3.conf
~/s/g/H/V/a/StandardAlgorithms (master|✔) $ make
nonmutating
maxmin
binarysearch
mutating
numeric
heap
make[2]: *** No rule to make target '"', needed by '@echo'.  Stop.
make[1]: *** [../Config/group.mk:50: heap_parent] Error 2
make: *** [Makefile:25: heap] Error 2

The version of Z3 and Coq differs slightly, is the error related to that difference?

Trying to solve this problem I also found that StandardAlgorithms/README.txt refers to a Makefile.template which has been deleted in cb67e3f
The described variables seem to be in Config/frama-c.mk now.

[jensgerlach]

README.txt is not up to date. Sorry for that.
I will also look at the particular problem of heap_parent

Another problem is that there is no meaningful default target in Makefile.
You should/could call.

• make test (recursively runs very basic tests)
• make report-clean and then make report which prints some numbers about the verification of the various examples. (This might take a long time and the printed numbers are not really explained.)

It might, however, make more sense to go to the individual examples.

• Calling there make wpgui runs Frama-C/WP and opens the Frama-C GUI.
• make wp just calls Frama-C/WP on the command line.

Hope this helps.

[jensgerlach]

The problem you reported has been fixed in the development version.
Thanks a lot!

[mgudemann]

@jensgerlach
With make report it works as intended.
Thank you very much for the explanation and the quick fix!