Merge commit '42edc5e9' into release/0.1-newotawa

include/PPLDomain.h

@@ -29,8 +29,8 @@ enum bound_t : signed long {
 };
 
 /* TODO(clement): detect stack conf. from OTAWA */ 
-enum stackconf_t : uint32_t {
-	STACK_TOP = 0x70000000,
+enum stackconf_t : int32_t {
+	STACK_TOP = -0x60000000,
 	STACK_SIZE = 0x10000000,
 };
 

include/PolyCommon.h

@@ -11,7 +11,7 @@
 
 #include "MyHTable.h"
 
-// #define POLY_DEBUG 1
+//#define POLY_DEBUG 1
 
 namespace otawa {
 namespace poly {

poly_PPLManager.cpp

@@ -41,6 +41,8 @@ PPLManager::PPLManager(const PropList &props, WorkSpace *ws)
 	/* TODO(clement): get real stack base address */
 	_init.doNewConstraint(var_ssp >= int(stackconf_t::STACK_TOP));
 	_init.doNewConstraint(var_sfp >= int(stackconf_t::STACK_TOP));
+	_init.doNewConstraint(var_ssp <= int(stackconf_t::STACK_TOP + 0x1000000));
+	_init.doNewConstraint(var_sfp <= int(stackconf_t::STACK_TOP + 0x1000000));
 }
 
 } // namespace poly