// frama-c -val strncpy.c -cpp-extra-args="-I$(frama-c -print-share-path)/libc" -val-builtin strlen:Frama_C_strlen

#include <string.h>

//@ assigns dest[0..n-1] \from src[0..n-1];
char * strncpy (char * dest, char const * src, size_t n);

struct truc { char name[10]; } obj;

int main (void) {
  struct truc * p = &obj;
  char name [] = "toto";
  size_t n = strlen(name);

  //@ assert a_n: n == 4;
  //@ assert a_name: \valid_read (name + (0..n));
  //@ assert a_rw_name: \valid (name + (0..n));
  //@ assert a_name_str: valid_string (name+0);

   strncpy(p->name, name, n);
   p->name[n] = '\0';

   return 0;
}