cprover
Loading...
Searching...
No Matches
inductiveness.h File Reference

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.