Fix for the propertyfile of the MemSafety-MemCleanup subcategory
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) )