diff --git a/README.md b/README.md index 3b6a0c25e6335f89687462303fe1a0ef361be8f0..78e883d3cba7c10661319832f1d46a533d899de9 100644 --- a/README.md +++ b/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: diff --git a/otawa-patch.diff b/otawa-patch.diff deleted file mode 100644 index 484fa3428303e25c78989e0ae7a80ee961aabcb9..0000000000000000000000000000000000000000 --- a/otawa-patch.diff +++ /dev/null @@ -1,71 +0,0 @@ -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; - } - - /**