Commit 5b8fa41b by Alan Mishchenko

Suggested bug fixes in the old code.

parent d892e632
...@@ -1333,7 +1333,7 @@ void Aig_ManCounterExampleValueStart( Aig_Man_t * pAig, Abc_Cex_t * pCex ) ...@@ -1333,7 +1333,7 @@ void Aig_ManCounterExampleValueStart( Aig_Man_t * pAig, Abc_Cex_t * pCex )
pAig->pData2 = ABC_CALLOC( unsigned, Abc_BitWordNum( (pCex->iFrame + 1) * Aig_ManObjNumMax(pAig) ) ); pAig->pData2 = ABC_CALLOC( unsigned, Abc_BitWordNum( (pCex->iFrame + 1) * Aig_ManObjNumMax(pAig) ) );
// the register values in the counter-example should be zero // the register values in the counter-example should be zero
Saig_ManForEachLo( pAig, pObj, k ) Saig_ManForEachLo( pAig, pObj, k )
assert( Abc_InfoHasBit(pCex->pData, iBit++) == 0 ); assert( Abc_InfoHasBit(pCex->pData, iBit) == 0 ), iBit++;
// iterate through the timeframes // iterate through the timeframes
nObjs = Aig_ManObjNumMax(pAig); nObjs = Aig_ManObjNumMax(pAig);
for ( i = 0; i <= pCex->iFrame; i++ ) for ( i = 0; i <= pCex->iFrame; i++ )
......
...@@ -195,7 +195,7 @@ void Gia_ManCounterExampleValueStart( Gia_Man_t * pGia, Abc_Cex_t * pCex ) ...@@ -195,7 +195,7 @@ void Gia_ManCounterExampleValueStart( Gia_Man_t * pGia, Abc_Cex_t * pCex )
pGia->pData2 = ABC_CALLOC( unsigned, Abc_BitWordNum( (pCex->iFrame + 1) * Gia_ManObjNum(pGia) ) ); pGia->pData2 = ABC_CALLOC( unsigned, Abc_BitWordNum( (pCex->iFrame + 1) * Gia_ManObjNum(pGia) ) );
// the register values in the counter-example should be zero // the register values in the counter-example should be zero
Gia_ManForEachRo( pGia, pObj, k ) Gia_ManForEachRo( pGia, pObj, k )
assert( Abc_InfoHasBit(pCex->pData, iBit++) == 0 ); assert( Abc_InfoHasBit(pCex->pData, iBit) == 0 ), iBit++;
// iterate through the timeframes // iterate through the timeframes
nObjs = Gia_ManObjNum(pGia); nObjs = Gia_ManObjNum(pGia);
for ( i = 0; i <= pCex->iFrame; i++ ) for ( i = 0; i <= pCex->iFrame; i++ )
......
...@@ -438,7 +438,7 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck ) ...@@ -438,7 +438,7 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
// read the file into the buffer // read the file into the buffer
nFileSize = Ioa_FileSize( pFileName ); nFileSize = Ioa_FileSize( pFileName );
pFile = fopen( pFileName, "rb" ); pFile = fopen( pFileName, "rb" );
pContents = ABC_ALLOC( char, nFileSize ); pContents = ABC_CALLOC( char, nFileSize+1 );
RetValue = fread( pContents, nFileSize, 1, pFile ); RetValue = fread( pContents, nFileSize, 1, pFile );
fclose( pFile ); fclose( pFile );
......
...@@ -1034,7 +1034,7 @@ static word * Ses_ManDeriveTruth( Ses_Man_t * pSes, char * pSol, int fInvert ) ...@@ -1034,7 +1034,7 @@ static word * Ses_ManDeriveTruth( Ses_Man_t * pSes, char * pSol, int fInvert )
for ( i = 0; i < nGates; ++i ) for ( i = 0; i < nGates; ++i )
{ {
f = *p++; f = *p++;
assert( *p++ == 2 ); assert( *p == 2 ), p++;
j = *p++; j = *p++;
k = *p++; k = *p++;
......
...@@ -800,7 +800,7 @@ void Wlc_NtkTrace_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int iFrame, Vec_Int_t * ...@@ -800,7 +800,7 @@ void Wlc_NtkTrace_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int iFrame, Vec_Int_t *
{ {
int Index = 3*(iFrame*Vec_IntSize(vMemObjs) + iNum); int Index = 3*(iFrame*Vec_IntSize(vMemObjs) + iNum);
int Value = (int)Vec_WrdEntry( vValues, Index ); int Value = (int)Vec_WrdEntry( vValues, Index );
assert( Value == 0 && Value == 1 ); assert( Value == 0 || Value == 1 );
Wlc_NtkTrace_rec( p, Value ? Wlc_ObjFanin2(p, pObj) : Wlc_ObjFanin1(p, pObj), iFrame, vMemObjs, vValues, ValueA, vRes ); Wlc_NtkTrace_rec( p, Value ? Wlc_ObjFanin2(p, pObj) : Wlc_ObjFanin1(p, pObj), iFrame, vMemObjs, vValues, ValueA, vRes );
Vec_IntPush( vRes, (iObj << 11) | (iFrame << 1) | Value ); Vec_IntPush( vRes, (iObj << 11) | (iFrame << 1) | Value );
} }
......
...@@ -278,15 +278,14 @@ Abc_Lit2Var(iFan2), (Abc_LitIsCompl(iFan2)?'-':'+') ); ...@@ -278,15 +278,14 @@ Abc_Lit2Var(iFan2), (Abc_LitIsCompl(iFan2)?'-':'+') );
int ** Amap_LibLookupTableAlloc( Vec_Ptr_t * vVec, int fVerbose ) int ** Amap_LibLookupTableAlloc( Vec_Ptr_t * vVec, int fVerbose )
{ {
Vec_Int_t * vOne; Vec_Int_t * vOne;
int ** pRes, * pBuffer; int ** pRes;
int i, k, nTotal, nSize, nEntries, Value; int i, k, nTotal, nSize, nEntries, Value;
// count the total size // count the total size
nEntries = nSize = Vec_PtrSize( vVec ); nEntries = nSize = Vec_PtrSize( vVec );
Vec_PtrForEachEntry( Vec_Int_t *, vVec, vOne, i ) Vec_PtrForEachEntry( Vec_Int_t *, vVec, vOne, i )
nEntries += Vec_IntSize(vOne); nEntries += Vec_IntSize(vOne);
pBuffer = ABC_ALLOC( int, nSize * sizeof(void *) + nEntries ); pRes = (int **)ABC_ALLOC( char, nSize * sizeof(void *) + nEntries * sizeof(int) );
pRes = (int **)pBuffer; pRes[0] = (int *)((char *)pRes + nSize * sizeof(void *));
pRes[0] = pBuffer + nSize * sizeof(void *);
nTotal = 0; nTotal = 0;
Vec_PtrForEachEntry( Vec_Int_t *, vVec, vOne, i ) Vec_PtrForEachEntry( Vec_Int_t *, vVec, vOne, i )
{ {
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment