Merge lp:~verifydtapn-contributers/verifydtapn/win-compile into lp:verifydtapn

Proposed by Jiri Srba
Status: Merged
Approved by: Jiri Srba
Approved revision: 342
Merged at revision: 335
Proposed branch: lp:~verifydtapn-contributers/verifydtapn/win-compile
Merge into: lp:verifydtapn
Diff against target: 314 lines (+91/-40)
9 files modified
makefile.osx32 (+2/-2)
makefile.osx64 (+2/-2)
makefile.win32 (+4/-3)
makefile.win64 (+20/-0)
src/Core/ArgsParser.cpp (+15/-17)
src/Core/ArgsParser.hpp (+2/-3)
src/DiscreteVerification/Util/IntervalOps.cpp (+22/-4)
src/DiscreteVerification/Util/IntervalOps.hpp (+23/-8)
src/DiscreteVerification/VerificationTypes/TimeDartVerification.cpp (+1/-1)
To merge this branch: bzr merge lp:~verifydtapn-contributers/verifydtapn/win-compile
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Review via email: mp+330911@code.launchpad.net

Description of the change

Allows to cross compile for windows.

To post a comment you must log in.
Revision history for this message
Jiri Srba (srba) :
review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'makefile.osx32'
2--- makefile.osx32 2015-05-27 12:24:10 +0000
3+++ makefile.osx32 2017-09-18 13:36:53 +0000
4@@ -8,8 +8,8 @@
5 CUT = cut
6
7 # Compiler and linker flags
8-COMMONFLAGS = -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -O3 -Wall -mtune=core2 -mmacosx-version-min=10.9 -m32
9-CFLAGS = $(COMMONFLAGS) -I. -I -I/usr/local/include -I/opt/local/include -I
10+COMMONFLAGS = -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -O3 -Wall -mtune=core2 -mmacosx-version-min=10.9 -m32 -std=c++14
11+CFLAGS = $(COMMONFLAGS) -I. -I/usr/local/include -I/opt/local/include
12 LDFLAGS = $(COMMONFLAGS) -lstdc++
13
14 # Input files
15
16=== modified file 'makefile.osx64'
17--- makefile.osx64 2015-05-27 12:24:10 +0000
18+++ makefile.osx64 2017-09-18 13:36:53 +0000
19@@ -8,8 +8,8 @@
20 CUT = cut
21
22 # Compiler and linker flags
23-COMMONFLAGS = -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -O3 -Wall -mtune=core2 -mmacosx-version-min=10.9 -m64
24-CFLAGS = $(COMMONFLAGS) -I. -I -I/usr/local/include -I/opt/local/include -I
25+COMMONFLAGS = -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -O3 -Wall -mtune=core2 -mmacosx-version-min=10.9 -m64 -std=c++14
26+CFLAGS = $(COMMONFLAGS) -I. -I/usr/local/include -I/opt/local/include -I/usr/local/
27 LDFLAGS = $(COMMONFLAGS) -lstdc++
28
29 # Input files
30
31=== modified file 'makefile.win32'
32--- makefile.win32 2014-08-07 21:45:35 +0000
33+++ makefile.win32 2017-09-18 13:36:53 +0000
34@@ -8,12 +8,13 @@
35 CUT = cut
36
37 # Compiler and linker flags
38-CFLAGS = -static -static-libgcc -static-libstdc++ -O3 -L. -Wl,--enable-stdcall-fixup -I ${HOME}/dev/iaw32/include -I
39-LDFLAGS = -static -static-libgcc -static-libstdc++ -O3 -L. -Wl,--enable-stdcall-fixup -I ${HOME}/dev/iaw32/include -I
40+CFLAGS = -flto -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -static -static -static-libgcc -static-libstdc++ -Wall -I../iaw32
41+
42+LDFLAGS = -flto=4 -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -static -static -static-libgcc -static-libstdc++ -Wall
43
44 # Input files
45 SOURCES = $(shell find * -name "*.cpp")
46 OBJECTS = $(SOURCES:.cpp=.o)
47-TARGET = verifydtapn-win32.exe
48+TARGET = verifydtapn-win32
49
50 include rules.mk
51
52=== added file 'makefile.win64'
53--- makefile.win64 1970-01-01 00:00:00 +0000
54+++ makefile.win64 2017-09-18 13:36:53 +0000
55@@ -0,0 +1,20 @@
56+# For bash on OS X, as /bin/sh is compiled with --enable-strict-posix-default
57+SHELL = /bin/bash
58+
59+# Programs for processing
60+LEX = flex
61+YACC = bison
62+CC = x86_64-w64-mingw32-g++
63+CUT = cut
64+
65+# Compiler and linker flags
66+CFLAGS = -flto -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -static -static -static-libgcc -static-libstdc++ -Wall -I../iaw64
67+
68+LDFLAGS = -flto=4 -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -static -static -static-libgcc -static-libstdc++ -Wall
69+
70+# Input files
71+SOURCES = $(shell find * -name "*.cpp")
72+OBJECTS = $(SOURCES:.cpp=.o)
73+TARGET = verifydtapn-win64
74+
75+include rules.mk
76
77=== modified file 'src/Core/ArgsParser.cpp'
78--- src/Core/ArgsParser.cpp 2015-06-24 13:25:59 +0000
79+++ src/Core/ArgsParser.cpp 2017-09-18 13:36:53 +0000
80@@ -3,7 +3,6 @@
81 #include <sstream>
82 #include "boost/algorithm/string.hpp"
83 #include "boost/lexical_cast.hpp"
84-#include "boost/make_shared.hpp"
85 #include <iomanip>
86 #include "boost/tokenizer.hpp"
87
88@@ -135,52 +134,52 @@
89 // Each line in the description is assumed to fit within the remaining width
90 // of the console, so keep descriptions short, or implement manual word-wrapping :).
91 parsers.push_back(
92- boost::make_shared<SwitchWithArg > ("k", KBOUND_OPTION,
93+ new SwitchWithArg ("k", KBOUND_OPTION,
94 "Max tokens to use during exploration.", 0));
95 parsers.push_back(
96- boost::make_shared<SwitchWithArg > ("o", SEARCH_OPTION,
97+ new SwitchWithArg ("o", SEARCH_OPTION,
98 "Specify the desired search strategy.\n - 0: Breadth-First Search\n - 1: Depth-First Search\n - 2: Random Search\n - 3: Heuristic Search\n - 4: Default",
99 4));
100 parsers.push_back(
101- boost::make_shared<SwitchWithArg > ("m", VERIFICATION_OPTION,
102+ new SwitchWithArg ("m", VERIFICATION_OPTION,
103 "Specify the desired verification method.\n - 0: Default (discrete)\n - 1: Time Darts",
104 0));
105 parsers.push_back(
106- boost::make_shared<SwitchWithArg > ("p", MEMORY_OPTIMIZATION_OPTION,
107+ new SwitchWithArg ("p", MEMORY_OPTIMIZATION_OPTION,
108 "Specify the desired memory optimization.\n - 0: None \n - 1: PTrie",
109 0));
110 parsers.push_back(
111- boost::make_shared<SwitchWithArg > ("t", TRACE_OPTION,
112+ new SwitchWithArg ("t", TRACE_OPTION,
113 "Specify the desired trace option.\n - 0: none\n - 1: some\n - 2: fastest",
114 0));
115 parsers.push_back(
116- boost::make_shared<Switch > ("d", KEEP_DEAD,
117+ new Switch ("d", KEEP_DEAD,
118 "Do not discard dead tokens\n(used for boundedness checking)"));
119 parsers.push_back(
120- boost::make_shared<Switch > ("g", MAX_CONSTANT_OPTION,
121+ new Switch ("g", MAX_CONSTANT_OPTION,
122 "Use global maximum constant for \nextrapolation (as opposed to local \nconstants)."));
123 parsers.push_back(
124- boost::make_shared<Switch > ("s", LEGACY,
125+ new Switch ("s", LEGACY,
126 "Legacy option (no effect)."));
127
128 parsers.push_back(
129- boost::make_shared<Switch > ("x", XML_TRACE_OPTION,
130+ new Switch ("x", XML_TRACE_OPTION,
131 "Output trace in xml format for TAPAAL."));
132
133 parsers.push_back(
134- boost::make_shared<Switch >("c", GCD,
135+ new Switch("c", GCD,
136 "Enable lowering the guards by the greatest common divisor"));
137
138 parsers.push_back(
139- boost::make_shared<SwitchWithArg > ("w", WORKFLOW,
140+ new SwitchWithArg ("w", WORKFLOW,
141 "Workflow mode.\n - 0: Disabled\n - 1: Soundness (and min)\n - 2: Strong Soundness (and max)",
142 0));
143 parsers.push_back(
144- boost::make_shared<SwitchWithArg > ("b", STRONG_WORKFLOW_BOUND,
145+ new SwitchWithArg ("b", STRONG_WORKFLOW_BOUND,
146 "Maximum delay bound for strong workflow analysis",
147 0));
148 parsers.push_back(
149- boost::make_shared<Switch> ("n", CALCULATE_CMAX,
150+ new Switch ("n", CALCULATE_CMAX,
151 "Calculate the place bounds"));
152
153 };
154@@ -194,9 +193,8 @@
155 << "Displays this help message." << std::endl;
156 std::cout << std::setw(WIDTH) << std::left << "-v [ --version ]"
157 << "Displays version information." << std::endl;
158- for (parser_vec::const_iterator arg = parsers.begin(); arg != parsers.end();
159- arg++) {
160- std::cout << **arg;
161+ for (auto& p : parsers) {
162+ std::cout << *p;
163 }
164 }
165 ;
166
167=== modified file 'src/Core/ArgsParser.hpp'
168--- src/Core/ArgsParser.hpp 2015-08-31 12:42:10 +0000
169+++ src/Core/ArgsParser.hpp 2017-09-18 13:36:53 +0000
170@@ -5,7 +5,6 @@
171 #include <map>
172 #include <string>
173 #include <iosfwd>
174-#include "boost/smart_ptr.hpp"
175 #include "VerificationOptions.hpp"
176 #include "boost/lexical_cast.hpp"
177
178@@ -78,10 +77,10 @@
179 };
180
181 class ArgsParser {
182- typedef std::vector< boost::shared_ptr<Switch> > parser_vec;
183+ typedef std::vector< Switch* > parser_vec;
184 public:
185 ArgsParser() : parsers(), version(3,2,0) { initialize(); };
186- virtual ~ArgsParser() {};
187+ virtual ~ArgsParser() { for( auto p : parsers) delete p; };
188
189 VerificationOptions parse(int argc, char* argv[]) const;
190 private:
191
192=== modified file 'src/DiscreteVerification/Util/IntervalOps.cpp'
193--- src/DiscreteVerification/Util/IntervalOps.cpp 2013-04-23 10:51:59 +0000
194+++ src/DiscreteVerification/Util/IntervalOps.cpp 2017-09-18 13:36:53 +0000
195@@ -12,7 +12,6 @@
196 namespace Util {
197
198 using namespace std;
199-using namespace boost::numeric;
200
201 vector<interval > setIntersection(const vector<interval >& first, const vector<interval >& second){
202 vector<interval > result;
203@@ -29,7 +28,7 @@
204
205 interval intersection = intersect(first.at(i), second.at(j));
206
207- if(!empty(intersection)){
208+ if(!intersection.empty()){
209 result.push_back(intersection);
210 }
211
212@@ -44,6 +43,25 @@
213 return result;
214 }
215
216+interval intersect(const interval& l, const interval r)
217+{
218+ if(l.empty()) return l;
219+ if(r.empty()) return r;
220+ interval n(std::max(l.low, r.low), std::min(l.high, r.high));
221+ return n;
222+}
223+
224+interval hull(const interval& l, const interval r)
225+{
226+ return interval(std::min(l.low, r.low), std::max(l.high, r.high));
227+}
228+
229+bool overlap(const interval& l, const interval r)
230+{
231+ auto i = intersect(l, r);
232+ return !i.empty();
233+}
234+
235 void setAdd(vector< interval >& first, const interval& element){
236
237 for(unsigned int i = 0; i < first.size(); i++){
238@@ -55,13 +73,13 @@
239 } else if(overlap(element, first.at(i))){
240 interval u = hull(element, first.at(i));
241 // Merge with node
242- first.at(i).assign(u.lower(), u.upper());
243+ first[i] = u;
244 // Clean up
245 for(i++; i < first.size(); i++){
246 if(first.at(i).lower() <= u.upper()){
247 // Merge items
248 if(first.at(i).upper() > u.upper()){
249- first.at(i-1).assign(first.at(i-1).lower(), first.at(i).upper());
250+ first[i-1] = interval(first.at(i-1).lower(), first.at(i).upper());
251 }
252 first.erase(first.begin()+i);
253 i--;
254
255=== modified file 'src/DiscreteVerification/Util/IntervalOps.hpp'
256--- src/DiscreteVerification/Util/IntervalOps.hpp 2013-04-23 10:51:59 +0000
257+++ src/DiscreteVerification/Util/IntervalOps.hpp 2017-09-18 13:36:53 +0000
258@@ -9,20 +9,35 @@
259 #define INTERVALOPS_HPP_
260
261 #include <vector>
262-#include "boost/numeric/interval.hpp"
263+#include <limits>
264
265 namespace VerifyTAPN {
266 namespace DiscreteVerification {
267 namespace Util {
268
269-typedef boost::numeric::interval_lib::rounded_math< int > rounding_policy;
270-typedef boost::numeric::interval_lib::checking_no_nan< int > checking_policy;
271-typedef boost::numeric::interval_lib::policies< rounding_policy, checking_policy > interval_policies;
272-typedef boost::numeric::interval< int, interval_policies > interval;
273+ struct interval {
274+ int low, high;
275+ interval(int l, int h) : low(l), high(h)
276+ {
277+ if(low > high)
278+ {
279+ low = std::numeric_limits<int>::max();
280+ high = std::numeric_limits<int>::min();
281+ }
282+ };
283+ auto upper() const {return high; }
284+ auto lower() const {return low; }
285+ auto empty() const { return high < low; }
286+ };
287
288-void setAdd(std::vector< interval >& first, const interval& element);
289-std::vector<interval > setIntersection(const std::vector<interval >& first,
290- const std::vector<interval >& second);
291+ interval intersect(const interval& l, const interval r);
292+ interval hull(const interval& l, const interval r);
293+ bool overlap(const interval& l, const interval r);
294+
295+
296+ void setAdd(std::vector< interval >& first, const interval& element);
297+ std::vector<interval > setIntersection(const std::vector<interval >& first,
298+ const std::vector<interval >& second);
299
300 } /* namespace Util */
301 } /* namespace DiscreteVerification */
302
303=== modified file 'src/DiscreteVerification/VerificationTypes/TimeDartVerification.cpp'
304--- src/DiscreteVerification/VerificationTypes/TimeDartVerification.cpp 2015-08-18 08:10:19 +0000
305+++ src/DiscreteVerification/VerificationTypes/TimeDartVerification.cpp 2017-09-18 13:36:53 +0000
306@@ -88,7 +88,7 @@
307 Util::interval arcGuard((*arc)->getInterval().getLowerBound(), (*arc)->getInterval().getUpperBound());
308 Util::interval invGuard(0, (*arc)->getDestination().getInvariant().getBound());
309
310- Util::interval arcInterval = boost::numeric::intersect(arcGuard, invGuard);
311+ Util::interval arcInterval = Util::intersect(arcGuard, invGuard);
312 vector<Util::interval > intervals;
313 int range;
314 if (arcInterval.upper() == INT_MAX) {

Subscribers

People subscribed via source and target branches