alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

[buddy] Fix several PVS-Studio warnings

Browse source 
For #192.

* src/bddio.c, src/cppext.cxx, src/kernel.c: Fix printf formats, calls
to new, and simplify one check in bdd_delref_nc().
This commit is contained in:
Alexandre Duret-Lutz 2016-10-28 17:12:21 +02:00
parent 41b47966b0
commit 63818a3e69
3 changed files with 12 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

2
buddy/src/bddio.c
View file

@ -130,7 +130,7 @@ void bdd_fprintall(FILE *ofile)
{ {
if (LOW(n) != -1) if (LOW(n) != -1)
{ {
fprintf(ofile, "[%5d - %2d] ", n, bddnodes[n].refcou); fprintf(ofile, "[%5d - %2u] ", n, bddnodes[n].refcou);
if (filehandler) if (filehandler)
filehandler(ofile, bddlevel2var[LEVEL(n)]); filehandler(ofile, bddlevel2var[LEVEL(n)]);
else else

5
buddy/src/cppext.cxx
View file

@ -37,6 +37,7 @@
#include <string.h> #include <string.h>
#include <stdlib.h> #include <stdlib.h>
#include <iomanip> #include <iomanip>
#include <new>
#include "kernel.h" #include "kernel.h"
#include "bvecx.h" #include "bvecx.h"
@ -190,7 +191,7 @@ ostream &operator<<(ostream &o, const bdd &r)
return o; return o;
} }
int *set = new int[bddvarnum]; int *set = new (std::nothrow) int[bddvarnum];
if (set == NULL) if (set == NULL)
{ {
bdd_error(BDD_MEMORY); bdd_error(BDD_MEMORY);
@ -252,7 +253,7 @@ ostream &operator<<(ostream &o, const bdd &r)
return o; return o;
} }
int *set = new int[bddvarnum]; int *set = new (std::nothrow) int[bddvarnum];
if (set == NULL) if (set == NULL)
{ {
bdd_error(BDD_MEMORY); bdd_error(BDD_MEMORY);

16
buddy/src/kernel.c
View file

@ -774,19 +774,19 @@ void bdd_fprintstat(FILE *ofile)
fprintf(ofile, "\nCache statistics\n"); fprintf(ofile, "\nCache statistics\n");
fprintf(ofile, "----------------\n"); fprintf(ofile, "----------------\n");
fprintf(ofile, "Unique Access: %ld\n", s.uniqueAccess); fprintf(ofile, "Unique Access: %lu\n", s.uniqueAccess);
fprintf(ofile, "Unique Chain: %ld\n", s.uniqueChain); fprintf(ofile, "Unique Chain: %lu\n", s.uniqueChain);
fprintf(ofile, "Unique Hit: %ld\n", s.uniqueHit); fprintf(ofile, "Unique Hit: %lu\n", s.uniqueHit);
fprintf(ofile, "Unique Miss: %ld\n", s.uniqueMiss); fprintf(ofile, "Unique Miss: %lu\n", s.uniqueMiss);
fprintf(ofile, "=> Hit rate = %.2f\n", fprintf(ofile, "=> Hit rate = %.2f\n",
(s.uniqueHit+s.uniqueMiss > 0) ? (s.uniqueHit+s.uniqueMiss > 0) ?
((float)s.uniqueHit)/((float)s.uniqueHit+s.uniqueMiss) : 0); ((float)s.uniqueHit)/((float)s.uniqueHit+s.uniqueMiss) : 0);
fprintf(ofile, "Operator Hits: %ld\n", s.opHit); fprintf(ofile, "Operator Hits: %lu\n", s.opHit);
fprintf(ofile, "Operator Miss: %ld\n", s.opMiss); fprintf(ofile, "Operator Miss: %lu\n", s.opMiss);
fprintf(ofile, "=> Hit rate = %.2f\n", fprintf(ofile, "=> Hit rate = %.2f\n",
(s.opHit+s.opMiss > 0) ? (s.opHit+s.opMiss > 0) ?
((float)s.opHit)/((float)s.opHit+s.opMiss) : 0); ((float)s.opHit)/((float)s.opHit+s.opMiss) : 0);
fprintf(ofile, "Swap count = %ld\n", s.swapCount); fprintf(ofile, "Swap count = %lu\n", s.swapCount);
} }
@ -1164,7 +1164,7 @@ BDD bdd_addref(BDD root)
BDD bdd_delref_nc(BDD root) BDD bdd_delref_nc(BDD root)
{ {
#ifndef NDEBUG #ifndef NDEBUG
if (root < 2 || !bddrunning) if (!bddrunning)
return root; return root;
if (root >= bddnodesize) if (root >= bddnodesize)
return bdd_error(BDD_ILLBDD); return bdd_error(BDD_ILLBDD);