Adds description of the Instantiate plug-in

_fc-plugins/instantiate.md

+---
+layout: plugin
+title: Instantiate
+description: Instantiate creates function specializations for other plugins.
+key: code
+distrib_mode: main
+---
+
+## Overview
+
+The **Instantiate** plug-in (distributed with Frama-C and disabled by
+default) is meant to build function specialization to C functions in a
+project 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 call for which an instantiation generator is available and if
+the call is well-typed according to this generator, **Instantiate**
+replaces this call with a call to an automatically generated
+specialization corresponding to the call. 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
+
+- The default behavior of this plugin is to replace calls in every
+  functions. 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
\ No newline at end of file