CBMC: /home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/memory_predicates.h File Reference

CBMC

Loading...

Searching...

No Matches

memory_predicates.h File Reference

Predicates to specify memory footprint in function contracts. More...

#include <util/symbol.h>
#include <goto-programs/goto_program.h>

+ Include dependency graph for memory_predicates.h:

+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class is_fresh_baset

class is_fresh_enforcet

class is_fresh_replacet

class find_is_fresh_calls_visitort

Predicate to be used with the exprt::visit() function. More...

class functions_in_scope_visitort

Predicate to be used with the exprt::visit() function. More...

class function_binding_visitort

Detailed Description

Predicates to specify memory footprint in function contracts.

Definition in file memory_predicates.h.