From a2f174f7212ddafeefcc9b67a3ed6c6195e83a27 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 1 Feb 2017 15:09:40 +0100
Subject: [PATCH] [buddy] fix some -Wpedantic messages

* src/bddop.c: Empty macro arguments are undefined ISO C90 and
ISO C++98.  Use '+' when calling APPLY_SHORTCUTS.
* src/fdd.c, src/kernel.c: Avoid constructs invalid in C90.
* src/bddop.c, src/bddx.h, src/kernel.c, src/kernel.h,
examples/cmilner/cmilner.c: Remove C++ comments.
---
 buddy/examples/cmilner/cmilner.c |  2 +-
 buddy/src/bddop.c                | 14 ++---
 buddy/src/bddx.h                 |  7 +--
 buddy/src/fdd.c                  | 21 +++++---
 buddy/src/kernel.c               | 93 +++++++++++++++++---------------
 buddy/src/kernel.h               |  4 +-
 6 files changed, 79 insertions(+), 62 deletions(-)

diff --git a/buddy/examples/cmilner/cmilner.c b/buddy/examples/cmilner/cmilner.c
index ba6dafa3f..b68fc175c 100644
--- a/buddy/examples/cmilner/cmilner.c
+++ b/buddy/examples/cmilner/cmilner.c
@@ -214,7 +214,7 @@ static int has_deadlocks(bdd R, bdd T)
 
    for(int i=0; i<N; i++)
       C &= bdd_exist(T, primvar, N*3);
-   //C &= bdd_exist(bdd_exist(bdd_exist(T,i*6+3),i*6+5),i*6+1);
+   /* C &= bdd_exist(bdd_exist(bdd_exist(T,i*6+3),i*6+5),i*6+1); */
 
    if(C != bddfalse && R != bddfalse)
       return 0;
diff --git a/buddy/src/bddop.c b/buddy/src/bddop.c
index b77de0660..c01513e81 100644
--- a/buddy/src/bddop.c
+++ b/buddy/src/bddop.c
@@ -676,7 +676,9 @@ static BDD apply_rec(BDD l, BDD r)
        break;                                           \
      }
 
-   APPLY_SHORTCUTS(applyop, /* id */);
+   /* empty macro arguments are undefined in ISO C90 and ISO C++98, so
+      use + when we do not want to call any function.*/
+   APPLY_SHORTCUTS(applyop, +);
 
    if (__unlikely(ISCONST(l)  &&  ISCONST(r)))
       res = oprres[applyop][l<<1 | r];
@@ -684,7 +686,7 @@ static BDD apply_rec(BDD l, BDD r)
    {
       entry = BddCache_lookup(&applycache, APPLYHASH(l,r,applyop));
 
-      // Check entry->c last, because not_rec() does not initialize it.
+      /* Check entry->c last, because not_rec() does not initialize it. */
       if (entry->i.a == l  &&  entry->i.c == applyop  &&  entry->i.b == r)
       {
 #ifdef CACHESTATS
@@ -928,7 +930,7 @@ int bdd_implies(BDD l, BDD r)
     return 0;
 
   entry = BddCache_lookup(&misccache, IMPLIESHASH(l,r));
-   // Check entry->b last, because not_rec() does not initialize it.
+  /* Check entry->b last, because not_rec() does not initialize it. */
   if (entry->i.a == l && entry->i.c == CACHEID_IMPLIES && entry->i.b == r)
    {
 #ifdef CACHESTATS
@@ -944,8 +946,8 @@ int bdd_implies(BDD l, BDD r)
     {
       int hl = HIGH(l);
       int hr = HIGH(r);
-      // Avoid the recursion if the second implication will trivially
-      // fail.
+      /* Avoid the recursion if the second implication will trivially
+         fail. */
       if ((ISONE(hl) || ISZERO(hr)) && (hl != hr))
         res = 0;
       else
@@ -1792,7 +1794,7 @@ static BDD simplify_rec(BDD f, BDD d)
 
    entry = BddCache_lookup(&applycache, APPLYHASH(f,d,bddop_simplify));
 
-   // Check entry->b last, because not_rec() does not initialize it.
+   /* Check entry->b last, because not_rec() does not initialize it. */
    if (entry->i.a == f && entry->i.c == bddop_simplify && entry->i.b == d)
    {
 #ifdef CACHESTATS
diff --git a/buddy/src/bddx.h b/buddy/src/bddx.h
index 84bd066b0..a1d80f61c 100644
--- a/buddy/src/bddx.h
+++ b/buddy/src/bddx.h
@@ -68,9 +68,10 @@
   #endif
 #endif
 
-// BUDDY_API is used for the public API symbols. It either DLL imports
-// or DLL exports (or does nothing for static build) BUDDY_LOCAL is
-// used for non-api symbols.
+/* BUDDY_API is used for the public API symbols. It either DLL imports
+** or DLL exports (or does nothing for static build) BUDDY_LOCAL is
+** used for non-api symbols.
+*/
 #ifdef BUDDY_DLL
   #ifdef BUDDY_DLL_EXPORTS
     #define BUDDY_API BUDDY_HELPER_DLL_EXPORT
diff --git a/buddy/src/fdd.c b/buddy/src/fdd.c
index 2142d9498..46c1ba758 100644
--- a/buddy/src/fdd.c
+++ b/buddy/src/fdd.c
@@ -143,10 +143,13 @@ int fdd_extdomain(int *dom, int num)
       {
          fdvaralloc += (num > fdvaralloc) ? num : fdvaralloc;
 
-	 Domain* tmp_ptr = (Domain*)realloc(domain, sizeof(Domain)*fdvaralloc);
-	 if (tmp_ptr == NULL)
-	    return bdd_error(BDD_MEMORY);
-	 domain = tmp_ptr;
+         {
+           Domain* tmp_ptr =
+             (Domain*)realloc(domain, sizeof(Domain)*fdvaralloc);
+           if (tmp_ptr == NULL)
+             return bdd_error(BDD_MEMORY);
+           domain = tmp_ptr;
+         }
       }
    }
 
@@ -220,10 +223,12 @@ int fdd_overlapdomain(int v1, int v2)
    {
       fdvaralloc += fdvaralloc;
 
-      Domain* tmp_ptr = (Domain*)realloc(domain, sizeof(Domain)*fdvaralloc);
-      if (tmp_ptr == NULL)
-	 return bdd_error(BDD_MEMORY);
-      domain = tmp_ptr;
+      {
+        Domain* tmp_ptr = (Domain*)realloc(domain, sizeof(Domain)*fdvaralloc);
+        if (tmp_ptr == NULL)
+          return bdd_error(BDD_MEMORY);
+        domain = tmp_ptr;
+      }
    }
 
    d = &domain[fdvarnum];
diff --git a/buddy/src/kernel.c b/buddy/src/kernel.c
index 09ece7e5b..b414de1c4 100644
--- a/buddy/src/kernel.c
+++ b/buddy/src/kernel.c
@@ -194,20 +194,21 @@ int bdd_init(int initnodesize, int cs)
 
    /* Load these globals into local variables to help the
       optimizer. */
-   int sz = bddnodesize;
-   BddNodeInit* b = (BddNodeInit*)bddnodes;
-   for (n=0 ; n<sz ; n++)
    {
-     b[n].z = 0;
-     b[n].low = -1;
-     // Initializing HIGH is useless in BuDDy, but it helps the
-     // compiler vectorizing the code, and it helps the processor
-     // write-combining data to memory.
-     b[n].high = 0;
-     b[n].next = n+1;
+     int sz = bddnodesize;
+     BddNodeInit* b = (BddNodeInit*)bddnodes;
+     for (n=0 ; n<sz ; n++)
+       {
+         b[n].z = 0;
+         b[n].low = -1;
+         /* Initializing HIGH is useless in BuDDy, but it helps the
+            compiler vectorizing the code, and it helps the processor
+            write-combining data to memory. */
+         b[n].high = 0;
+         b[n].next = n+1;
+       }
+     b[sz-1].next = 0;
    }
-   b[sz-1].next = 0;
-
    bddnodes[0].refcou = bddnodes[1].refcou = MAXREF;
    LOW(0) = HIGH(0) = 0;
    LOW(1) = HIGH(1) = 1;
@@ -341,25 +342,31 @@ int bdd_setvarnum(int num)
    }
    else
    {
-     BDD* tmp_ptr = (BDD*)realloc(bddvarset,sizeof(BDD)*num*2);
-     if (__unlikely(tmp_ptr == NULL))
-       return bdd_error(BDD_MEMORY);
-     bddvarset = tmp_ptr;
-     int* tmp_ptr2 = (int*)realloc(bddlevel2var,sizeof(int)*(num+1));
-     if (__unlikely(tmp_ptr2 == NULL))
-       {
-	 free(bddvarset);
-	 return bdd_error(BDD_MEMORY);
-       }
-     bddlevel2var = tmp_ptr2;
-     tmp_ptr2 = (int*)realloc(bddvar2level,sizeof(int)*(num+1));
-     if (__unlikely(tmp_ptr2 == NULL))
-      {
-	 free(bddvarset);
-	 free(bddlevel2var);
-	 return bdd_error(BDD_MEMORY);
-      }
-     bddvar2level = tmp_ptr2;
+     {
+       BDD* tmp_ptr = (BDD*)realloc(bddvarset,sizeof(BDD)*num*2);
+       if (__unlikely(tmp_ptr == NULL))
+         return bdd_error(BDD_MEMORY);
+       bddvarset = tmp_ptr;
+     }
+     {
+       int* tmp_ptr2 = (int*)realloc(bddlevel2var,sizeof(int)*(num+1));
+       if (__unlikely(tmp_ptr2 == NULL))
+         {
+           free(bddvarset);
+           return bdd_error(BDD_MEMORY);
+         }
+       bddlevel2var = tmp_ptr2;
+     }
+     {
+       int* tmp_ptr2 = (int*)realloc(bddvar2level,sizeof(int)*(num+1));
+       if (__unlikely(tmp_ptr2 == NULL))
+         {
+           free(bddvarset);
+           free(bddlevel2var);
+           return bdd_error(BDD_MEMORY);
+         }
+       bddvar2level = tmp_ptr2;
+     }
    }
 
    if (__likely(bddrefstack != NULL))
@@ -1162,7 +1169,7 @@ BDD bdd_addref(BDD root)
    return root;
 }
 
-// Non constant version
+/* Non constant version */
 BDD bdd_delref_nc(BDD root)
 {
 #ifndef NDEBUG
@@ -1448,18 +1455,20 @@ int bdd_noderesize(int doRehash)
 
    /* copy these global variables into local variables to help the
       optimizer */
-   int sz = bddnodesize;
-   BddNodeInit* b = (BddNodeInit*)(bddnodes);
-   for (n=oldsize ; n<sz ; n++)
    {
-     b[n].z = 0;
-     b[n].low = -1;
-     b[n].high = 0;
-     b[n].next = n+1;
+     int sz = bddnodesize;
+     BddNodeInit* b = (BddNodeInit*)(bddnodes);
+     for (n=oldsize ; n<sz ; n++)
+       {
+         b[n].z = 0;
+         b[n].low = -1;
+         b[n].high = 0;
+         b[n].next = n+1;
+       }
+     b[sz-1].next = bddfreepos;
+     bddfreepos = oldsize;
+     bddfreenum += bddnodesize - oldsize;
    }
-   b[sz-1].next = bddfreepos;
-   bddfreepos = oldsize;
-   bddfreenum += bddnodesize - oldsize;
 
    if (doRehash)
       bdd_gbc_rehash();
diff --git a/buddy/src/kernel.h b/buddy/src/kernel.h
index 4f929a624..5ed3d412e 100644
--- a/buddy/src/kernel.h
+++ b/buddy/src/kernel.h
@@ -99,8 +99,8 @@ typedef struct s_BddNode /* Node table entry */
    int next;
 } BddNode;
 
-// This structure is used during initialization of the above
-// structure, to help gcc vectorize the initializing loop.
+/* This structure is used during initialization of the above
+   structure, to help gcc vectorize the initializing loop. */
 typedef struct s_BddNodeInit
 {
    int z;