fraunhoferfokus / acsl-by-example Goto Github PK

Public snapshots of "ACSL by Example"

License: MIT License

C 19.94% Makefile 7.86% Shell 4.68% C++ 9.89% Coq 0.34% Perl 3.26% Python 2.42% TeX 51.60%

frama-c acsl wp-plugin formal-methods formal-specification formal-verification c

acsl-by-example's Introduction

Important Note: This software is not actively maintained anymore

As of 2021, ACSL by Example is not maintained anymore. The main reason is that my research centers now on quantum computing. Although this field also demands for formal methods, I have not enough time to continue providing high quality releases of ACSL by Example.

It was a great pleasure for me to learn about the Frama-C tool chain, in particular the Frama-C/WP plug-in. We at Fraunhofer FOKUS could not have produced ACSL by Example without the great help we received from the team of Frama-C at CEA List!

Special thanks also to Denis Efremov from ISPRAS for his contributions to ACSL by Example.

ACSL by Example

This repository contains version 22.0.0 of ACSL by Example --- a collection of C functions and data types whose behavior has been formally specified with ACSL and formally verified with Frama-C/WP.

The directory StandardAlgorithms contains the complete C source code including ACSL annotations of the examples.

This version of ACSL by Example is intended for Frama-C 22.0 and relies among others on the following sofware packages.

Package	Version
Why3	1.3.3
Alt-Ergo	2.3.3
CVC4	1.7
Z3	4.8.6
Coq	8.12.1

For more details on verifying the examples see the file README.txt.

Accompanying LaTeX files

We also inlude for each example corresponding LaTeX file (see directory Informal). This might be interesting for someone who wants to apply machine learning algorithms on this (small) collection of informal and formal specifications. Note that these LaTeX files are not sufficient to generate ACSL by Example.

acsl-by-example's People

Contributors

Stargazers

Watchers

Forkers

jbenden antonalekseev chenmin46 lars-meijer evdenis vandanapgaallee zeta1999 irvise ndinh215 findo monate rahxephon89 asakul popularpinguin mgudemann gaybro8777 vongaisberg lyonel2017 lambda2023

acsl-by-example's Issues

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.

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.

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

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.

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?

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.