-
Notifications
You must be signed in to change notification settings - Fork 1
/
README
executable file
·111 lines (73 loc) · 3.98 KB
/
README
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
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
---------------------------- EZPROOFC TOOL (Beta) v3 -------------------------------
.-.
/v\
// \\ > L I N U X - GPL<
/( )\
^^-^^
__________________________________________________________________________________________
Goal: This tool aims to automate the method proposed aims to automate the collection and manipulation of counterexamples in order to instantiate a C program for proving the root cause of the identified error. Such method may be seen as a complementary technique for the verification performed by Bounded Model Checkers
Author: Herbert O. Rocha E-mail: herberthb12@gmail.com
Version: 3 - Year: 2012
Status: This tool is still in development phase to full implementation of the proposed method in this approach.
__________________________________________________________________________________________
-> Requirements for using the tool
__________________________________________________________________________________________
To use this tool is necessary that the system contains the following software already installed properly:
- Python;
- Perl;
- And the ESBMC model checker, which you should set the environment variable PATH in your .bashrc.
__________________________________________________________________________________________
-> How to install ESBMC?
__________________________________________________________________________________________
The ESBMC can be downloaded at http://esbmc.org/
In order to install ESBMC on your PC, you should download and save the esbmc-vx.x.tar.gz file on your disk.
After that, you should type the following command:
$ tar -xzvf esbmc-v1.12.tar.gz
The ESBMC distribution is split into three directories:
- bin
- smoke-tests
- licenses
The directory bin contains the binary file of ESBMC. The directory smoke-tests contains some ANSI-C programs and also
includes a shell script that can be used to collect experimental results for different ANSI-C benchmarks
(e.g., check the encoding time, decision procedure time, total number of lines of code, total number of properties
to be verified, how many properties passed, violated and failed during the verification process).
You should set the environment variable PATH in your .bashrc file as follows:
$ export PATH=$PATH:/home/herbert/esbmc-vx.x/bin/
__________________________________________________________________________________________
-> How to install EZProofC?
__________________________________________________________________________________________
In order to install EZProofC on your PC, you should download and save the EZProofC_vx.tar.gz file on your disk.
After that, you should type the following command:
>> STEP 1:
$ tar -xzvf EZProofC_vx.tar.gz
The EZProofC distribution is split into directories and files:
- code_samples (Samples codes to apply EZProofC)
- modules
- instanciation
- preprocessor
- verification
- README
- ezproofc.sh
- config.sh
>> STEP 2:
Open the directory where the EZProofC tool was extracted and then you should locate the config.sh and ezproofc script. After that, you should run the config.sh script, it is worth to say that you should run the config.sh script from inside the directory where EZProofC was extracted.
Example:
1) $ cd EZProofC_vx
2) $ ls
code_samples <config.sh> <ezproofc> modules README
3) $ ./config.sh
>> STEP 3:
It is advisable that you should set the environment variable PATH in your .bashrc file as follows:
$ export PATH=$PATH:/home/user/EZProofC_vx/
>> STEP 4:
Testing EZProofC
$ ezproofc code_samples/D_CBMC_bound_array.c
__________________________________________________________________________________________
-> How running the EZProofC?
__________________________________________________________________________________________
Running EZProofC.
$ ezproofc <file.c>
For help and others options:
$ ezproofc -h
__________________________________________________________________________________________
------------------------------------------------------------------------------------------