From b65a2e3cea58dea5f2122c44a57e16662fe11a2d Mon Sep 17 00:00:00 2001
From: Marion Guthmuller <marion.guthmuller@loria.fr>
Date: Fri, 8 Feb 2013 14:37:03 +0100
Subject: [PATCH 1/1] model-checker : get instruction pointer and frame name
 with libunwind for the comparison of stacks

---
 src/mc/mc_checkpoint.c |  5 ++++-
 src/mc/mc_compare.c    | 42 +++++++++++++++++++++++++++++++-----------
 2 files changed, 35 insertions(+), 12 deletions(-)

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index a8591eec76..f4ec6ef414 100644
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -463,7 +463,10 @@ static xbt_strbuff_t get_local_variables_values(void *stack_context, void *heap)
       return variables;
     }
 
-    to_append = bprintf("ip=%s\n", frame_name);
+    to_append = bprintf("ip=%lx\n", ip);
+    xbt_strbuff_append(variables, to_append);
+    xbt_free(to_append);
+    to_append = bprintf("frame_name=%s\n", frame_name);
     xbt_strbuff_append(variables, to_append);
     xbt_free(to_append);
 
diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c
index bc91e37605..6aa077780c 100644
--- a/src/mc/mc_compare.c
+++ b/src/mc/mc_compare.c
@@ -521,7 +521,7 @@ static int compare_local_variables(char *s1, char *s2){
   xbt_dynar_t s_tokens1, s_tokens2;
   unsigned int cursor = 0;
   void *addr1, *addr2;
-  char *ip1 = NULL, *ip2 = NULL;
+  char *frame_name1 = NULL, *frame_name2 = NULL;
   int res_compare = 0;
 
   #ifdef MC_VERBOSE
@@ -535,18 +535,18 @@ static int compare_local_variables(char *s1, char *s2){
       #ifdef MC_VERBOSE
         var_name = xbt_dynar_get_as(s_tokens1, 0, char *);
       #endif
-      if((strcmp(xbt_dynar_get_as(s_tokens1, 0, char *), "ip") == 0) && (strcmp(xbt_dynar_get_as(s_tokens2, 0, char *), "ip") == 0)){
-        xbt_free(ip1);
-        xbt_free(ip2);
-        ip1 = strdup(xbt_dynar_get_as(s_tokens1, 1, char *));
-        ip2 = strdup(xbt_dynar_get_as(s_tokens2, 1, char *));
+      if((strcmp(xbt_dynar_get_as(s_tokens1, 0, char *), "frame_name") == 0) && (strcmp(xbt_dynar_get_as(s_tokens2, 0, char *), "frame_name") == 0)){
+        xbt_free(frame_name1);
+        xbt_free(frame_name2);
+        frame_name1 = strdup(xbt_dynar_get_as(s_tokens1, 1, char *));
+        frame_name2 = strdup(xbt_dynar_get_as(s_tokens2, 1, char *));
       }
       addr1 = (void *) strtoul(xbt_dynar_get_as(s_tokens1, 1, char *), NULL, 16);
       addr2 = (void *) strtoul(xbt_dynar_get_as(s_tokens2, 1, char *), NULL, 16);
       if(addr1 > std_heap && (char *)addr1 <= (char *)std_heap + STD_HEAP_SIZE && addr2 > std_heap && (char *)addr2 <= (char *)std_heap + STD_HEAP_SIZE){
         res_compare = compare_area(addr1, addr2, NULL);
         if(res_compare == 1){
-          if(is_stack_ignore_variable(ip1, xbt_dynar_get_as(s_tokens1, 0, char *)) && is_stack_ignore_variable(ip2, xbt_dynar_get_as(s_tokens2, 0, char *))){
+          if(is_stack_ignore_variable(frame_name1, xbt_dynar_get_as(s_tokens1, 0, char *)) && is_stack_ignore_variable(frame_name2, xbt_dynar_get_as(s_tokens2, 0, char *))){
             xbt_dynar_free(&s_tokens1);
             xbt_dynar_free(&s_tokens2);
             cursor++;
@@ -559,8 +559,28 @@ static int compare_local_variables(char *s1, char *s2){
             xbt_dynar_free(&s_tokens2);
             xbt_dynar_free(&tokens1);
             xbt_dynar_free(&tokens2);
-            xbt_free(ip1);
-            xbt_free(ip2);
+            xbt_free(frame_name1);
+            xbt_free(frame_name2);
+            return 1;
+          }
+        }
+      }else{
+        if(strcmp(xbt_dynar_get_as(s_tokens1, 1, char *), xbt_dynar_get_as(s_tokens2, 1, char *)) != 0){
+          if(is_stack_ignore_variable(frame_name1, xbt_dynar_get_as(s_tokens1, 0, char *)) && is_stack_ignore_variable(frame_name2, xbt_dynar_get_as(s_tokens2, 0, char *))){
+            xbt_dynar_free(&s_tokens1);
+            xbt_dynar_free(&s_tokens2);
+            cursor++;
+            continue;
+          }else {
+            #ifdef MC_VERBOSE
+              XBT_VERB("Different local variable : %s (%s - %s)", var_name, xbt_dynar_get_as(s_tokens1, 1, char *), xbt_dynar_get_as(s_tokens2, 1, char *));
+            #endif
+            xbt_dynar_free(&s_tokens1);
+            xbt_dynar_free(&s_tokens2);
+            xbt_dynar_free(&tokens1);
+            xbt_dynar_free(&tokens2);
+            xbt_free(frame_name1);
+            xbt_free(frame_name2);
             return 1;
           }
         }
@@ -572,8 +592,8 @@ static int compare_local_variables(char *s1, char *s2){
     cursor++;
   }
 
-  xbt_free(ip1);
-  xbt_free(ip2);
+  xbt_free(frame_name1);
+  xbt_free(frame_name2);
   xbt_dynar_free(&tokens1);
   xbt_dynar_free(&tokens2);
   return 0;
-- 
2.20.1