package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

Extend the environment with statements which allocate/deallocate memory blocks.

For each variable of the given list, if necessary according to the mtracking analysis, add a call to __e_acsl_store_block in the given environment.

Same as store, with a call to __e_acsl_duplicate_store_block.

Same as store, with a call to __e_acsl_delete_block.

Same as delete_from_list with a set of variables instead of a list.