Commit 49738a6d authored by Ballabriga Clément's avatar Ballabriga Clément
Browse files

update doc

parent 24fb1deb
# Polymalys
Requirements:
=============
## Requirements
a) Parma Polyhedra Library (PPL): http://bugseng.com/products/ppl/
* Parma Polyhedra Library (PPL): http://bugseng.com/products/ppl/
b) Having otawa-config in $PATH: export PATH=$PATH:/path/to/otawa/binaries/
* Having otawa-config in $PATH: export PATH=$PATH:/path/to/otawa/binaries/
c) Having otawa lib dir in $LD_LIBRARY_PATH: export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:$(otawa-config --libdir)
* Having otawa lib dir in $LD_LIBRARY_PATH: export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:$(otawa-config --libdir)
d) For testing, you will need an ARM cross-compiler
* For testing, you will need an ARM cross-compiler
e) OTAWA 2
* OTAWA 2
First, install all required dependencies. On debian/ubuntu:
```
sudo apt install build-essential python2 git cmake flex bison libxml2-dev libxslt-dev ocaml gcc-arm-none-eabi
```
To download and install OTAWA v2, first download the following script
and execute it using python 2.7:
```
http://www.tracesgroup.net/otawa/packages/otawa-install.py
Warning: the script is compatible with python 2.7 (NOT python 3). If
```
*Warning*: the script is compatible with python 2.7 (NOT python 3). If
your default python installation is python3, you need to edit the first
line of otawa-install.py and replace #!/usr/bin/python by
#!/usr/bin/python2
line of `otawa-install.py` and replace `#!/usr/bin/python` by
`#!/usr/bin/python2`
You will also need to install the OTAWA plugins for ARM, and
lp-solve. Go to <otawa dir>/bin (where otawa dir is the directory
lp-solve. Go to `<otawa dir>/bin` (where otawa dir is the directory
where you just installed otawa) and type:
```
python otawa-install.py otawa-arm otawa-lp_solve5
```
Warning: to install plugins, do not use otawa-install.py in
<otawa_dir>.
*Warning*: to install plugins, do not use `otawa-install.py` in
`<otawa_dir>`.
Setting up the environment:
===========================
## Setting up the environment:
Modify your environment variables as follows:
add <otawa dir>/bin to variable PATH
add `<otawa dir>/bin` to variable `PATH`
add <otawa dir>/lib to variable LD_LIBRARY_PATH
add `<otawa dir>/lib` to variable `LD_LIBRARY_PATH`
Compiling:
==========
## Compiling:
```
make
```
# Installing (in home directory, no root required):
Installing (in home directory, no root required):
=================================================
```
make install
```
## Automated tests
Automated tests:
================
```
make test
```
## Testing with a source code target program:
Testing with a source code target program:
==========================================
```
cd tests
./do.sh <filename> # where <filename>.c is a C program
```
# Testing with a binary target program:
Testing with a binary target program:
=====================================
```
cd tests
./poly <binary> # where <binary> is an ARM binary program
```
## Using in your program:
Using in your program:
======================
Read tests/poly.cpp
Read `tests/poly.cpp`
Known limitations (future works):
=================================
## Known limitations (future works):
- No modular inter-procedural analysis
- No support for integer wrap/overflow
- Loops with equality (instead of inequality) in loop condition will have pessimistic bounds
- We assume that each memory access has 32bits-size, and is 32bits-aligned
- Lots of speed optimization needs to be done
* No modular inter-procedural analysis
* No support for integer wrap/overflow
* Loops with equality (instead of inequality) in loop condition will have pessimistic bounds
* We assume that each memory access has 32bits-size, and is 32bits-aligned
* Lots of speed optimization needs to be done
Questions:
==========
## Questions:
mail: Clement.Ballabriga@univ-lille1.fr
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment