Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
[mc] Remove useless braces
authorGabriel Corona <gabriel.corona@loria.fr>
Thu, 3 Mar 2016 17:58:46 +0000 (18:58 +0100)
committerGabriel Corona <gabriel.corona@loria.fr>
Mon, 7 Mar 2016 08:48:18 +0000 (09:48 +0100)
15 files changed:
src/mc/ModelChecker.cpp
src/mc/PageStore.cpp
src/mc/Process.cpp
src/mc/RegionSnapshot.cpp
src/mc/mc_global.cpp
src/mc/mc_ignore.cpp
src/mc/mc_liveness.cpp
src/mc/mc_memory.cpp
src/mc/mc_mmu.h
src/mc/mc_protocol.cpp
src/mc/mc_request.cpp
src/mc/mc_safety.cpp
src/mc/mc_smx.cpp
src/mc/mc_snapshot.cpp
src/mc/mc_state.cpp

index 15f6d23..0d97a64 100644 (file)
@@ -319,9 +319,8 @@ bool ModelChecker::handle_events()
         throw simgrid::xbt::errno_error(errno);
       return handle_message(buffer, size);
     }
         throw simgrid::xbt::errno_error(errno);
       return handle_message(buffer, size);
     }
-    if (socket_pollfd->revents & POLLERR) {
+    if (socket_pollfd->revents & POLLERR)
       throw_socket_error(socket_pollfd->fd);
       throw_socket_error(socket_pollfd->fd);
-    }
     if (socket_pollfd->revents & POLLHUP)
       xbt_die("Socket hang up?");
   }
     if (socket_pollfd->revents & POLLHUP)
       xbt_die("Socket hang up?");
   }
@@ -331,9 +330,8 @@ bool ModelChecker::handle_events()
       this->handle_signals();
       return true;
     }
       this->handle_signals();
       return true;
     }
-    if (signalfd_pollfd->revents & POLLERR) {
+    if (signalfd_pollfd->revents & POLLERR)
       throw_socket_error(signalfd_pollfd->fd);
       throw_socket_error(signalfd_pollfd->fd);
-    }
     if (signalfd_pollfd->revents & POLLHUP)
       xbt_die("Signalfd hang up?");
   }
     if (signalfd_pollfd->revents & POLLHUP)
       xbt_die("Signalfd hang up?");
   }
@@ -427,10 +425,9 @@ void ModelChecker::on_signal(const struct signalfd_siginfo* info)
 void ModelChecker::wait_client(simgrid::mc::Process& process)
 {
   this->resume(process);
 void ModelChecker::wait_client(simgrid::mc::Process& process)
 {
   this->resume(process);
-  while (this->process().running()) {
+  while (this->process().running())
     if (!this->handle_events())
       return;
     if (!this->handle_events())
       return;
-  }
 }
 
 void ModelChecker::simcall_handle(simgrid::mc::Process& process, unsigned long pid, int value)
 }
 
 void ModelChecker::simcall_handle(simgrid::mc::Process& process, unsigned long pid, int value)
@@ -442,10 +439,9 @@ void ModelChecker::simcall_handle(simgrid::mc::Process& process, unsigned long p
   m.value = value;
   process.send_message(m);
   process.cache_flags = (mc_process_cache_flags_t) 0;
   m.value = value;
   process.send_message(m);
   process.cache_flags = (mc_process_cache_flags_t) 0;
-  while (process.running()) {
+  while (process.running())
     if (!this->handle_events())
       return;
     if (!this->handle_events())
       return;
-  }
 }
 
 }
 }
 
 }
index 7f7e166..3289157 100644 (file)
@@ -39,9 +39,8 @@ PageStore::hash_type mc_hash_page(const void* data)
 
   // This djb2:
   std::uint64_t hash = 5381;
 
   // This djb2:
   std::uint64_t hash = 5381;
-  for (std::size_t i = 0; i != n; ++i) {
+  for (std::size_t i = 0; i != n; ++i)
     hash = ((hash << 5) + hash) + values[i];
     hash = ((hash << 5) + hash) + values[i];
-  }
   return hash;
 }
 
   return hash;
 }
 
@@ -54,9 +53,8 @@ PageStore::PageStore(size_t size) :
   // by relocating it somewhere else in the virtual memory
   // space:
   void* memory = ::mmap(nullptr, size << xbt_pagebits, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS|MAP_POPULATE, -1, 0);
   // by relocating it somewhere else in the virtual memory
   // space:
   void* memory = ::mmap(nullptr, size << xbt_pagebits, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS|MAP_POPULATE, -1, 0);
-  if (memory == MAP_FAILED) {
+  if (memory == MAP_FAILED)
     xbt_die("Could not mmap initial snapshot pages.");
     xbt_die("Could not mmap initial snapshot pages.");
-  }
 
   this->top_index_ = 0;
   this->capacity_ = size;
 
   this->top_index_ = 0;
   this->capacity_ = size;
@@ -77,9 +75,8 @@ void PageStore::resize(std::size_t size)
   // Expand the memory region by moving it into another
   // virtual memory address if necessary:
   void* new_memory = mremap(this->memory_, old_bytesize, new_bytesize, MREMAP_MAYMOVE);
   // Expand the memory region by moving it into another
   // virtual memory address if necessary:
   void* new_memory = mremap(this->memory_, old_bytesize, new_bytesize, MREMAP_MAYMOVE);
-  if (new_memory == MAP_FAILED) {
+  if (new_memory == MAP_FAILED)
     xbt_die("Could not mremap snapshot pages.");
     xbt_die("Could not mremap snapshot pages.");
-  }
 
   this->capacity_ = size;
   this->memory_ = new_memory;
 
   this->capacity_ = size;
   this->memory_ = new_memory;
@@ -95,10 +92,9 @@ std::size_t PageStore::alloc_page()
   if (this->free_pages_.empty()) {
 
     // Expand the region:
   if (this->free_pages_.empty()) {
 
     // Expand the region:
-    if (this->top_index_ == this->capacity_) {
+    if (this->top_index_ == this->capacity_)
       // All the pages are allocated, we need add more pages:
       this->resize(2 * this->capacity_);
       // All the pages are allocated, we need add more pages:
       this->resize(2 * this->capacity_);
-    }
 
     // Use a page from the top:
     return this->top_index_++;
 
     // Use a page from the top:
     return this->top_index_++;
index 5f52f50..80fa3f2 100644 (file)
@@ -246,9 +246,8 @@ Process::~Process()
   this->maestro_stack_start_ = nullptr;
   this->maestro_stack_end_ = nullptr;
 
   this->maestro_stack_start_ = nullptr;
   this->maestro_stack_end_ = nullptr;
 
-  if (this->memory_file >= 0) {
+  if (this->memory_file >= 0)
     close(this->memory_file);
     close(this->memory_file);
-  }
 
   if (this->unw_underlying_addr_space != unw_local_addr_space) {
     unw_destroy_addr_space(this->unw_underlying_addr_space);
 
   if (this->unw_underlying_addr_space != unw_local_addr_space) {
     unw_destroy_addr_space(this->unw_underlying_addr_space);
index bfcc7ba..333aed2 100644 (file)
@@ -119,11 +119,10 @@ RegionSnapshot region(
   RegionType type, void *start_addr, void* permanent_addr, size_t size,
   RegionSnapshot const* ref_region)
 {
   RegionType type, void *start_addr, void* permanent_addr, size_t size,
   RegionSnapshot const* ref_region)
 {
-  if (_sg_mc_sparse_checkpoint) {
+  if (_sg_mc_sparse_checkpoint)
     return sparse_region(type, start_addr, permanent_addr, size, ref_region);
     return sparse_region(type, start_addr, permanent_addr, size, ref_region);
-  } else  {
+  else
     return dense_region(type, start_addr, permanent_addr, size);
     return dense_region(type, start_addr, permanent_addr, size);
-  }
 }
 
 RegionSnapshot sparse_region(RegionType region_type,
 }
 
 RegionSnapshot sparse_region(RegionType region_type,
index 1fc984e..fa37b30 100644 (file)
@@ -112,9 +112,8 @@ void MC_init()
     MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
 
     smx_process_t process;
     MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
 
     smx_process_t process;
-    xbt_swag_foreach(process, simix_global->process_list) {
+    xbt_swag_foreach(process, simix_global->process_list)
       MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup));
       MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup));
-    }
   }
 }
 
   }
 }
 
@@ -165,12 +164,11 @@ int MC_deadlock_check()
   smx_process_t process;
   if (xbt_swag_size(simix_global->process_list)) {
     deadlock = TRUE;
   smx_process_t process;
   if (xbt_swag_size(simix_global->process_list)) {
     deadlock = TRUE;
-    xbt_swag_foreach(process, simix_global->process_list) {
+    xbt_swag_foreach(process, simix_global->process_list)
       if (MC_process_is_enabled(process)) {
         deadlock = FALSE;
         break;
       }
       if (MC_process_is_enabled(process)) {
         deadlock = FALSE;
         break;
       }
-    }
   }
   return deadlock;
 }
   }
   return deadlock;
 }
@@ -514,9 +512,8 @@ double MC_process_clock_get(smx_process_t process)
       return mc_time[process->pid];
     else
       return -1;
       return mc_time[process->pid];
     else
       return -1;
-  } else {
+  } else
     return 0;
     return 0;
-  }
 }
 
 void MC_process_clock_add(smx_process_t process, double amount)
 }
 
 void MC_process_clock_add(smx_process_t process, double amount)
index 5a440b5..1df9b1a 100644 (file)
@@ -92,9 +92,9 @@ void MC_register_stack_area(void *stack, smx_process_t process, ucontext_t* cont
       ((char *) stack -
        (char *) heap->heapbase) / BLOCKSIZE + 1;
 #ifdef HAVE_SMPI
       ((char *) stack -
        (char *) heap->heapbase) / BLOCKSIZE + 1;
 #ifdef HAVE_SMPI
-  if (smpi_privatize_global_variables && process) {
+  if (smpi_privatize_global_variables && process)
     region.process_index = smpi_process_index_of_smx_process(process);
     region.process_index = smpi_process_index_of_smx_process(process);
-  else
+  else
 #endif
   region.process_index = -1;
 
 #endif
   region.process_index = -1;
 
index d184f90..3d9dd53 100644 (file)
@@ -57,11 +57,9 @@ static mc_visited_pair_t is_reached_acceptance_pair(mc_pair_t pair)
   new_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
   new_pair->acceptance_pair = 1;
 
   new_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
   new_pair->acceptance_pair = 1;
 
-  if (xbt_dynar_is_empty(acceptance_pairs)) {
-
+  if (xbt_dynar_is_empty(acceptance_pairs))
     xbt_dynar_push(acceptance_pairs, &new_pair);
     xbt_dynar_push(acceptance_pairs, &new_pair);
-
-  } else {
+  else {
 
     int min = -1, max = -1, index;
     //int res;
 
     int min = -1, max = -1, index;
     //int res;
@@ -99,14 +97,12 @@ static mc_visited_pair_t is_reached_acceptance_pair(mc_pair_t pair)
       xbt_dynar_insert_at(acceptance_pairs, min, &new_pair);
     } else {
       pair_test = (mc_visited_pair_t) xbt_dynar_get_as(acceptance_pairs, index, mc_visited_pair_t);
       xbt_dynar_insert_at(acceptance_pairs, min, &new_pair);
     } else {
       pair_test = (mc_visited_pair_t) xbt_dynar_get_as(acceptance_pairs, index, mc_visited_pair_t);
-      if (pair_test->nb_processes < new_pair->nb_processes) {
+      if (pair_test->nb_processes < new_pair->nb_processes)
         xbt_dynar_insert_at(acceptance_pairs, index + 1, &new_pair);
         xbt_dynar_insert_at(acceptance_pairs, index + 1, &new_pair);
-      } else {
-        if (pair_test->heap_bytes_used < new_pair->heap_bytes_used)
-          xbt_dynar_insert_at(acceptance_pairs, index + 1, &new_pair);
-        else
-          xbt_dynar_insert_at(acceptance_pairs, index, &new_pair);
-      }
+      else if (pair_test->heap_bytes_used < new_pair->heap_bytes_used)
+        xbt_dynar_insert_at(acceptance_pairs, index + 1, &new_pair);
+      else
+        xbt_dynar_insert_at(acceptance_pairs, index, &new_pair);
     }
   }
   return new_pair;
     }
   }
   return new_pair;
@@ -118,12 +114,11 @@ static void remove_acceptance_pair(int pair_num)
   mc_visited_pair_t pair_test = nullptr;
   int pair_found = 0;
 
   mc_visited_pair_t pair_test = nullptr;
   int pair_found = 0;
 
-  xbt_dynar_foreach(acceptance_pairs, cursor, pair_test) {
+  xbt_dynar_foreach(acceptance_pairs, cursor, pair_test)
     if (pair_test->num == pair_num) {
        pair_found = 1;
       break;
     }
     if (pair_test->num == pair_num) {
        pair_found = 1;
       break;
     }
-  }
 
   if(pair_found == 1) {
     xbt_dynar_remove_at(acceptance_pairs, cursor, &pair_test);
 
   if(pair_found == 1) {
     xbt_dynar_remove_at(acceptance_pairs, cursor, &pair_test);
@@ -165,9 +160,8 @@ static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l,
       }
       return -1;
     }
       }
       return -1;
     }
-  case 4:{
-      return 2;
-    }
+  case 4:
+    return 2;
   default:
     return -1;
   }
   default:
     return -1;
   }
index 3df9bbe..5a452f6 100644 (file)
@@ -21,9 +21,8 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_memory, mc,
 /* It creates the two heap regions: std_heap and mc_heap */
 void MC_memory_init()
 {
 /* It creates the two heap regions: std_heap and mc_heap */
 void MC_memory_init()
 {
-  if (!malloc_use_mmalloc()) {
+  if (!malloc_use_mmalloc())
     xbt_die("Model-checking support is not enabled: run with simgrid-mc.");
     xbt_die("Model-checking support is not enabled: run with simgrid-mc.");
-  }
 }
 
 /* Finalize the memory subsystem */
 }
 
 /* Finalize the memory subsystem */
index 50b83dd..1117208 100644 (file)
@@ -27,9 +27,8 @@ static inline __attribute__ ((always_inline))
 size_t mc_page_count(size_t size)
 {
   size_t page_count = size >> xbt_pagebits;
 size_t mc_page_count(size_t size)
 {
   size_t page_count = size >> xbt_pagebits;
-  if (size & (xbt_pagesize-1)) {
+  if (size & (xbt_pagesize-1))
     page_count ++;
     page_count ++;
-  }
   return page_count;
 }
 
   return page_count;
 }
 
index 29fd979..027bdda 100644 (file)
@@ -27,12 +27,11 @@ int MC_protocol_send(int socket, const void* message, std::size_t size)
     MC_mode_name(mc_mode),
     MC_message_type_name(*(e_mc_message_type*) message));
 
     MC_mode_name(mc_mode),
     MC_message_type_name(*(e_mc_message_type*) message));
 
-  while (send(socket, message, size, 0) == -1) {
+  while (send(socket, message, size, 0) == -1)
     if (errno == EINTR)
       continue;
     else
       return errno;
     if (errno == EINTR)
       continue;
     else
       return errno;
-  }
   return 0;
 }
 
   return 0;
 }
 
@@ -46,11 +45,10 @@ int MC_protocol_send_simple_message(int socket, e_mc_message_type type)
 ssize_t MC_receive_message(int socket, void* message, size_t size, int options)
 {
   int res = recv(socket, message, size, options);
 ssize_t MC_receive_message(int socket, void* message, size_t size, int options)
 {
   int res = recv(socket, message, size, options);
-  if (res != -1) {
+  if (res != -1)
     XBT_DEBUG("Protocol [%s] received %s",
       MC_mode_name(mc_mode),
       MC_message_type_name(*(e_mc_message_type*) message));
     XBT_DEBUG("Protocol [%s] received %s",
       MC_mode_name(mc_mode),
       MC_message_type_name(*(e_mc_message_type*) message));
-  }
   return res;
 }
 
   return res;
 }
 
index 0e8640d..f85fad2 100644 (file)
@@ -348,9 +348,8 @@ char *MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t req
       args = bprintf("comm=%s (%d of %lu)",
         p, value + 1, xbt_dynar_length(&comms));
       xbt_free(p);
       args = bprintf("comm=%s (%d of %lu)",
         p, value + 1, xbt_dynar_length(&comms));
       xbt_free(p);
-    } else {
+    } else
       args = bprintf("comm at idx %d", value);
       args = bprintf("comm at idx %d", value);
-    }
     break;
   }
 
     break;
   }
 
@@ -412,19 +411,18 @@ char *MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t req
   }
 
   char* str;
   }
 
   char* str;
-  if (args != nullptr) {
+  if (args != nullptr)
     str =
         bprintf("[(%lu)%s (%s)] %s(%s)", issuer->pid,
                 MC_smx_process_get_host_name(issuer),
                 MC_smx_process_get_name(issuer),
                 type, args);
     str =
         bprintf("[(%lu)%s (%s)] %s(%s)", issuer->pid,
                 MC_smx_process_get_host_name(issuer),
                 MC_smx_process_get_name(issuer),
                 type, args);
-  } else {
+  else
     str =
         bprintf("[(%lu)%s (%s)] %s ", issuer->pid,
                 MC_smx_process_get_host_name(issuer),
                 MC_smx_process_get_name(issuer),
                 type);
     str =
         bprintf("[(%lu)%s (%s)] %s ", issuer->pid,
                 MC_smx_process_get_host_name(issuer),
                 MC_smx_process_get_name(issuer),
                 type);
-  }
   xbt_free(args);
   return str;
 }
   xbt_free(args);
   return str;
 }
index 5d3c23a..4047f13 100644 (file)
@@ -112,9 +112,8 @@ int MC_modelcheck_safety(void)
       XBT_DEBUG("Execute: %s", req_str);
       xbt_free(req_str);
 
       XBT_DEBUG("Execute: %s", req_str);
       xbt_free(req_str);
 
-      if (dot_output != nullptr) {
+      if (dot_output != nullptr)
         req_str = MC_request_get_dot_output(req, value);
         req_str = MC_request_get_dot_output(req, value);
-      }
 
       MC_state_set_executed_request(state, req, value);
       mc_stats->executed_transitions++;
 
       MC_state_set_executed_request(state, req, value);
       mc_stats->executed_transitions++;
@@ -147,12 +146,9 @@ int MC_modelcheck_safety(void)
         if (dot_output != nullptr)
           std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
 
         if (dot_output != nullptr)
           std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
 
-      } else {
-
-        if (dot_output != nullptr)
-          std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
+      } else if (dot_output != nullptr)
+        std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
 
 
-      }
 
       xbt_fifo_unshift(mc_stack, next_state);
 
 
       xbt_fifo_unshift(mc_stack, next_state);
 
@@ -173,12 +169,9 @@ int MC_modelcheck_safety(void)
         else
           XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num);
 
         else
           XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num);
 
-      } else {
-
+      } else
         XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack) + 1);
 
         XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack) + 1);
 
-      }
-
       /* Trash the current state, no longer needed */
       xbt_fifo_shift(mc_stack);
       XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
       /* Trash the current state, no longer needed */
       xbt_fifo_shift(mc_stack);
       XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
index 409834a..07f11b8 100644 (file)
@@ -212,12 +212,10 @@ int MC_smpi_process_count(void)
 {
   if (mc_mode == MC_MODE_CLIENT)
     return smpi_process_count();
 {
   if (mc_mode == MC_MODE_CLIENT)
     return smpi_process_count();
-  else {
-    int res;
-    mc_model_checker->process().read_variable("process_count",
-      &res, sizeof(res));
-    return res;
-  }
+  int res;
+  mc_model_checker->process().read_variable("process_count",
+    &res, sizeof(res));
+  return res;
 }
 #endif
 
 }
 #endif
 
index d39fbf7..eb9e92d 100644 (file)
@@ -41,15 +41,12 @@ mc_mem_region_t mc_get_snapshot_region(
     if (region->storage_type() == simgrid::mc::StorageType::Privatized) {
 #ifdef HAVE_SMPI
       // Use the current process index of the snapshot:
     if (region->storage_type() == simgrid::mc::StorageType::Privatized) {
 #ifdef HAVE_SMPI
       // Use the current process index of the snapshot:
-      if (process_index == simgrid::mc::ProcessIndexDisabled) {
+      if (process_index == simgrid::mc::ProcessIndexDisabled)
         process_index = snapshot->privatization_index;
         process_index = snapshot->privatization_index;
-      }
-      if (process_index < 0) {
+      if (process_index < 0)
         xbt_die("Missing process index");
         xbt_die("Missing process index");
-      }
-      if (process_index >= (int) region->privatized_data().size()) {
+      if (process_index >= (int) region->privatized_data().size())
         xbt_die("Invalid process index");
         xbt_die("Invalid process index");
-      }
       simgrid::mc::RegionSnapshot& priv_region = region->privatized_data()[process_index];
       xbt_assert(priv_region.contain(simgrid::mc::remote(addr)));
       return &priv_region;
       simgrid::mc::RegionSnapshot& priv_region = region->privatized_data()[process_index];
       xbt_assert(priv_region.contain(simgrid::mc::remote(addr)));
       return &priv_region;
@@ -82,9 +79,8 @@ const void* MC_region_read_fragmented(mc_mem_region_t region, void* target, cons
 
   void* dest = target;
 
 
   void* dest = target;
 
-  if (dest==nullptr) {
+  if (dest==nullptr)
     xbt_die("Missing destination buffer for fragmented memory access");
     xbt_die("Missing destination buffer for fragmented memory access");
-  }
 
   // Read each page:
   while (mc_page_number(nullptr, addr) != page_end) {
 
   // Read each page:
   while (mc_page_number(nullptr, addr) != page_end) {
@@ -127,11 +123,10 @@ int MC_snapshot_region_memcmp(
   const void* buffer1 = MC_region_read(region1, buffer1a, addr1, size);
   const void* buffer2 = MC_region_read(region2, buffer2a, addr2, size);
   int res;
   const void* buffer1 = MC_region_read(region1, buffer1a, addr1, size);
   const void* buffer2 = MC_region_read(region2, buffer2a, addr2, size);
   int res;
-  if (buffer1 == buffer2) {
+  if (buffer1 == buffer2)
     res = 0;
     res = 0;
-  } else {
+  else
     res = memcmp(buffer1, buffer2, size);
     res = memcmp(buffer1, buffer2, size);
-  }
   if (!stack_alloc) {
     free(buffer1a);
     free(buffer2a);
   if (!stack_alloc) {
     free(buffer1a);
     free(buffer2a);
index 726294f..566d98d 100644 (file)
@@ -54,9 +54,8 @@ mc_state_t MC_state_new()
  * \param trans The state to be deleted
  */
 void MC_state_delete(mc_state_t state, int free_snapshot){
  * \param trans The state to be deleted
  */
 void MC_state_delete(mc_state_t state, int free_snapshot){
-  if (state->system_state && free_snapshot){
+  if (state->system_state && free_snapshot)
     delete state->system_state;
     delete state->system_state;
-  }
   if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
     xbt_free(state->index_comm);
     xbt_free(state->incomplete_comm_pattern);
   if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
     xbt_free(state->index_comm);
     xbt_free(state->incomplete_comm_pattern);
@@ -81,13 +80,10 @@ void MC_state_remove_interleave_process(mc_state_t state, smx_process_t process)
 unsigned int MC_state_interleave_size(mc_state_t state)
 {
   unsigned int i, size = 0;
 unsigned int MC_state_interleave_size(mc_state_t state)
 {
   unsigned int i, size = 0;
-
-  for (i = 0; i < state->max_pid; i++) {
+  for (i = 0; i < state->max_pid; i++)
     if ((state->proc_status[i].state == MC_INTERLEAVE)
         || (state->proc_status[i].state == MC_MORE_INTERLEAVE))
       size++;
     if ((state->proc_status[i].state == MC_INTERLEAVE)
         || (state->proc_status[i].state == MC_MORE_INTERLEAVE))
       size++;
-  }
-
   return size;
 }
 
   return size;
 }
 
@@ -154,7 +150,7 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req,
   case SIMCALL_MC_RANDOM: {
     state->internal_req = *req;
     int random_max = simcall_mc_random__get__max(req);
   case SIMCALL_MC_RANDOM: {
     state->internal_req = *req;
     int random_max = simcall_mc_random__get__max(req);
-    if (value != random_max) {
+    if (value != random_max)
       for (auto& p : mc_model_checker->process().simix_processes()) {
         mc_procstate_t procstate = &state->proc_status[p.copy.pid];
         const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
       for (auto& p : mc_model_checker->process().simix_processes()) {
         mc_procstate_t procstate = &state->proc_status[p.copy.pid];
         const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
@@ -163,7 +159,6 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req,
           break;
         }
       }
           break;
         }
       }
-    }
     break;
   }
 
     break;
   }
 
@@ -224,13 +219,12 @@ static inline smx_simcall_t MC_state_get_request_for_process(
         *value = -1;
         while (procstate->interleave_count <
                 read_length(mc_model_checker->process(),
         *value = -1;
         while (procstate->interleave_count <
                 read_length(mc_model_checker->process(),
-                  remote(simcall_comm_testany__get__comms(&process->simcall)))) {
+                  remote(simcall_comm_testany__get__comms(&process->simcall))))
           if (MC_request_is_enabled_by_idx
               (&process->simcall, procstate->interleave_count++)) {
             *value = procstate->interleave_count - 1;
             break;
           }
           if (MC_request_is_enabled_by_idx
               (&process->simcall, procstate->interleave_count++)) {
             *value = procstate->interleave_count - 1;
             break;
           }
-        }
 
         if (procstate->interleave_count >=
             read_length(mc_model_checker->process(),
 
         if (procstate->interleave_count >=
             read_length(mc_model_checker->process(),
@@ -248,15 +242,13 @@ static inline smx_simcall_t MC_state_get_request_for_process(
         s_smx_synchro_t act;
         mc_model_checker->process().read_bytes(
           &act, sizeof(act), remote(remote_act));
         s_smx_synchro_t act;
         mc_model_checker->process().read_bytes(
           &act, sizeof(act), remote(remote_act));
-        if (act.comm.src_proc && act.comm.dst_proc) {
+        if (act.comm.src_proc && act.comm.dst_proc)
           *value = 0;
           *value = 0;
-        } else {
-          if (act.comm.src_proc == nullptr && act.comm.type == SIMIX_COMM_READY
+        else if (act.comm.src_proc == nullptr && act.comm.type == SIMIX_COMM_READY
               && act.comm.detached == 1)
               && act.comm.detached == 1)
-            *value = 0;
-          else
-            *value = -1;
-        }
+          *value = 0;
+        else
+          *value = -1;
         procstate->state = MC_DONE;
         return &process->simcall;
       }
         procstate->state = MC_DONE;
         return &process->simcall;
       }
@@ -264,10 +256,8 @@ static inline smx_simcall_t MC_state_get_request_for_process(
       case SIMCALL_MC_RANDOM:
         if (procstate->state == MC_INTERLEAVE)
           *value = simcall_mc_random__get__min(&process->simcall);
       case SIMCALL_MC_RANDOM:
         if (procstate->state == MC_INTERLEAVE)
           *value = simcall_mc_random__get__min(&process->simcall);
-        else {
-          if (state->req_num < simcall_mc_random__get__max(&process->simcall))
-            *value = state->req_num + 1;
-        }
+        else if (state->req_num < simcall_mc_random__get__max(&process->simcall))
+          *value = state->req_num + 1;
         procstate->state = MC_DONE;
         return &process->simcall;
 
         procstate->state = MC_DONE;
         return &process->simcall;