Creating a separate issue for the leftover from #527 as this is not really a data race analysis issue, rather a problem with flat memory encoding.
pthread-complex/elimination_backoff_stack.yml wrong verdict: likely a memory encoding issue. It is parsed with the flat memory model.
Command to reproduce:
--property-value DATA_RACE --loglevel INFO --prunestrategy FULL --search DFS --refinement SEQ_ITP --stacktrace --maxenum 1 --predsplit WHOLE --lbe LBE_LOCAL --input /mnt/d/Theta/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.yml --domain PRED_CART --por SPOR --coi NO_COI --memory-model flat
Detailed issue:
We have these declarations, and a variable practically defined as ThreadInfo *ti = threads[0];
struct Cell {
Cell *pnext;
int pdata;
};
typedef struct ThreadInfo ThreadInfo;
struct ThreadInfo {
unsigned int id;
int op;
Cell cell;
};
ThreadInfo threads[4];
int PushOpen[2];
Our memory encoding allows ti->cell to point to the same location in the memory as PushOpen causing a data race for example for accesses ti->cell.pdata and PushOpen[1] (both having the same offset after the incorrectly allowed same base).
Creating a separate issue for the leftover from #527 as this is not really a data race analysis issue, rather a problem with flat memory encoding.
pthread-complex/elimination_backoff_stack.ymlwrong verdict: likely a memory encoding issue. It is parsed with the flat memory model.Command to reproduce:
--property-value DATA_RACE --loglevel INFO --prunestrategy FULL --search DFS --refinement SEQ_ITP --stacktrace --maxenum 1 --predsplit WHOLE --lbe LBE_LOCAL --input /mnt/d/Theta/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.yml --domain PRED_CART --por SPOR --coi NO_COI --memory-model flatDetailed issue:
We have these declarations, and a variable practically defined as ThreadInfo *ti = threads[0];
struct Cell {
Cell *pnext;
int pdata;
};
typedef struct ThreadInfo ThreadInfo;
struct ThreadInfo {
unsigned int id;
int op;
Cell cell;
};
ThreadInfo threads[4];
int PushOpen[2];
Our memory encoding allows ti->cell to point to the same location in the memory as PushOpen causing a data race for example for accesses ti->cell.pdata and PushOpen[1] (both having the same offset after the incorrectly allowed same base).