Skip to content

Inconsistent results for properties that introduce several error locations #418

Open
@Heizmann

Description

@Heizmann

Some C properties are translated into several error locations (e.g., memsafety).
If only some of the error locations are reachable and we do not stop after the first violation was found, we report that the property holds and that the property does not hold.

A less severe symptom of this problem is that we sometimes report several positive results for the same property.

A solution:
Let baktranslation merge results.

Metadata

Metadata

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions