Skip to content

Data race check memory location incomplete dereferences #446

@csanadtelbisz

Description

@csanadtelbisz

Fix incomplete dereferences issue in the solver check of mayBeSameMemoryLocation in XcfaDataRaceCheck.kt (e.g., by wrapping expr in an AssumeStmt in an XcfaAction and getting its statements: it should do the necessary transformation)

e.g., --property-value DATA_RACE --lbe LBE_LOCAL --input sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.yml --maxenum 1 --refinement SEQ_ITP --domain EXPL --por SPOR --prunestrategy FULL --search DFS

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions