Overview

Version 20 (Stefan Blom, 23 Sep 2013 16:31)

1 1 Stefan Blom
h1. Overview
2 1 Stefan Blom
3 20 Stefan Blom
!>{width:100px}http://fmt.ewi.utwente.nl/files/LOGO-ERC.jpg!
4 20 Stefan Blom
5 3 Stefan Blom
The "VerCors project":http://fmt.ewi.utwente.nl/research/projects/VerCors/ is about Verification of Concurrent Data Structures.
6 1 Stefan Blom
7 1 Stefan Blom
The VerCors toolset currently consists of two tools:
8 2 Stefan Blom
* "Histogram":http://fmt.ewi.utwente.nl/tools/histogram: a tool for creating Histograms of class/method occurrences.
9 2 Stefan Blom
* [[Verifier Overview|The VerCors verifier]]: an annotated code compiler/verifier.
10 4 Stefan Blom
11 16 Stefan Blom
h1. Online Demo
12 1 Stefan Blom
13 17 Stefan Blom
Several verified examples are available in the "online version of the verifier":http://fmt.ewi.utwente.nl/puptol/vercors-verifier/ , described 
14 18 Stefan Blom
[[Puptol|here]]
15 5 Stefan Blom
16 16 Stefan Blom
h1. Prerequisites for the distributions.
17 1 Stefan Blom
18 16 Stefan Blom
To run the tools, you will need a Java 7 Runtime Environment. Note that the toolset has been tested with the Oracle Java 1.7 SE SDK. Compatibility with other JVMs is untested.
19 5 Stefan Blom
20 16 Stefan Blom
h2. Windows
21 1 Stefan Blom
22 16 Stefan Blom
The tool distribution requires no non-standard components.
23 1 Stefan Blom
24 16 Stefan Blom
h2. Linux
25 1 Stefan Blom
26 5 Stefan Blom
You need mono, version 2.10 or better, to run Boogie.
27 5 Stefan Blom
28 16 Stefan Blom
Note that, not all common Linux distributions include a sufficiently up-to-date version of mono. Thus you may need to download sources from http://www.mono-project.com/ and follow instructions on how to compile them.
29 16 Stefan Blom
30 16 Stefan Blom
h2. Mac OS X
31 16 Stefan Blom
32 16 Stefan Blom
You need mono, version 2.10 or better, to run Boogie.
33 16 Stefan Blom
34 16 Stefan Blom
For installing mono, you have many options. For example:
35 16 Stefan Blom
# Get a binary distribution from http://www.mono-project.com/.
36 16 Stefan Blom
# Get the sources from http://www.mono-project.com/ and install them.
37 16 Stefan Blom
# Install using macports:
38 1 Stefan Blom
  <pre>
39 12 Stefan Blom
  sudo port install mono???
40 1 Stefan Blom
  </pre>
41 12 Stefan Blom
42 12 Stefan Blom
43 16 Stefan Blom
h1. Binary Distribution
44 12 Stefan Blom
45 16 Stefan Blom
h2. Obtaining the code
46 16 Stefan Blom
47 16 Stefan Blom
There is no public release yet. Please ask for a copy by email.
48 16 Stefan Blom
49 16 Stefan Blom
h2. Installation
50 16 Stefan Blom
51 16 Stefan Blom
# Given the zip archive with the binary distribution. E.g. @vct-1.0.zip@.
52 1 Stefan Blom
# Extract the files from the zip archive.
53 1 Stefan Blom
# For easy command line access: add the bin subdirectory to your PATH variable.
54 1 Stefan Blom
55 16 Stefan Blom
h1. Source Distribution
56 5 Stefan Blom
57 1 Stefan Blom
The source distribution has been structured to allow both command line building with ant and development with eclipse.
58 1 Stefan Blom
59 5 Stefan Blom
h2. Getting the sources.
60 5 Stefan Blom
61 5 Stefan Blom
There are two ways to get the sources:
62 5 Stefan Blom
63 1 Stefan Blom
# Download a zip archive.
64 5 Stefan Blom
# Clone one of the git repositories.
65 5 Stefan Blom
66 1 Stefan Blom
h3. Git repository.
67 10 Stefan Blom
68 7 Stefan Blom
See [[Installing git for windows]].
69 7 Stefan Blom
70 5 Stefan Blom
* SSH based git server.
71 16 Stefan Blom
>> access: create an SSH key pair and email the public key to Stefan Blom.
72 12 Stefan Blom
>> URL: gitshare@sccblom.ewi.utwente.nl:vercors-toolset.git
73 10 Stefan Blom
74 12 Stefan Blom
Note that the git repository has submodules. That is, after cloning one of the git repositories
75 13 Stefan Blom
you must initialize submodules
76 13 Stefan Blom
<pre>
77 13 Stefan Blom
git submodule update --init
78 13 Stefan Blom
</pre>
79 12 Stefan Blom
and after every update, you must synchronize
80 12 Stefan Blom
the submodules:
81 5 Stefan Blom
<pre>
82 12 Stefan Blom
git submodule sync
83 12 Stefan Blom
git submodule update
84 10 Stefan Blom
</pre>
85 5 Stefan Blom
86 5 Stefan Blom
h2. Command line building.
87 5 Stefan Blom
88 9 Stefan Blom
Command line building uses Apache ant. To build the tool set go to the root directory and enter the command 
89 5 Stefan Blom
<pre>
90 5 Stefan Blom
ant
91 5 Stefan Blom
</pre>
92 5 Stefan Blom
To create a distribution enter
93 5 Stefan Blom
<pre>
94 5 Stefan Blom
ant dist
95 5 Stefan Blom
</pre>
96 5 Stefan Blom
97 1 Stefan Blom
h2. Overview of the Modules of the VerCors Tool set
98 8 Stefan Blom
99 11 Stefan Blom
The VerCors tool set is split into several modules plus scripts to make everything work together. The idea behind the modules is that you can choose between command line and eclipse development for each module independently. For detailed configuration instructions for eclipse see [[Eclipse Setup]].
100 8 Stefan Blom
101 9 Stefan Blom
Next, we will give an overview of the modules. The name of the subdirectory of the module is given between parenthesis.
102 5 Stefan Blom
103 5 Stefan Blom
h3. Hybrid Runtime Environment (hre)
104 5 Stefan Blom
105 5 Stefan Blom
depends on: - 
106 5 Stefan Blom
107 5 Stefan Blom
This module contains functionality that has uses outside of the VerCors toolset.
108 5 Stefan Blom
109 5 Stefan Blom
h3. Core Data Structures (core)
110 5 Stefan Blom
111 5 Stefan Blom
depends on: hre
112 5 Stefan Blom
113 5 Stefan Blom
This module contains the main data structures for the VerCors toolset:
114 5 Stefan Blom
* the Common Object Language (COL) Abstract Syntax Tree.
115 5 Stefan Blom
* Pretty printing framework.
116 5 Stefan Blom
* Visitor Patterns for AST.
117 5 Stefan Blom
118 5 Stefan Blom
h3. Main program (main)
119 1 Stefan Blom
120 14 Stefan Blom
depends on: hre, core, clang
121 5 Stefan Blom
122 5 Stefan Blom
The main program of the VerCors verifier Tool (vct).
123 5 Stefan Blom
124 5 Stefan Blom
h3. Java Parser plugin (java-parser)
125 5 Stefan Blom
126 5 Stefan Blom
depends on: hre, core
127 5 Stefan Blom
128 5 Stefan Blom
Parser for Java, written with the JavaCC 5.0 parser generator.
129 5 Stefan Blom
130 5 Stefan Blom
To compile this parser plugin, you may:
131 5 Stefan Blom
* Perform a command line build using ant.
132 5 Stefan Blom
* Perform an eclipse build using the eclipse ant builder.
133 5 Stefan Blom
* Install and use the JavaCC eclipse plugin.
134 5 Stefan Blom
135 19 Stefan Blom
h3. PVL Parser plugin (pvl-parser) [legacy code]
136 5 Stefan Blom
137 5 Stefan Blom
depends on: hre, core
138 5 Stefan Blom
139 1 Stefan Blom
Parser for PVL (toy language used in the program verification course), written with the ANTLR 3.4 parser generator.
140 1 Stefan Blom
141 1 Stefan Blom
To compile this parser plugin, you may:
142 1 Stefan Blom
* Perform a command line build using ant.
143 1 Stefan Blom
* Perform an eclipse build using the eclipse ant builder.
144 1 Stefan Blom
* Install and use the ANTLR v3 eclipse plugin.
145 19 Stefan Blom
146 19 Stefan Blom
h3. ANTLR4 Parser plugin (antlr4-parser)
147 19 Stefan Blom
148 19 Stefan Blom
depends on: hre, core
149 19 Stefan Blom
150 19 Stefan Blom
Parsers written in ANTLR4 for the following languages:
151 19 Stefan Blom
* PVL (toy language used in the program verification course, extended with openCL kernel syntax).
152 19 Stefan Blom
153 19 Stefan Blom
To compile this parser plugin, you may:
154 19 Stefan Blom
* Perform a command line build using ant.
155 19 Stefan Blom
* Perform an eclipse build using the eclipse ant builder.
156 15 Stefan Blom
157 15 Stefan Blom
h3. CLang Parser plugin (clang-parser)
158 15 Stefan Blom
159 15 Stefan Blom
depends on: hre, core
160 15 Stefan Blom
161 15 Stefan Blom
Parser for C, C++, etc. using the clang/llvm parser.
162 15 Stefan Blom
163 15 Stefan Blom
To compile this parser plugin, you will need to:
164 15 Stefan Blom
* Install clang+llvm version 3.2.
165 15 Stefan Blom
* Configure eclipse to compile this projects.