-
Notifications
You must be signed in to change notification settings - Fork 20
/
Copy pathREADME.txt
78 lines (53 loc) · 2.45 KB
/
README.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
A number of environment variables affect the generation of reports:
Please check Makefile.template for their precise definitions (including default values).
WP_TIMEOUT (1)
The default timeout when running provers. This value is multiplied
by 1.1 for each additional process after the first in $WP_PROCESSES.
WP_COQ_TIMEOUT (5)
The timeout for coq. This timeout is scaled in the same way
WP_TIMEOUT is.
WP_PROCESSES (1)
The number of provers to run in parallel.
SCRIPT (wp0.script)
The proof script used for discharging proof obligations with coq.
You probably won't need to touch this variable.
Library of Standard Algorithms
================================
The directories 'mutating', 'nonmutating', 'binary_search', 'stack', 'maxmin' and so on
group algorithms together. Each contains subfolders for every specified algorithm.
In each folder <algorithm> you can find the following files:
<algorithm>.c
<algorithm>.h
<algorithm>_test.cpp contains a C++ testfile where algorithm is compared to/with std::algorithm
If some obligations are proven with Coq, then there is a file 'wp0.script' which contains the proofs.
In addition each subfolder contains a makefile, see usage below.
Besides there is directory 'Scripts' to enable the makefile oppurtunities.
The directory 'Logic' is a collection of lemmas and logic functions used
in the ACSL specifications.
USAGE:
========
For individual examples, the most interesting targets are
make clean
- remove generate files in example directory
make wpgui
- runs Frama-C/WP on the example and shows the results in the Frama-C GUI
make wp
- runs Frama-C/WP on the example and shows the results on the command line
supported commands in directory StandardAlgorithms:
----------------------------------------------------
make clean
- removes all generated files for each algorithm in the subfolders
make report-clean
- remove verification results for all examples
make preport-clean
- remove verification results for all examples and all provers
make test
- compiles and runs the testfiles for each algorithm in the subfolders
- if successful it outputs: successful test of different <algorithm> implementations
make report
- generate verification results for all examples
- call 'make report-clean' before generating new reports
make preport
- generate verification results for all examples when running all provers on all
proof obligations
- call 'make preport-clean' before generating new reports