[splint-discuss] ensures isnull?

[Tommy Pettersson]

This works:

  #include <stdio.h>
  
  struct test {
          int i;
          /*@null@*/ /*@dependent@*/ char * a;
  };
  
  void test2(struct test * param) /*@ensures isnull param->a @*/ {
          if ( param->a != NULL )
                  param->a = NULL;
          else
                  param->a = NULL;
          return;
  }

So presumably splint does not analyze the logic of alternative
paths for the ensure clause; but instead checks that all
possible paths fulfill the clause.

For example, this is not enough to convince splint:

  void test2(struct test * param) /*@ensures isnull param->a @*/ {
          if ( 1 )
                  param->a = NULL;
          return;
  }


-- 
Tommy Pettersson <ptp at lysator.liu.se>