From: Marion Guthmuller Date: Tue, 25 Oct 2011 08:47:11 +0000 (+0200) Subject: model-checker : change printf for size_t variables X-Git-Tag: exp_20120216~133^2~60 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/0d1c9172064ba746ed23e4e36146a3605491f5fa model-checker : change printf for size_t variables --- diff --git a/examples/msg/mc/CMakeLists.txt b/examples/msg/mc/CMakeLists.txt index 3a9eb3e15b..f330a040e8 100644 --- a/examples/msg/mc/CMakeLists.txt +++ b/examples/msg/mc/CMakeLists.txt @@ -14,6 +14,10 @@ automatonparse_promela.c example_liveness_without_cycle.c) add_executable(example2_liveness_without_cycle automaton.c automatonparse_promela.c example2_liveness_without_cycle.c) +add_executable(example_liveness_with_cycle automaton.c +automatonparse_promela.c example_liveness_with_cycle.c) + + target_link_libraries(centralized simgrid m ) @@ -24,4 +28,5 @@ target_link_libraries(bugged2 simgrid m ) target_link_libraries(bugged3 simgrid m ) target_link_libraries(random_test simgrid m ) target_link_libraries(example_liveness_without_cycle simgrid m ) -target_link_libraries(example2_liveness_without_cycle simgrid m ) \ No newline at end of file +target_link_libraries(example2_liveness_without_cycle simgrid m ) +target_link_libraries(example_liveness_with_cycle simgrid m ) diff --git a/examples/msg/mc/bugged3.c b/examples/msg/mc/bugged3.c index a398f0fa8a..8e33b31fa1 100644 --- a/examples/msg/mc/bugged3.c +++ b/examples/msg/mc/bugged3.c @@ -29,7 +29,7 @@ int server(int argc, char *argv[]) val1 = (long) MSG_task_get_data(task1); XBT_INFO("Received %lu", val1); - //MC_assert(val1 == 2); + MC_assert(val1 == 2); XBT_INFO("OK"); return 0; diff --git a/examples/msg/mc/example2_liveness_without_cycle.c b/examples/msg/mc/example2_liveness_without_cycle.c index 14c54b063a..519933c5dd 100644 --- a/examples/msg/mc/example2_liveness_without_cycle.c +++ b/examples/msg/mc/example2_liveness_without_cycle.c @@ -20,7 +20,7 @@ XBT_LOG_NEW_DEFAULT_CATEGORY(example_liveness_with_cycle, "Example liveness with extern xbt_automaton_t automaton; -int p=1; +int p=0; int q=0; @@ -51,7 +51,7 @@ int server(int argc, char *argv[]) val1 = (long) MSG_task_get_data(task1); XBT_INFO("Received %lu", val1); - //MC_assert_pair_stateless(val1 == 2); + MC_assert_pair_stateless(val1 == 2); /*if(val1 == 2) q = 1; diff --git a/examples/msg/mc/example_liveness_with_cycle.c b/examples/msg/mc/example_liveness_with_cycle.c index 42ef27daa1..09deb12f98 100644 --- a/examples/msg/mc/example_liveness_with_cycle.c +++ b/examples/msg/mc/example_liveness_with_cycle.c @@ -12,7 +12,7 @@ #include "y.tab.c" #define AMOUNT_OF_CLIENTS 2 -#define CS_PER_PROCESS 1 +#define CS_PER_PROCESS 2 XBT_LOG_NEW_DEFAULT_CATEGORY(example_liveness_with_cycle, "my log messages"); @@ -27,6 +27,10 @@ int predQ(){ return q; } + +//xbt_dynar_t listeVars -> { void *ptr; int size (nb octets); } => liste de structures +//=> parcourir la liste et comparer les contenus de chaque pointeur + int coordinator(int argc, char *argv[]) { xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL); // dynamic vector storing requests (which are char*) @@ -48,23 +52,21 @@ int coordinator(int argc, char *argv[]) m_task_t answer = MSG_task_create("grant", 0, 1000, NULL); MSG_task_send(answer, req); CS_used = 1; - }else{ + }else{ m_task_t answer = MSG_task_create("notgrant", 0, 1000, NULL); MSG_task_send(answer, req); } - } } else { // that's a release. Check if someone was waiting for the lock if (xbt_dynar_length(requests) > 0) { XBT_INFO("CS release. Grant to queued requests (queue size: %lu)", xbt_dynar_length(requests)); - char *req; + char *req ; + xbt_dynar_pop(requests, &req); if(strcmp(req, "1") == 0){ - xbt_dynar_pop(requests, &req); MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req); todo--; }else{ - xbt_dynar_pop(requests, &req); MSG_task_send(MSG_task_create("notgrant", 0, 1000, NULL), req); todo--; } @@ -88,12 +90,10 @@ int client(int argc, char *argv[]) // request the CS 2 times, sleeping a bit in between int i; for (i = 0; i < CS_PER_PROCESS; i++) { - p = 1; - q = 0; XBT_INFO("Ask the request"); MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator"); - if(strcmp(my_mailbox, "1") == 0){ + if(strcmp(my_mailbox, "2") == 0){ p = 1; q = 0; } @@ -112,12 +112,6 @@ int client(int argc, char *argv[]) MSG_process_sleep(1); MSG_task_send(MSG_task_create("release", 0, 1000,NULL ), "coordinator"); - }else{ - MSG_task_destroy(grant); - XBT_INFO("Negative answer"); - MSG_process_sleep(1); - MSG_task_send(MSG_task_create("notrelease", 0, 1000,NULL ), - "coordinator"); } MSG_process_sleep(my_pid); diff --git a/examples/msg/mc/example_liveness_without_cycle.c b/examples/msg/mc/example_liveness_without_cycle.c index a6e998cb24..a43f7c8c00 100644 --- a/examples/msg/mc/example_liveness_without_cycle.c +++ b/examples/msg/mc/example_liveness_without_cycle.c @@ -12,32 +12,18 @@ XBT_LOG_NEW_DEFAULT_CATEGORY(example_liveness_without_cycle, "Example liveness w extern xbt_automaton_t automaton; - -int p=1; int r=1; -int q=1; int e=1; int d=1; - -int predP(){ - return p; -} - int predR(){ return r; } -int predQ(){ - return q; -} - - int predD(){ return d; } - int predE(){ return e; } @@ -59,7 +45,7 @@ int server(int argc, char *argv[]) //XBT_INFO("r (server) = %d", r); } - MC_assert_pair_stateless(atoi(MSG_task_get_name(task)) == 3); + //MC_assert_pair_stateless(atoi(MSG_task_get_name(task)) == 3); XBT_INFO("OK"); return 0; @@ -76,7 +62,7 @@ int client(int argc, char *argv[]) XBT_INFO("Sent!"); - //r=(r+1)%3; + r=(r+1)%2; //XBT_INFO("r (client) = %d", r); return 0; @@ -88,9 +74,7 @@ int main(int argc, char **argv){ init(); yyparse(); automaton = get_automaton(); - xbt_propositional_symbol_t ps = xbt_new_propositional_symbol(automaton,"p", &predP); - ps = xbt_new_propositional_symbol(automaton,"q", &predQ); - ps = xbt_new_propositional_symbol(automaton,"r", &predR); + xbt_propositional_symbol_t ps = xbt_new_propositional_symbol(automaton,"r", &predR); ps = xbt_new_propositional_symbol(automaton,"e", &predE); ps = xbt_new_propositional_symbol(automaton,"d", &predD); diff --git a/examples/msg/mc/example_liveness_without_cycle.h b/examples/msg/mc/example_liveness_without_cycle.h index 1ff4c9982b..1667c45f65 100644 --- a/examples/msg/mc/example_liveness_without_cycle.h +++ b/examples/msg/mc/example_liveness_without_cycle.h @@ -1,5 +1,5 @@ -#ifndef _EXAMPLE_AUTOMATON_H -#define _EXAMPLE_AUTOMATON_H +#ifndef _EXAMPLE_LIVENESS_WITHOUT_CYCLE_H +#define _EXAMPLE_LIVENESS_WITHOUT_CYCLE_H int yyparse(void); int yywrap(void); diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index 60adc472da..480358ff7d 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -82,10 +82,11 @@ int reached(xbt_automaton_t a, mc_snapshot_t s){ cursor = 0; mc_pair_reached_t pair_test; + int (*compare_dynar)(const void*; const void*) = propositional_symbols_compare; xbt_dynar_foreach(reached_pairs, cursor, pair_test){ if(automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){ - if(xbt_dynar_compare(pair_test->prop_ato, pair->prop_ato, propositional_symbols_compare_value) == 0){ + if(xbt_dynar_compare(pair_test->prop_ato, pair->prop_ato, compare_dynar) == 0){ if(snapshot_compare(pair_test->system_state, pair->system_state) == 0){ MC_UNSET_RAW_MEM; return 1; diff --git a/src/xbt/automaton.c b/src/xbt/automaton.c index 46d06fa8d9..e9f4f02787 100644 --- a/src/xbt/automaton.c +++ b/src/xbt/automaton.c @@ -343,6 +343,6 @@ int automaton_label_transition_compare(xbt_exp_label_t l1, xbt_exp_label_t l2){ int propositional_symbols_compare_value(const void *s1, const void *s2){ - return (!((int)s1 == (int)s2)); + return (!(s1 == s2)); } diff --git a/src/xbt/mmalloc/mm_legacy.c b/src/xbt/mmalloc/mm_legacy.c index b2814b3fd4..6c72b25ee4 100644 --- a/src/xbt/mmalloc/mm_legacy.c +++ b/src/xbt/mmalloc/mm_legacy.c @@ -298,7 +298,7 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){ size_t block_free1, start1, block_free2 , start2, block_busy1, block_busy2 ; - unsigned int i; + size_t i; void *addr_block1, *addr_block2; struct mdesc* mdp; @@ -307,7 +307,7 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){ block_busy1 = start1 + mdp1->heapinfo[start1].free.size; block_busy2 = start2 + mdp2->heapinfo[start2].free.size; - XBT_DEBUG("Block busy : %d - %d", block_busy1, block_busy2); + XBT_DEBUG("Block busy : %Zu - %Zu", block_busy1, block_busy2); if(mdp1->heapinfo[start1].free.size != mdp2->heapinfo[start2].free.size){ // <=> check block_busy @@ -326,12 +326,12 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){ i=block_busy1 ; - XBT_DEBUG("Next free : %d", mdp1->heapinfo[start1].free.next); + XBT_DEBUG("Next free : %Zu", mdp1->heapinfo[start1].free.next); while(iheapinfo[start1].free.next){ - XBT_DEBUG("i (block busy) : %d", i); + XBT_DEBUG("i (block busy) : %Zu", i); if(mdp1->heapinfo[i].busy.type != mdp2->heapinfo[i].busy.type){ XBT_DEBUG("Different type of busy block"); @@ -347,9 +347,9 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){ XBT_DEBUG("Different size of a large cluster"); return 1; }else{ - XBT_DEBUG("Blocks %d : %p - %p / Data size : %d (%d blocks)", i, addr_block1, addr_block2, (mdp->heapinfo[i].busy.info.size * BLOCKSIZE),mdp->heapinfo[i].busy.info.size ); + XBT_DEBUG("Blocks %Zu : %p - %p / Data size : %Zu (%Zu blocks)", i, addr_block1, addr_block2, (mdp->heapinfo[i].busy.info.size * BLOCKSIZE),mdp->heapinfo[i].busy.info.size ); if(memcmp(addr_block1, addr_block2, mdp1->heapinfo[i].busy.info.size * BLOCKSIZE) != 0){ - XBT_DEBUG("Different data in block %d", i); + XBT_DEBUG("Different data in block %Zu", i); return 1; } } @@ -365,7 +365,7 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){ return 1; }else{ if(memcmp(addr_block1, addr_block2, BLOCKSIZE) != 0){ - XBT_DEBUG("Different data in block %d", i); + XBT_DEBUG("Different data in block %Zu", i); return 1; } } @@ -392,14 +392,14 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){ return 1; }else{ - XBT_DEBUG("Index of next busy block : %d - %d", block_busy1, block_busy2); - XBT_DEBUG("Index of next free cluster : %d", mdp1->heapinfo[block_free1].free.next); + XBT_DEBUG("Index of next busy block : %Zu - %Zu", block_busy1, block_busy2); + XBT_DEBUG("Index of next free cluster : %Zu", mdp1->heapinfo[block_free1].free.next); i = block_busy1; while(iheapinfo[block_free1].free.next){ - XBT_DEBUG("i (block busy) : %d", i); + XBT_DEBUG("i (block busy) : %Zu", i); if(mdp1->heapinfo[i].busy.type != mdp2->heapinfo[i].busy.type){ XBT_DEBUG("Different type of busy block"); @@ -415,10 +415,10 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){ XBT_DEBUG("Different size of a large cluster"); return 1; }else{ - XBT_DEBUG("Blocks %d : %p - %p / Data size : %d", i, addr_block1, addr_block2, (mdp->heapinfo[i].busy.info.size * BLOCKSIZE)); + XBT_DEBUG("Blocks %Zu : %p - %p / Data size : %Zu", i, addr_block1, addr_block2, (mdp->heapinfo[i].busy.info.size * BLOCKSIZE)); //XBT_DEBUG("Size of large cluster %d", mdp->heapinfo[i].busy.info.size); if(memcmp(addr_block1, addr_block2, (mdp1->heapinfo[i].busy.info.size * BLOCKSIZE)) != 0){ - XBT_DEBUG("Different data in block %d", i); + XBT_DEBUG("Different data in block %Zu", i); return 1; } } @@ -434,7 +434,7 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){ return 1; }else{ if(memcmp(addr_block1, addr_block2, BLOCKSIZE) != 0){ - XBT_DEBUG("Different data in fragmented block %d", i); + XBT_DEBUG("Different data in fragmented block %Zu", i); return 1; } }