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 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));
      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);

Technical Notes

  • The default behavior of this plugin is to replace calls in every function. The option -instantiate-fct can be used to select the functions to process.

  • Currently, the plugin supports memcmp, memcpy, memmove, memset (partially, check the README for more details), malloc, calloc and free. The support of each of this function is enabled by default and can be deactivated using the option -instantiate-no-<function name>.

Further Reading

Information about the plug-in is available via its help option:

frama-c -instantiate-help