VerifyDTAPN

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

  1. win-compile
  2. Merge into trunk
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
=== modified file 'makefile.osx32'
--- makefile.osx32 2015-05-27 12:24:10 +0000
+++ makefile.osx32 2017-09-18 13:36:53 +0000
@@ -8,8 +8,8 @@
8CUT = cut8CUT = cut
99
10# Compiler and linker flags10# Compiler and linker flags
11COMMONFLAGS = -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -O3 -Wall -mtune=core2 -mmacosx-version-min=10.9 -m3211COMMONFLAGS = -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -O3 -Wall -mtune=core2 -mmacosx-version-min=10.9 -m32 -std=c++14
12CFLAGS = $(COMMONFLAGS) -I. -I -I/usr/local/include -I/opt/local/include -I 12CFLAGS = $(COMMONFLAGS) -I. -I/usr/local/include -I/opt/local/include
13LDFLAGS = $(COMMONFLAGS) -lstdc++ 13LDFLAGS = $(COMMONFLAGS) -lstdc++
1414
15# Input files15# Input files
1616
=== modified file 'makefile.osx64'
--- makefile.osx64 2015-05-27 12:24:10 +0000
+++ makefile.osx64 2017-09-18 13:36:53 +0000
@@ -8,8 +8,8 @@
8CUT = cut8CUT = cut
99
10# Compiler and linker flags10# Compiler and linker flags
11COMMONFLAGS = -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -O3 -Wall -mtune=core2 -mmacosx-version-min=10.9 -m6411COMMONFLAGS = -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -O3 -Wall -mtune=core2 -mmacosx-version-min=10.9 -m64 -std=c++14
12CFLAGS = $(COMMONFLAGS) -I. -I -I/usr/local/include -I/opt/local/include -I 12CFLAGS = $(COMMONFLAGS) -I. -I/usr/local/include -I/opt/local/include -I/usr/local/
13LDFLAGS = $(COMMONFLAGS) -lstdc++ 13LDFLAGS = $(COMMONFLAGS) -lstdc++
1414
15# Input files15# Input files
1616
=== modified file 'makefile.win32'
--- makefile.win32 2014-08-07 21:45:35 +0000
+++ makefile.win32 2017-09-18 13:36:53 +0000
@@ -8,12 +8,13 @@
8CUT = cut8CUT = cut
99
10# Compiler and linker flags10# Compiler and linker flags
11CFLAGS = -static -static-libgcc -static-libstdc++ -O3 -L. -Wl,--enable-stdcall-fixup -I ${HOME}/dev/iaw32/include -I11CFLAGS = -flto -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -static -static -static-libgcc -static-libstdc++ -Wall -I../iaw32
12LDFLAGS = -static -static-libgcc -static-libstdc++ -O3 -L. -Wl,--enable-stdcall-fixup -I ${HOME}/dev/iaw32/include -I 12
13LDFLAGS = -flto=4 -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -static -static -static-libgcc -static-libstdc++ -Wall
1314
14# Input files15# Input files
15SOURCES = $(shell find * -name "*.cpp") 16SOURCES = $(shell find * -name "*.cpp")
16OBJECTS = $(SOURCES:.cpp=.o)17OBJECTS = $(SOURCES:.cpp=.o)
17TARGET = verifydtapn-win32.exe18TARGET = verifydtapn-win32
1819
19include rules.mk20include rules.mk
2021
=== added file 'makefile.win64'
--- makefile.win64 1970-01-01 00:00:00 +0000
+++ makefile.win64 2017-09-18 13:36:53 +0000
@@ -0,0 +1,20 @@
1# For bash on OS X, as /bin/sh is compiled with --enable-strict-posix-default
2SHELL = /bin/bash
3
4# Programs for processing
5LEX = flex
6YACC = bison
7CC = x86_64-w64-mingw32-g++
8CUT = cut
9
10# Compiler and linker flags
11CFLAGS = -flto -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -static -static -static-libgcc -static-libstdc++ -Wall -I../iaw64
12
13LDFLAGS = -flto=4 -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -static -static -static-libgcc -static-libstdc++ -Wall
14
15# Input files
16SOURCES = $(shell find * -name "*.cpp")
17OBJECTS = $(SOURCES:.cpp=.o)
18TARGET = verifydtapn-win64
19
20include rules.mk
021
=== modified file 'src/Core/ArgsParser.cpp'
--- src/Core/ArgsParser.cpp 2015-06-24 13:25:59 +0000
+++ src/Core/ArgsParser.cpp 2017-09-18 13:36:53 +0000
@@ -3,7 +3,6 @@
3#include <sstream>3#include <sstream>
4#include "boost/algorithm/string.hpp"4#include "boost/algorithm/string.hpp"
5#include "boost/lexical_cast.hpp"5#include "boost/lexical_cast.hpp"
6#include "boost/make_shared.hpp"
7#include <iomanip>6#include <iomanip>
8#include "boost/tokenizer.hpp"7#include "boost/tokenizer.hpp"
98
@@ -135,52 +134,52 @@
135 // Each line in the description is assumed to fit within the remaining width134 // Each line in the description is assumed to fit within the remaining width
136 // of the console, so keep descriptions short, or implement manual word-wrapping :).135 // of the console, so keep descriptions short, or implement manual word-wrapping :).
137 parsers.push_back(136 parsers.push_back(
138 boost::make_shared<SwitchWithArg > ("k", KBOUND_OPTION,137 new SwitchWithArg ("k", KBOUND_OPTION,
139 "Max tokens to use during exploration.", 0));138 "Max tokens to use during exploration.", 0));
140 parsers.push_back(139 parsers.push_back(
141 boost::make_shared<SwitchWithArg > ("o", SEARCH_OPTION,140 new SwitchWithArg ("o", SEARCH_OPTION,
142 "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",141 "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",
143 4));142 4));
144 parsers.push_back(143 parsers.push_back(
145 boost::make_shared<SwitchWithArg > ("m", VERIFICATION_OPTION,144 new SwitchWithArg ("m", VERIFICATION_OPTION,
146 "Specify the desired verification method.\n - 0: Default (discrete)\n - 1: Time Darts",145 "Specify the desired verification method.\n - 0: Default (discrete)\n - 1: Time Darts",
147 0));146 0));
148 parsers.push_back(147 parsers.push_back(
149 boost::make_shared<SwitchWithArg > ("p", MEMORY_OPTIMIZATION_OPTION,148 new SwitchWithArg ("p", MEMORY_OPTIMIZATION_OPTION,
150 "Specify the desired memory optimization.\n - 0: None \n - 1: PTrie",149 "Specify the desired memory optimization.\n - 0: None \n - 1: PTrie",
151 0)); 150 0));
152 parsers.push_back(151 parsers.push_back(
153 boost::make_shared<SwitchWithArg > ("t", TRACE_OPTION,152 new SwitchWithArg ("t", TRACE_OPTION,
154 "Specify the desired trace option.\n - 0: none\n - 1: some\n - 2: fastest",153 "Specify the desired trace option.\n - 0: none\n - 1: some\n - 2: fastest",
155 0));154 0));
156 parsers.push_back(155 parsers.push_back(
157 boost::make_shared<Switch > ("d", KEEP_DEAD,156 new Switch ("d", KEEP_DEAD,
158 "Do not discard dead tokens\n(used for boundedness checking)"));157 "Do not discard dead tokens\n(used for boundedness checking)"));
159 parsers.push_back(158 parsers.push_back(
160 boost::make_shared<Switch > ("g", MAX_CONSTANT_OPTION,159 new Switch ("g", MAX_CONSTANT_OPTION,
161 "Use global maximum constant for \nextrapolation (as opposed to local \nconstants)."));160 "Use global maximum constant for \nextrapolation (as opposed to local \nconstants)."));
162 parsers.push_back(161 parsers.push_back(
163 boost::make_shared<Switch > ("s", LEGACY,162 new Switch ("s", LEGACY,
164 "Legacy option (no effect)."));163 "Legacy option (no effect)."));
165164
166 parsers.push_back(165 parsers.push_back(
167 boost::make_shared<Switch > ("x", XML_TRACE_OPTION,166 new Switch ("x", XML_TRACE_OPTION,
168 "Output trace in xml format for TAPAAL."));167 "Output trace in xml format for TAPAAL."));
169168
170 parsers.push_back(169 parsers.push_back(
171 boost::make_shared<Switch >("c", GCD,170 new Switch("c", GCD,
172 "Enable lowering the guards by the greatest common divisor"));171 "Enable lowering the guards by the greatest common divisor"));
173 172
174 parsers.push_back(173 parsers.push_back(
175 boost::make_shared<SwitchWithArg > ("w", WORKFLOW,174 new SwitchWithArg ("w", WORKFLOW,
176 "Workflow mode.\n - 0: Disabled\n - 1: Soundness (and min)\n - 2: Strong Soundness (and max)",175 "Workflow mode.\n - 0: Disabled\n - 1: Soundness (and min)\n - 2: Strong Soundness (and max)",
177 0));176 0));
178 parsers.push_back(177 parsers.push_back(
179 boost::make_shared<SwitchWithArg > ("b", STRONG_WORKFLOW_BOUND,178 new SwitchWithArg ("b", STRONG_WORKFLOW_BOUND,
180 "Maximum delay bound for strong workflow analysis",179 "Maximum delay bound for strong workflow analysis",
181 0));180 0));
182 parsers.push_back(181 parsers.push_back(
183 boost::make_shared<Switch> ("n", CALCULATE_CMAX,182 new Switch ("n", CALCULATE_CMAX,
184 "Calculate the place bounds"));183 "Calculate the place bounds"));
185184
186 };185 };
@@ -194,9 +193,8 @@
194 << "Displays this help message." << std::endl;193 << "Displays this help message." << std::endl;
195 std::cout << std::setw(WIDTH) << std::left << "-v [ --version ]"194 std::cout << std::setw(WIDTH) << std::left << "-v [ --version ]"
196 << "Displays version information." << std::endl;195 << "Displays version information." << std::endl;
197 for (parser_vec::const_iterator arg = parsers.begin(); arg != parsers.end();196 for (auto& p : parsers) {
198 arg++) {197 std::cout << *p;
199 std::cout << **arg;
200 }198 }
201}199}
202;200;
203201
=== modified file 'src/Core/ArgsParser.hpp'
--- src/Core/ArgsParser.hpp 2015-08-31 12:42:10 +0000
+++ src/Core/ArgsParser.hpp 2017-09-18 13:36:53 +0000
@@ -5,7 +5,6 @@
5#include <map>5#include <map>
6#include <string>6#include <string>
7#include <iosfwd>7#include <iosfwd>
8#include "boost/smart_ptr.hpp"
9#include "VerificationOptions.hpp"8#include "VerificationOptions.hpp"
10#include "boost/lexical_cast.hpp"9#include "boost/lexical_cast.hpp"
1110
@@ -78,10 +77,10 @@
78 };77 };
7978
80 class ArgsParser {79 class ArgsParser {
81 typedef std::vector< boost::shared_ptr<Switch> > parser_vec;80 typedef std::vector< Switch* > parser_vec;
82 public:81 public:
83 ArgsParser() : parsers(), version(3,2,0) { initialize(); };82 ArgsParser() : parsers(), version(3,2,0) { initialize(); };
84 virtual ~ArgsParser() {};83 virtual ~ArgsParser() { for( auto p : parsers) delete p; };
8584
86 VerificationOptions parse(int argc, char* argv[]) const;85 VerificationOptions parse(int argc, char* argv[]) const;
87 private:86 private:
8887
=== modified file 'src/DiscreteVerification/Util/IntervalOps.cpp'
--- src/DiscreteVerification/Util/IntervalOps.cpp 2013-04-23 10:51:59 +0000
+++ src/DiscreteVerification/Util/IntervalOps.cpp 2017-09-18 13:36:53 +0000
@@ -12,7 +12,6 @@
12namespace Util {12namespace Util {
1313
14using namespace std;14using namespace std;
15using namespace boost::numeric;
1615
17vector<interval > setIntersection(const vector<interval >& first, const vector<interval >& second){16vector<interval > setIntersection(const vector<interval >& first, const vector<interval >& second){
18 vector<interval > result;17 vector<interval > result;
@@ -29,7 +28,7 @@
2928
30 interval intersection = intersect(first.at(i), second.at(j));29 interval intersection = intersect(first.at(i), second.at(j));
3130
32 if(!empty(intersection)){31 if(!intersection.empty()){
33 result.push_back(intersection);32 result.push_back(intersection);
34 }33 }
3534
@@ -44,6 +43,25 @@
44 return result;43 return result;
45}44}
4645
46interval intersect(const interval& l, const interval r)
47{
48 if(l.empty()) return l;
49 if(r.empty()) return r;
50 interval n(std::max(l.low, r.low), std::min(l.high, r.high));
51 return n;
52}
53
54interval hull(const interval& l, const interval r)
55{
56 return interval(std::min(l.low, r.low), std::max(l.high, r.high));
57}
58
59bool overlap(const interval& l, const interval r)
60{
61 auto i = intersect(l, r);
62 return !i.empty();
63}
64
47void setAdd(vector< interval >& first, const interval& element){65void setAdd(vector< interval >& first, const interval& element){
4866
49 for(unsigned int i = 0; i < first.size(); i++){67 for(unsigned int i = 0; i < first.size(); i++){
@@ -55,13 +73,13 @@
55 } else if(overlap(element, first.at(i))){73 } else if(overlap(element, first.at(i))){
56 interval u = hull(element, first.at(i));74 interval u = hull(element, first.at(i));
57 // Merge with node75 // Merge with node
58 first.at(i).assign(u.lower(), u.upper());76 first[i] = u;
59 // Clean up77 // Clean up
60 for(i++; i < first.size(); i++){78 for(i++; i < first.size(); i++){
61 if(first.at(i).lower() <= u.upper()){79 if(first.at(i).lower() <= u.upper()){
62 // Merge items80 // Merge items
63 if(first.at(i).upper() > u.upper()){81 if(first.at(i).upper() > u.upper()){
64 first.at(i-1).assign(first.at(i-1).lower(), first.at(i).upper());82 first[i-1] = interval(first.at(i-1).lower(), first.at(i).upper());
65 }83 }
66 first.erase(first.begin()+i);84 first.erase(first.begin()+i);
67 i--;85 i--;
6886
=== modified file 'src/DiscreteVerification/Util/IntervalOps.hpp'
--- src/DiscreteVerification/Util/IntervalOps.hpp 2013-04-23 10:51:59 +0000
+++ src/DiscreteVerification/Util/IntervalOps.hpp 2017-09-18 13:36:53 +0000
@@ -9,20 +9,35 @@
9#define INTERVALOPS_HPP_9#define INTERVALOPS_HPP_
1010
11#include <vector>11#include <vector>
12#include "boost/numeric/interval.hpp"12#include <limits>
1313
14namespace VerifyTAPN {14namespace VerifyTAPN {
15namespace DiscreteVerification {15namespace DiscreteVerification {
16namespace Util {16namespace Util {
1717
18typedef boost::numeric::interval_lib::rounded_math< int > rounding_policy;18 struct interval {
19typedef boost::numeric::interval_lib::checking_no_nan< int > checking_policy;19 int low, high;
20typedef boost::numeric::interval_lib::policies< rounding_policy, checking_policy > interval_policies;20 interval(int l, int h) : low(l), high(h)
21typedef boost::numeric::interval< int, interval_policies > interval;21 {
22 if(low > high)
23 {
24 low = std::numeric_limits<int>::max();
25 high = std::numeric_limits<int>::min();
26 }
27 };
28 auto upper() const {return high; }
29 auto lower() const {return low; }
30 auto empty() const { return high < low; }
31 };
2232
23void setAdd(std::vector< interval >& first, const interval& element);33 interval intersect(const interval& l, const interval r);
24std::vector<interval > setIntersection(const std::vector<interval >& first,34 interval hull(const interval& l, const interval r);
25 const std::vector<interval >& second);35 bool overlap(const interval& l, const interval r);
36
37
38 void setAdd(std::vector< interval >& first, const interval& element);
39 std::vector<interval > setIntersection(const std::vector<interval >& first,
40 const std::vector<interval >& second);
2641
27} /* namespace Util */42} /* namespace Util */
28} /* namespace DiscreteVerification */43} /* namespace DiscreteVerification */
2944
=== modified file 'src/DiscreteVerification/VerificationTypes/TimeDartVerification.cpp'
--- src/DiscreteVerification/VerificationTypes/TimeDartVerification.cpp 2015-08-18 08:10:19 +0000
+++ src/DiscreteVerification/VerificationTypes/TimeDartVerification.cpp 2017-09-18 13:36:53 +0000
@@ -88,7 +88,7 @@
88 Util::interval arcGuard((*arc)->getInterval().getLowerBound(), (*arc)->getInterval().getUpperBound());88 Util::interval arcGuard((*arc)->getInterval().getLowerBound(), (*arc)->getInterval().getUpperBound());
89 Util::interval invGuard(0, (*arc)->getDestination().getInvariant().getBound());89 Util::interval invGuard(0, (*arc)->getDestination().getInvariant().getBound());
9090
91 Util::interval arcInterval = boost::numeric::intersect(arcGuard, invGuard);91 Util::interval arcInterval = Util::intersect(arcGuard, invGuard);
92 vector<Util::interval > intervals;92 vector<Util::interval > intervals;
93 int range;93 int range;
94 if (arcInterval.upper() == INT_MAX) {94 if (arcInterval.upper() == INT_MAX) {

Subscribers

People subscribed via source and target branches