Skip to content

Fix for the propertyfile of the MemSafety-MemCleanup subcategory

versokova requested to merge valid-memcleanup into main

After Tuesday's discussion I realized that valid-memcleanup.prp is incorrect. It should check all three properties (one stronger than in memsafety). Otherwise, this could lead to undefined behavior and the task should not be considered memory safe. It is obvious that there are no such tasks in the benchmark (only one property can be violated). So the solution looks like this:

CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memcleanup) )

Merge request reports