goto_contractor.h File Reference

#include <iostream>
#include <util/ssa/goto_expr_factory.h>
#include <goto-programs/goto_functions.h>
#include <goto-programs/goto_functions_algorithm.h>
#include <util/message/message.h>
#include <goto-programs/goto_loops.h>
#include <goto-programs/remove_no_op.h>
#include <goto-programs/loopst.h>
#include <util/irep/std_types.h>
#include <ibex.h>
#include <ibex/ibex_Interval.h>
#include <ibex/ibex_Expr.h>
#include <ibex/ibex_Ctc.h>
#include <irep2/irep2.h>
#include <util/base/host_rounding_mode.h>
#include <util/expr/type_byte_size.h>
#include <goto-programs/abstract-interpretation/interval_analysis.h>
#include <limits>
#include <chrono>

Include dependency graph for goto_contractor.h:

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

Go to the source code of this file.

Classes
class	vart
class	Contractor
class	Contractors
class	CspMap
	This class is for mapping the variables with their names and intervals. More...
class	expr_to_ibex_parser
	This class will parse ESBMC expressions to ibex expressions: More...
class	goto_contractort
class	interval_analysis_ibex_contractor

Functions
void	goto_contractor (goto_functionst &goto_functions, const namespacet &namespacet, const optionst &options)

Function Documentation

goto_contractor()

void goto_contractor	(	goto_functionst &	goto_functions,
		const namespacet &	namespacet,
		const optionst &	options )