Check out-of-bound during the computation

of successors

* tools/dvecompile.cpp, tools/dvecompile.h: here.

tools/dvecompile.cpp

@@ -982,6 +982,7 @@ void dve_compiler::transition_effect( ext_transition_t *et, std::string in, std:
         }
     }
 
+          
     //first transition effect
     assign( process_state( et->first->get_process_gid(), out ),
             fmt( et->first->get_state2_lid() ) );

tools/dvecompile.h

@@ -161,7 +161,7 @@ struct dve_compiler: public dve_explicit_system_t
     }
 
     void assign( std::string left, std::string right ) {
-        line( left + " = " + right + ";" );
+      line( left + " = " + right + ";" );
     }
 
     std::string relate( std::string left, std::string op, std::string right ) {
@@ -201,9 +201,55 @@ struct dve_compiler: public dve_explicit_system_t
 
     std::string cmaybe( dve_expression_t &expr, std::string state );
     std::string cexpr( dve_expression_t &expr, std::string state, bool wrap );
-    void print_cexpr( dve_expression_t &expr, std::string state )
-    {
-        line( cexpr( expr, state, false ) + ";" );
+
+  
+  template <typename T>
+  string to_string(T val)
+  {
+    stringstream stream;
+    stream << val;
+    return stream.str();
+  }
+
+  void print_check_bounds( dve_expression_t &expr, std::string state)
+  {
+    assert(expr.get_operator() == T_SQUARE_BRACKETS);
+    if (!expr.arity())
+      return ;
+    dve_symbol_table_t * parent_table = expr.get_symbol_table();
+    line ("// Here check out-of-bounds");
+    line ("if ("
+          + to_string(parent_table->get_variable(expr.get_ident_gid())->get_vector_size())
+          + "<="
+          + to_string (cexpr(*expr.subexpr(0), state, false ))
+          + ")"); 
+    line ("{ /* fprintf( stderr, \"Out-of-bound! see line:\" );*/ return -1; }");
+  }
+
+  
+  void print_cexpr( dve_expression_t &expr, std::string state )
+  {
+    if (expr.get_operator() == T_SQUARE_BRACKETS)
+      {
+        print_check_bounds(expr, state);
+      }
+    // Case where we perform exp_1 = expr_2
+    else if (expr.get_operator() == T_ASSIGNMENT)
+      {
+        dve_symbol_table_t * parent_table = expr.get_symbol_table();
+        if (expr.left()->get_operator() == T_SQUARE_BRACKETS &&
+            parent_table->get_variable(expr.left()->get_ident_gid())->is_vector())
+          {
+            print_check_bounds(*expr.left(), state);
+          }
+        if (expr.right()->get_operator() == T_SQUARE_BRACKETS &&
+            parent_table->get_variable(expr.right()->get_ident_gid())->is_vector())
+          {
+            print_check_bounds(*expr.right(), state);
+          }
+      }
+      
+    line( cexpr( expr, state, false ) + ";" );
     }
 
     void new_label() {