Inductiveness. More...
#include "solver_types.h"
Include dependency graph for inductiveness.h: This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Classes | |
| class | inductiveness_resultt |
Functions | |
| inductiveness_resultt | inductiveness_check (std::vector< framet > &frames, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const solver_optionst &, const namespacet &, std::vector< propertyt > &properties, std::size_t property_index) |
Detailed Description
Inductiveness.
Definition in file inductiveness.h.
Function Documentation
◆ inductiveness_check()
| inductiveness_resultt inductiveness_check | ( | std::vector< framet > & | frames, |
| const std::unordered_set< symbol_exprt, irep_hash > & | address_taken, | ||
| const solver_optionst & | solver_options, | ||
| const namespacet & | ns, | ||
| std::vector< propertyt > & | properties, | ||
| std::size_t | property_index | ||
| ) |
Definition at line 98 of file inductiveness.cpp.
