0

我正在编写程序但收到此警告！有人可以在这方面帮助我。

#include <stdio.h>
#include <stdlib.h>

typedef int bool;
#define true 1
#define false 0


#define M 5                 // Define total molecules 
#define MAX 31               // used to Create a range 
#define N 6              // Define total nodes in the given graph


unsigned int nondet_uint();   // returns a non_deterministic uint

typedef unsigned __CPROVER_bitvector[M] bitvector; 

//constrains the non_detrministic uint to be between 0 and n
unsigned int oneTon (unsigned int n){  
unsigned int result = nondet_uint();
   __CPROVER_assume(result>=1 && result<=n);
      return result;
};

//Constrain the value between 0 and 1
unsigned int  nondet (){  
unsigned int num = nondet_uint();
__CPROVER_assume( num>= 0 && num  <= 1);
return num;
 };


//Define a structure to represent the EdgeBag that is a tuple :
// edgeBag := (i,j,edgeWeight, mask, inclusionSet, exclusionSet)
struct EdgeBag
 {
  int ith;
  int jth;
  bitvector edgeWeight;
  bitvector mask;
  bitvector inclusionSet;
  bitvector exclusionSet;
 };


 // Setweight function
// Going to give the edges the weight and then allow furture   calculation of inclusion and exclusion set 

bitvector setWeight( bitvector node) {
     bitvector edge;
     edge = 00000;
     for(unsigned int k=0; k<N; k++){
         if ((node & (00001 << k)) == (00001 << k)) {
                edge =  (edge |  (nondet() << k));
           } 
     }
     printf("value of the egde is %d", edge);
     return edge;
}

void main(){

unsigned int pos , i, j, k, l, v, w, x, y , iVal, jVal;
unsigned int edgePos, bagNo = 0, colorNode = 0 , minColor, len = 0, cPos = 0;
bool C0 , C1 , C2 , C3; 

bitvector compartment1 , compartment2 , compartment3 , compartment4, compartment5, compartment6;
bitvector nodes[N] = {compartment1, compartment2, compartment3, compartment4, compartment5, compartment6};
bitvector  total , fareTotal, outTotal, inTotal;


// Represent the graph with given topology 
bool graph[N][N] = {{0, 0, 1, 1, 0, 0 },
                    {1, 0, 0, 0, 0, 0},
                    {0, 1, 0, 0, 0, 0},
                    {0, 0, 1, 0, 1, 0},
                    {0, 0, 0, 0, 0, 1},
                    {0, 1, 0, 0, 0, 0}
   };


// Specify that all compartments are distinct  
  for(i=0; i<N; i++) {
      for(j=0 ; j < N ; j++) {
          if(graph[i][j] == 1) {
              len = len + 1;
           }
          if(i != j) {
              __CPROVER_assume(nodes[i] != nodes[j]);
          }
      }
  }

 // Create a structure that will contain edges. 
  struct EdgeBag edgeBag[len];

 // Define colorGraph and colorSet for the represetaion
  bool colorGraph[len][len];
  unsigned int colorSet[len];


 // Set the weight of the edge : for each edge in the graph call add to the esdge bag and add its edgeweight 
 // setWeight function and allow all possible subsets to move from a node to anotheer 
 // Set ith jth position and edgeweight to the position of edgeBag[len] array 
 edgePos = 0;
 for(i=0; i<N; i++) {
     for(j=0; j<N; j++) {
          if (graph[i][j] == 1) {
              edgeBag[edgePos].ith = i;
              edgeBag[edgePos].jth = j;

             **HERE IS THE PROBLEM !!!**
              edgeBag[edgePos].edgeWeight  = setWeight(nodes[i]);

              edgePos = edgePos + 1;
          }
     }
}

我知道当编译器在函数使用之前没有看到声明时会出现此警告。但是我已经声明了 setWeight 函数并且看起来类型太匹配了。请帮帮我，从昨晚开始我就被困在这里了。谢谢

4

1 回答 1

1

你的函数需要位向量 -bitvector setWeight( bitvector node)

但得到位向量[] -

bitvector nodes[N] = {...};

...

[edgePos].edgeWeight = setWeight(nodes);

于 2015-10-22T06:45:44.120 回答