+ }
+ if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
+ //XBT_DEBUG("Different memcmp for data in libsimgrid");
+ errors++;
+ }
+ break;
+ case 2:
+ //XBT_DEBUG("Region : program");
+ if(s1->regions[i]->size != s2->regions[i]->size){
+ //XBT_DEBUG("Different size of program (s1 = %Zu, s2 = %Zu)", s1->regions[i]->size, s2->regions[i]->size);
+ return 1;
+ }
+ if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
+ //XBT_DEBUG("Different start addr of program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
+ return 1;
+ }
+ if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
+ //XBT_DEBUG("Different memcmp for data in program");
+ errors++;
+ }
+ break;
+ case 3:
+ //XBT_DEBUG("Region : stack");
+ if(s1->regions[i]->size != s2->regions[i]->size){
+ //XBT_DEBUG("Different size of stack (s1 = %Zu, s2 = %Zu)", s1->regions[i]->size, s2->regions[i]->size);
+ return 1;
+ }
+ if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
+ //XBT_DEBUG("Different start addr of stack (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
+ return 1;
+ }
+ if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
+ //XBT_DEBUG("Different memcmp for data in stack");
+ errors++;
+ }
+ break;
+ }
+ }
+
+ return (errors>0);
+
+}
+
+int reached(xbt_automaton_t a, xbt_state_t st, char *prgm){
+
+
+ if(xbt_fifo_size(reached_pairs) == 0){
+
+ return 0;
+
+ }else{
+
+ xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
+
+ /* Get values of propositional symbols */
+ unsigned int cursor = 0;
+ xbt_propositional_symbol_t ps = NULL;
+ xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
+ int (*f)() = ps->function;
+ int res = (*f)();
+ xbt_dynar_push_as(prop_ato, int, res);
+ }
+
+ MC_SET_RAW_MEM;
+ mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
+ MC_take_snapshot_liveness(sn, prgm);
+ MC_UNSET_RAW_MEM;
+
+ int i=0;
+ xbt_fifo_item_t item = xbt_fifo_get_first_item(reached_pairs);
+ mc_pair_reached_t pair_test = NULL;
+
+ while(i < xbt_fifo_size(reached_pairs)){
+
+ pair_test = (mc_pair_reached_t) xbt_fifo_get_item_content(item);
+
+ if(automaton_state_compare(pair_test->automaton_state, st) == 0){
+ if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
+ if(snapshot_compare(sn, pair_test->system_state) == 0){
+ MC_SET_RAW_MEM;
+ MC_free_snapshot(sn);
+ MC_UNSET_RAW_MEM;
+ return 1;
+ }
+ }
+ }
+
+ item = xbt_fifo_get_next_item(item);
+
+ i++;
+