utwente-fmt / vercors

The VerCors verification toolset for verifying parallel and concurrent software
https://utwente.nl/vercors
Mozilla Public License 2.0
58 stars 26 forks source link

Make contract of free (for C) conditional on ptr being non-null #1250

Closed wandernauta closed 2 months ago

wandernauta commented 2 months ago

In C, passing NULL to free has no effect. This change weakens the precondition on the argument to free so that it only applies if the pointer is non-null, so this program now verifies:

  #include <stdlib.h>
  int main(){
      int* xs = NULL;
      free(xs);
      free(xs);
      free(xs);
  }

Adds test; changes existing test; fixes #1240. As @bobismijnnaam mentioned in that issue, this does introduce a number of branches - the hope there was that this "would not influence verification significantly", but I'm not sure how to check this; the existing examples seem to be okay, but those are quite small.