fraunhoferfokus / acsl-by-example Goto Github PK

https://github.com/fraunhoferfokus/acsl-by-example/blob/master/StandardAlgorithms/nonmutating/find/find.h has the following spec:

ensures   0 <= \result <= \result;

the right part of which is always true. Did you mean 0 <= \result <= n?

just a trial

In the latest version of ACSL by Example (i.e., 16.1.0), I think Figure 5.5 on page 66 is incorrect. Node '11' is pointing to index 6 but I think it should be pointing to index 7.

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.

This issue is intended to test the email notification mechanism.

Hi, i am new to frama-c. I want to know how to use this repo.
I download this repo, and type make, then I don't know how to use it.
When i type make is_sorted.wp(in the is_sorted subdir), it gives me a error, could you please tell me
how to use this repo, I am confused with readme.txt. Thanks.

In section 3.5.2 (Formal specification of equal and mismatch), the first sentence reads: "Using predicate equal_range we can formulate the specification of equal..." . Given that EqualRanges (and not equal_range) was the predicate defined just above this section, I believe you meant: "Using predicate EqualRanges ...".

BTW: I was going to submit a patch but I did not find the files that are used to generate the pdf. This is the reason why I did not submit a patch.

I've already mentioned that the cache should be dropped before the merge #12 for TravisCI to work . It can be done on TravisCI site "More Options" > "Cache" > "Delete" (#12 (comment)). This will make the tests pass. After the changes in #12 system compiler is not used anymore and opam should be reinitialized, but the existing cache prevents it.

There seems to be a missmatch between the default values for time and step limits in README.txt and in Makefile.template.

README.txt:

WP_TIMEOUT (20)
WP_COQ_TIMEOUT (20)
WP_ALT_ERGO_STEPS (1000)

Makefile.template:

export WP_TIMEOUT ?= 10
export WP_COQ_TIMEOUT ?= 10
export WP_ALT_ERGO_STEPS ?= 10000

@evdenis

I have created a potassium branch on GitHub and also started adapting to the travis file for the new tools. I think I need your help with installing z3 (4.8.4).