From 6b4943e18df21524b1377dfa4d78dec28a2aa93a Mon Sep 17 00:00:00 2001 From: Allan Blanchard <allan.blanchard@cea.fr> Date: Thu, 7 May 2020 14:14:33 +0200 Subject: [PATCH] Adds description of the Instantiate plug-in --- _fc-plugins/instantiate.md | 91 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 91 insertions(+) create mode 100644 _fc-plugins/instantiate.md diff --git a/_fc-plugins/instantiate.md b/_fc-plugins/instantiate.md new file mode 100644 index 00000000..2a3d6c71 --- /dev/null +++ b/_fc-plugins/instantiate.md @@ -0,0 +1,91 @@ +--- +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 -- GitLab