Translate functions that specify assignable and freeable targets declaratively into active functions that build write sets dynamically by rewriting calls to front-end functions into calls to library functions defining their dynamic semantics. More...
#include <util/arith_tools.h>#include <util/c_types.h>#include <util/message.h>#include <util/std_expr.h>#include <util/std_types.h>#include "dfcc_library.h"#include "dfcc_utils.h"#include <map>#include <set>
Include dependency graph for dfcc_spec_functions.h: This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Classes | |
| class | dfcc_spec_functionst |
| This class rewrites GOTO functions that use the built-ins: More... | |
Enumerations | |
| enum class | dfcc_ptr_havoc_modet { INVALID , NONDET } |
| Represents the different ways to havoc pointers. More... | |
Detailed Description
Translate functions that specify assignable and freeable targets declaratively into active functions that build write sets dynamically by rewriting calls to front-end functions into calls to library functions defining their dynamic semantics.
Definition in file dfcc_spec_functions.h.
Enumeration Type Documentation
◆ dfcc_ptr_havoc_modet
|
strong |
Represents the different ways to havoc pointers.
Remark:
- Function contracts use invalid
- Loop contracts use nondet
| Enumerator | |
|---|---|
| INVALID | havocs the pointer to an invalid pointer |
| NONDET | havocs the pointer to an nondet pointer |
Definition at line 40 of file dfcc_spec_functions.h.
