Instantiate

Overview

The Instantiate plug-in is meant to build function specializations for C functions when the original specification (or prototype of the function) cannot be efficiently used by some plugins. Generally, it is used to specialize functions that receive void* parameters.

For each compatible call, Instantiate replaces it with a call to an automatically generated specialization. Note that the contract of the generated function is considered verified.

Quick Start

The plug-in is enabled by setting the option -instantiate. The result can be output via the kernel option -print. It can also be directly used by other plug-ins.

Example

Example input:

#include <string.h>
void main(void){
  char copy[13];
  memcpy(copy, "Hello world!", 13);
}

Example output:

/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
#include "strings.h"
/*@ requires
      separation: \separated(dest + (0 .. len - 1), src + (0 .. len - 1));
    requires aligned_end: len % 1 ≡ 0;
    requires valid_dest: \valid(dest + (0 .. len - 1));
    requires valid_read_src: \valid_read(src + (0 .. len - 1));
    ensures
      copied: ∀ ℤ j0; 0 ≤ j0 < len ⇒ *(dest + j0) ≡ *(src + j0);
    ensures result: \result ≡ dest;
    assigns *(dest + (0 .. len - 1)), \result;
    assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1));
    assigns \result \from dest;
 */
char *memcpy_char(char *dest, char const *src, size_t len)
{
  char *__retres;
  __retres = (char *)memcpy((void *)dest,(void const *)src,len);
  return __retres;
}

void main(void)
{
  char copy[13];
  memcpy_char(copy,"Hello world!",(unsigned int)13);
  return;
}

Technical Notes