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

[Jiri Srba]

Allows to cross compile for windows.

[Jiri Srba (srba)]

review: Approve

=== 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 @@
 CUT				= cut
 
 # Compiler and linker flags
-COMMONFLAGS             = -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -O3 -Wall -mtune=core2 -mmacosx-version-min=10.9 -m32
-CFLAGS                  = $(COMMONFLAGS) -I. -I -I/usr/local/include -I/opt/local/include -I 
+COMMONFLAGS             = -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -O3 -Wall -mtune=core2 -mmacosx-version-min=10.9 -m32 -std=c++14
+CFLAGS                  = $(COMMONFLAGS) -I. -I/usr/local/include -I/opt/local/include 
 LDFLAGS                 = $(COMMONFLAGS) -lstdc++ 
 
 # Input files

=== 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 @@
 CUT				= cut
 
 # Compiler and linker flags
-COMMONFLAGS 		= -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -O3 -Wall -mtune=core2 -mmacosx-version-min=10.9 -m64
-CFLAGS			= $(COMMONFLAGS) -I. -I -I/usr/local/include -I/opt/local/include -I 
+COMMONFLAGS 		= -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -O3 -Wall -mtune=core2 -mmacosx-version-min=10.9 -m64 -std=c++14
+CFLAGS			= $(COMMONFLAGS) -I. -I/usr/local/include -I/opt/local/include -I/usr/local/ 
 LDFLAGS			= $(COMMONFLAGS) -lstdc++ 
 
 # Input files

=== 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 @@
 CUT				= cut
 
 # Compiler and linker flags
-CFLAGS			= -static -static-libgcc -static-libstdc++ -O3 -L. -Wl,--enable-stdcall-fixup -I ${HOME}/dev/iaw32/include -I
-LDFLAGS			= -static -static-libgcc -static-libstdc++ -O3 -L. -Wl,--enable-stdcall-fixup -I ${HOME}/dev/iaw32/include -I 
+CFLAGS 			= -flto -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -static -static -static-libgcc -static-libstdc++ -Wall -I../iaw32
+
+LDFLAGS 		= -flto=4 -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -static -static -static-libgcc -static-libstdc++ -Wall 
 
 # Input files
 SOURCES			= $(shell find * -name "*.cpp")	
 OBJECTS			= $(SOURCES:.cpp=.o)
-TARGET			= verifydtapn-win32.exe
+TARGET			= verifydtapn-win32
 
 include rules.mk

=== 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 @@
+# For bash on OS X, as /bin/sh is compiled with --enable-strict-posix-default
+SHELL    		= /bin/bash
+
+# Programs for processing
+LEX				= flex 
+YACC				= bison 
+CC				= x86_64-w64-mingw32-g++ 
+CUT				= cut
+
+# Compiler and linker flags
+CFLAGS 			= -flto -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -static -static -static-libgcc -static-libstdc++ -Wall -I../iaw64
+
+LDFLAGS 		= -flto=4 -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -static -static -static-libgcc -static-libstdc++ -Wall
+
+# Input files
+SOURCES			= $(shell find * -name "*.cpp")	
+OBJECTS			= $(SOURCES:.cpp=.o)
+TARGET			= verifydtapn-win64
+
+include rules.mk

=== 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 @@
 #include <sstream>
 #include "boost/algorithm/string.hpp"
 #include "boost/lexical_cast.hpp"
-#include "boost/make_shared.hpp"
 #include <iomanip>
 #include "boost/tokenizer.hpp"
 
@@ -135,52 +134,52 @@
     //       Each line in the description is assumed to fit within the remaining width
     //       of the console, so keep descriptions short, or implement manual word-wrapping :).
     parsers.push_back(
-            boost::make_shared<SwitchWithArg > ("k", KBOUND_OPTION,
+            new SwitchWithArg ("k", KBOUND_OPTION,
             "Max tokens to use during exploration.", 0));
     parsers.push_back(
-            boost::make_shared<SwitchWithArg > ("o", SEARCH_OPTION,
+            new SwitchWithArg ("o", SEARCH_OPTION,
             "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",
             4));
     parsers.push_back(
-            boost::make_shared<SwitchWithArg > ("m", VERIFICATION_OPTION,
+            new SwitchWithArg ("m", VERIFICATION_OPTION,
             "Specify the desired verification method.\n - 0: Default (discrete)\n - 1: Time Darts",
             0));
     parsers.push_back(
-            boost::make_shared<SwitchWithArg > ("p", MEMORY_OPTIMIZATION_OPTION,
+            new SwitchWithArg ("p", MEMORY_OPTIMIZATION_OPTION,
             "Specify the desired memory optimization.\n - 0: None \n - 1: PTrie",
             0)); 
     parsers.push_back(
-            boost::make_shared<SwitchWithArg > ("t", TRACE_OPTION,
+            new SwitchWithArg ("t", TRACE_OPTION,
             "Specify the desired trace option.\n - 0: none\n - 1: some\n - 2: fastest",
             0));
     parsers.push_back(
-            boost::make_shared<Switch > ("d", KEEP_DEAD,
+            new Switch ("d", KEEP_DEAD,
             "Do not discard dead tokens\n(used for boundedness checking)"));
     parsers.push_back(
-            boost::make_shared<Switch > ("g", MAX_CONSTANT_OPTION,
+            new Switch ("g", MAX_CONSTANT_OPTION,
             "Use global maximum constant for \nextrapolation (as opposed to local \nconstants)."));
     parsers.push_back(
-            boost::make_shared<Switch > ("s", LEGACY,
+            new Switch ("s", LEGACY,
             "Legacy option (no effect)."));
 
     parsers.push_back(
-            boost::make_shared<Switch > ("x", XML_TRACE_OPTION,
+            new Switch ("x", XML_TRACE_OPTION,
             "Output trace in xml format for TAPAAL."));
 
     parsers.push_back(
-            boost::make_shared<Switch >("c", GCD,
+            new Switch("c", GCD,
             "Enable lowering the guards by the greatest common divisor"));
     
     parsers.push_back(
-            boost::make_shared<SwitchWithArg > ("w", WORKFLOW,
+            new SwitchWithArg ("w", WORKFLOW,
             "Workflow mode.\n - 0: Disabled\n - 1: Soundness (and min)\n - 2: Strong Soundness (and max)",
             0));
     parsers.push_back(
-            boost::make_shared<SwitchWithArg > ("b", STRONG_WORKFLOW_BOUND,
+            new SwitchWithArg ("b", STRONG_WORKFLOW_BOUND,
             "Maximum delay bound for strong workflow analysis",
             0));
     parsers.push_back(
-            boost::make_shared<Switch> ("n", CALCULATE_CMAX,
+            new Switch ("n", CALCULATE_CMAX,
             "Calculate the place bounds"));
 
     };
@@ -194,9 +193,8 @@
 			<< "Displays this help message." << std::endl;
 	std::cout << std::setw(WIDTH) << std::left << "-v [ --version ]"
 			<< "Displays version information." << std::endl;
-	for (parser_vec::const_iterator arg = parsers.begin(); arg != parsers.end();
-			arg++) {
-		std::cout << **arg;
+	for (auto& p : parsers) {
+		std::cout << *p;
 	}
 }
 ;

=== 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 @@
 #include <map>
 #include <string>
 #include <iosfwd>
-#include "boost/smart_ptr.hpp"
 #include "VerificationOptions.hpp"
 #include "boost/lexical_cast.hpp"
 
@@ -78,10 +77,10 @@
 	};
 
 	class ArgsParser {
-		typedef std::vector< boost::shared_ptr<Switch> > parser_vec;
+		typedef std::vector< Switch* > parser_vec;
 	public:
 		ArgsParser() : parsers(), version(3,2,0) { initialize(); };
-		virtual ~ArgsParser() {};
+		virtual ~ArgsParser() { for( auto p : parsers) delete p; };
 
 		VerificationOptions parse(int argc, char* argv[]) const;
 	private:

=== 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 @@
 namespace Util {
 
 using namespace std;
-using namespace boost::numeric;
 
 vector<interval > setIntersection(const vector<interval >& first, const vector<interval >& second){
 	vector<interval > result;
@@ -29,7 +28,7 @@
 
 		interval intersection = intersect(first.at(i), second.at(j));
 
-		if(!empty(intersection)){
+		if(!intersection.empty()){
 			result.push_back(intersection);
 		}
 
@@ -44,6 +43,25 @@
 	return result;
 }
 
+interval intersect(const interval& l, const interval r)
+{
+    if(l.empty()) return l;
+    if(r.empty()) return r;
+    interval n(std::max(l.low, r.low), std::min(l.high, r.high));
+    return n;
+}
+
+interval hull(const interval& l, const interval r)
+{
+    return interval(std::min(l.low, r.low), std::max(l.high, r.high));
+}
+
+bool overlap(const interval& l, const interval r)
+{
+    auto i = intersect(l, r);
+    return !i.empty();
+}
+
 void setAdd(vector< interval >& first, const interval& element){
 
 	for(unsigned int i = 0; i < first.size(); i++){
@@ -55,13 +73,13 @@
 		} else if(overlap(element, first.at(i))){
 			interval u = hull(element, first.at(i));
 			// Merge with node
-			first.at(i).assign(u.lower(), u.upper());
+			first[i] = u;
 			// Clean up
 			for(i++; i < first.size(); i++){
 				if(first.at(i).lower() <= u.upper()){
 					// Merge items
 					if(first.at(i).upper() > u.upper()){
-						first.at(i-1).assign(first.at(i-1).lower(), first.at(i).upper());
+						first[i-1] = interval(first.at(i-1).lower(), first.at(i).upper());
 					}
 					first.erase(first.begin()+i);
 					i--;

=== 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 @@
 #define INTERVALOPS_HPP_
 
 #include <vector>
-#include "boost/numeric/interval.hpp"
+#include <limits>
 
 namespace VerifyTAPN {
 namespace DiscreteVerification {
 namespace Util {
 
-typedef boost::numeric::interval_lib::rounded_math< int > rounding_policy;
-typedef boost::numeric::interval_lib::checking_no_nan< int > checking_policy;
-typedef boost::numeric::interval_lib::policies< rounding_policy, checking_policy > interval_policies;
-typedef boost::numeric::interval< int, interval_policies > interval;
+    struct interval {
+        int low, high;
+        interval(int l, int h) : low(l), high(h) 
+        {
+            if(low > high)
+            {
+                low = std::numeric_limits<int>::max();
+                high = std::numeric_limits<int>::min();
+            }
+        };
+        auto upper() const {return high; }
+        auto lower() const {return low; }
+        auto empty() const { return high < low; }
+    };
 
-void setAdd(std::vector< interval >& first, const interval& element);
-std::vector<interval > setIntersection(const std::vector<interval >& first,
-		const std::vector<interval >& second);
+    interval intersect(const interval& l, const interval r);
+    interval hull(const interval& l, const interval r);
+    bool overlap(const interval& l, const interval r);
+    
+    
+    void setAdd(std::vector< interval >& first, const interval& element);
+    std::vector<interval > setIntersection(const std::vector<interval >& first,
+                    const std::vector<interval >& second);
 
 } /* namespace Util */
 } /* namespace DiscreteVerification */

=== 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 @@
                 Util::interval arcGuard((*arc)->getInterval().getLowerBound(), (*arc)->getInterval().getUpperBound());
                 Util::interval invGuard(0, (*arc)->getDestination().getInvariant().getBound());
 
-                Util::interval arcInterval = boost::numeric::intersect(arcGuard, invGuard);
+                Util::interval arcInterval = Util::intersect(arcGuard, invGuard);
                 vector<Util::interval > intervals;
                 int range;
                 if (arcInterval.upper() == INT_MAX) {