summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/misc/util/utilBridge.c4
-rw-r--r--src/proof/live/liveness.c18
-rw-r--r--src/proof/live/liveness_sim.c8
3 files changed, 15 insertions, 15 deletions
diff --git a/src/misc/util/utilBridge.c b/src/misc/util/utilBridge.c
index 57372c6a..e48b54df 100644
--- a/src/misc/util/utilBridge.c
+++ b/src/misc/util/utilBridge.c
@@ -202,7 +202,7 @@ void Gia_ManFromBridgeUnknown( FILE * pFile )
}
void Gia_ManFromBridgeCex( FILE * pFile, Abc_Cex_t * pCex )
{
- int i, f, iBit, RetValue;
+ int i, f, iBit;//, RetValue;
Vec_Str_t * vStr = Vec_StrAlloc( 1000 );
Vec_StrPush( vStr, (char)BRIDGE_VALUE_0 ); // false
Vec_StrPush( vStr, (char)1 ); // size of vector (Armin's encoding)
@@ -381,7 +381,7 @@ int Gia_ManFromBridgeReadPackage( FILE * pFile, int * pType, int * pSize, unsign
*pType = atoi( Temp );
*pSize = atoi( Temp + 7 );
- *ppBuffer = ABC_ALLOC( char, *pSize );
+ *ppBuffer = ABC_ALLOC( unsigned char, *pSize );
RetValue = fread( *ppBuffer, *pSize, 1, pFile );
if ( RetValue != 1 && *pSize != 0 )
{
diff --git a/src/proof/live/liveness.c b/src/proof/live/liveness.c
index 8368e121..cc430635 100644
--- a/src/proof/live/liveness.c
+++ b/src/proof/live/liveness.c
@@ -221,7 +221,7 @@ Vec_Ptr_t *vecLos, *vecLoNames;
int Aig_ManPiCleanupBiere( Aig_Man_t * p )
{
- int k = 0, nPisOld = Aig_ManPiNum(p);
+ int nPisOld = Aig_ManPiNum(p);
p->nObjs[AIG_OBJ_PI] = Vec_PtrSize( p->vPis );
if ( Aig_ManRegNum(p) )
@@ -233,7 +233,7 @@ int Aig_ManPiCleanupBiere( Aig_Man_t * p )
int Aig_ManPoCleanupBiere( Aig_Man_t * p )
{
- int k = 0, nPosOld = Aig_ManPoNum(p);
+ int nPosOld = Aig_ManPoNum(p);
p->nObjs[AIG_OBJ_PO] = Vec_PtrSize( p->vPos );
if ( Aig_ManRegNum(p) )
@@ -257,7 +257,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_
Aig_Obj_t *pObjOriginalSafetyPropertyOutput;
Aig_Obj_t *pDriverImage, *pArgument, *collectiveAssertSafety, *collectiveAssumeSafety;
char *nodeName;
- int piCopied = 0, liCopied = 0, loCopied = 0, liCreated = 0, loCreated = 0, piVecIndex = 0, liveLatch = 0, fairLatch = 0;
+ int piCopied = 0, liCopied = 0, loCopied = 0, liCreated = 0, loCreated = 0, liveLatch = 0, fairLatch = 0;
vecPis = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
vecPiNames = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
@@ -545,9 +545,9 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M
Aig_Man_t * pNew;
int i, nRegCount, iEntry;
Aig_Obj_t * pObjSavePi;
- Aig_Obj_t *pObjSavedLo, *pObjSavedLi;
+ Aig_Obj_t *pObjSavedLi, *pObjSavedLo;
Aig_Obj_t *pObj, *pMatch;
- Aig_Obj_t *pObjSaveOrSaved, *pObjSaveAndNotSaved, *pObjSavedLoAndEquality;
+ Aig_Obj_t *pObjSavedLoAndEquality, *pObjSaveOrSaved, *pObjSaveAndNotSaved;
Aig_Obj_t *pObjShadowLo, *pObjShadowLi, *pObjShadowLiDriver;
Aig_Obj_t *pObjXor, *pObjXnor, *pObjAndAcc;
Aig_Obj_t *pObjLive, *pObjFair, *pObjSafetyGate;
@@ -857,7 +857,7 @@ Aig_Man_t * LivenessToSafetyTransformationOneStepLoop( int mode, Abc_Ntk_t * pNt
Aig_Obj_t *collectiveAssertSafety, *collectiveAssumeSafety;
char *nodeName;
- int piCopied = 0, liCopied = 0, loCopied = 0, liCreated = 0, loCreated = 0, piVecIndex = 0;
+ int piCopied = 0, liCopied = 0, loCopied = 0;//, liCreated = 0, loCreated = 0, piVecIndex = 0;
if( Aig_ManRegNum( p ) == 0 )
{
@@ -1814,7 +1814,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A
Aig_Obj_t *pNegatedSafetyConjunction = NULL;
Aig_Obj_t *pObjSafetyAndLiveToSafety;
char *nodeName, *pFormula;
- int piCopied = 0, liCopied = 0, loCopied = 0, liCreated = 0, loCreated = 0, piVecIndex = 0, liveLatch = 0, fairLatch = 0;
+ int piCopied = 0, liCopied = 0, loCopied = 0, liCreated = 0, loCreated = 0, liveLatch = 0;//, piVecIndex = 0, fairLatch = 0;
Vec_Ptr_t *vSignal, *vTopASTNodeArray;
ltlNode *pEnrtyGLOBALLY;
ltlNode *topNodeOfAST, *tempTopASTNode;
@@ -2273,8 +2273,8 @@ int Abc_CommandAbcLivenessToSafetyWithLTL( Abc_Frame_t * pAbc, int argc, char **
int c;
Vec_Ptr_t * vLive, * vFair, *vAssertSafety, *vAssumeSafety;
int directive = -1;
- char *ltfFormulaString = NULL;
- int LTL_FLAG = 0, numOfLtlPropOutput;
+// char *ltfFormulaString = NULL;
+ int numOfLtlPropOutput;//, LTL_FLAG = 0;
Vec_Ptr_t *ltlBuffer;
pNtk = Abc_FrameReadNtk(pAbc);
diff --git a/src/proof/live/liveness_sim.c b/src/proof/live/liveness_sim.c
index 50153e50..c631e187 100644
--- a/src/proof/live/liveness_sim.c
+++ b/src/proof/live/liveness_sim.c
@@ -174,7 +174,7 @@ extern Vec_Ptr_t *vecLos, *vecLoNames;
static int Aig_ManPiCleanupBiere( Aig_Man_t * p )
{
- int k = 0, nPisOld = Aig_ManPiNum(p);
+ int nPisOld = Aig_ManPiNum(p);
p->nObjs[AIG_OBJ_PI] = Vec_PtrSize( p->vPis );
if ( Aig_ManRegNum(p) )
@@ -186,7 +186,7 @@ static int Aig_ManPiCleanupBiere( Aig_Man_t * p )
static int Aig_ManPoCleanupBiere( Aig_Man_t * p )
{
- int k = 0, nPosOld = Aig_ManPoNum(p);
+ int nPosOld = Aig_ManPoNum(p);
p->nObjs[AIG_OBJ_PO] = Vec_PtrSize( p->vPos );
if ( Aig_ManRegNum(p) )
@@ -208,7 +208,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_
Aig_Obj_t *pObjSafetyPropertyOutput;
Aig_Obj_t *pDriverImage;
char *nodeName;
- int piCopied = 0, liCopied = 0, loCopied = 0, liCreated = 0, loCreated = 0, piVecIndex = 0, liveLatch = 0, fairLatch = 0;
+ int piCopied = 0, liCopied = 0, loCopied = 0, liCreated = 0, loCreated = 0, liveLatch = 0, fairLatch = 0;
vecPis = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
vecPiNames = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
@@ -491,7 +491,7 @@ static Aig_Man_t * LivenessToSafetyTransformationOneStepLoopSim( Abc_Ntk_t * pNt
char *nodeName;
- int piCopied = 0, liCopied = 0, loCopied = 0, liCreated = 0, loCreated = 0, piVecIndex = 0;
+ int piCopied = 0, liCopied = 0, loCopied = 0;//, liCreated = 0, loCreated = 0, piVecIndex = 0;
vecPis = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
vecPiNames = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
generated by cgit v1.2.3 (git 2.25.1) at 2025-05-28 20:47:11 +0000