Merge branch 'public' of gitlab.cristal.univ-lille.fr:otawa-plugins/polymalys into public

README.md

@@ -29,8 +29,6 @@ theory, refer to [1].
 
 * Parma Polyhedra Library (PPL): http://bugseng.com/products/ppl/
 
-* OTAWA 2 (see below)
-
 * For testing, you will need an ARM cross-compiler
 
 First, install all required dependencies. On debian/ubuntu:
@@ -40,34 +38,7 @@ sudo apt install build-essential python2 git cmake flex bison libxml2-dev libxsl
 ```
 
 To prevent compatibility issues, Polymalys is linked to a specific
-version of OTAWA 2. To install that version, run the script
-`otawa-install.py` provided in this directory using python 2.7.
-
-*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`
-
-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
-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>`.
-
-
-## Setting up the environment:
-
-Modify your environment variables as follows:
-
-add `<otawa dir>/bin` to variable `PATH`
-
-add `<otawa dir>/lib:<otawa dir>/lib/otawa/otawa` to variable `LD_LIBRARY_PATH`
-
+version of OTAWA 2, which is bundled in the Polymalys directory.
 
 ## Compiling: 
 
@@ -98,7 +69,7 @@ cd tests
 
 ```
 cd tests
-./poly <binary> # where <binary> is an ARM binary program
+./poly.sh <binary> [<optional function name, defaults to main>] # where <binary> is an ARM binary program
 ```
 
 ## Using in your program:

otawa-patch.diff

-diff --git a/include/otawa/ai/EdgeStore.h b/include/otawa/ai/EdgeStore.h
-index 00678a70..5b1ea8ae 100644
---- a/include/otawa/ai/EdgeStore.h
-+++ b/include/otawa/ai/EdgeStore.h
-@@ -44,16 +44,18 @@ public:
- 	}
- 
- 	void set(vertex_t v, t s) {
--		for(auto e =_graph.succs(v); e; e++)
--			map.put(*e, s);
-+		for(typename G::Successor e(_graph, v); e(); e++)
-+                        map.put(*e, s);
-+
- 	}
- 
- 	inline void set(edge_t e, const t& s) { map.put(e, s); }
- 
- 	t get(vertex_t v) const {
- 		t s = _dom.bot();
--		for(auto e =_graph.succs(v); e; e++)
--			_dom.join(s, map.get(e, _dom.bot()));
-+		for(typename G::Successor e(_graph, v); e(); e++)
-+                        _dom.join(s, map.get(e, _dom.bot()));
-+
- 		return s;
- 	}
- 
-diff --git a/include/otawa/ai/WorkListDriver.h b/include/otawa/ai/WorkListDriver.h
-index 66bee111..2df79da0 100644
---- a/include/otawa/ai/WorkListDriver.h
-+++ b/include/otawa/ai/WorkListDriver.h
-@@ -236,7 +236,7 @@ public:
- 	OrderedDriver(D& dom, const G& graph, S& store, O *order)
- 	: _dom(dom), _graph(graph), _store(store), wl_set(graph.count()), end(false), _order(order) {
- 		store.set(_graph.entry(), dom.init());
--		for(typename G::Successor succ(graph, _graph.entry()); succ; succ++)
-+		for(typename G::Successor succ(graph, _graph.entry()); succ(); succ++)
- 			push(graph.sinkOf(*succ));
- 		next();
- 	}
-@@ -274,7 +274,7 @@ public:
- 	 * (and successors must be updated).
- 	 */
- 	inline void change(void) {
--		for(typename G::Successor succ(_graph, cur); succ; succ++)
-+		for(typename G::Successor succ(_graph, cur); succ(); succ++)
- 			push(*succ);
- 	}
- 
-@@ -354,7 +354,7 @@ public:
- 	 */
- 	inline typename D::t input(vertex_t vertex) {
- 		typename D::t s = _dom.bot();
--		for(typename G::Predecessor pred(_graph, vertex); pred; pred++) {
-+		for(typename G::Predecessor pred(_graph, vertex); pred(); pred++) {
- 			s = _dom.join(s, _store.get(*pred));
- 		}
- 		return s;
-diff --git a/src/oslice/LivenessChecker.cpp b/src/oslice/LivenessChecker.cpp
-index 04dfd02b..c0485aff 100644
---- a/src/oslice/LivenessChecker.cpp
-+++ b/src/oslice/LivenessChecker.cpp
-@@ -61,7 +61,7 @@ LivenessChecker::LivenessChecker(AbstractRegistration& _reg) : otawa::Processor(
- void LivenessChecker::configure(const PropList &props) {
- 	Processor::configure(props);
- 	_debugLevel = LIVENESS_DEBUG_LEVEL(props);
--	LIVENESS_DEBUG_LEVEL(workspace()) = _debugLevel;
-+//	LIVENESS_DEBUG_LEVEL(workspace()) = _debugLevel;
- }
- 
- /**