fraunhoferfokus/acsl-by-example

Public snapshots of "ACSL by Example"

acsl-by-example's Issues

Test issue

This issue is intended to test the email notification mechanism.

how to use this repo

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.

preparing potassium for travis

@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).

Minor mistake in section 3.5.2

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.

V16.1.0 : Figure 5.5 appears to be incorrect

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.

tautological inequality in the find algorithm ACSL

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?

Different default values in makefile and readme

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

communication check

just a trial

TravisCI: clean the cache

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.

Make error for `heap`

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.