forked from diffblue/cbmc
-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Indirect value_set_domaint -> value_sett operations via non-member fu…
…nctions These provide an oportunity for future implementers of value-sets not to have to conform to the same public interface as value_sett, e.g. to provide some type they can't or don't want to augment and provide non-member function specialisations instead.
- Loading branch information
Showing
1 changed file
with
82 additions
and
10 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -17,6 +17,77 @@ Author: Daniel Kroening, [email protected] | |
|
||
#include "value_set.h" | ||
|
||
template<class> class value_set_domaint; | ||
|
||
// Forwarders for value_set_domaint's calls against value_sett. | ||
// Specialise these if for some reason you can't just write a member function, | ||
// or for location numbers, expose the field. | ||
template<typename VST> | ||
inline bool value_set_make_union(VST &value_set, const VST &other) | ||
{ | ||
return value_set.make_union(other); | ||
} | ||
|
||
template<typename VST> | ||
inline void value_set_output( | ||
const VST &value_set, const namespacet &ns, std::ostream &out) | ||
{ | ||
value_set.output(ns, out); | ||
} | ||
|
||
template<typename VST> | ||
inline void value_set_clear(VST &value_set) | ||
{ | ||
value_set.clear(); | ||
} | ||
|
||
template<typename VST> | ||
inline void value_set_set_location_number(VST &value_set, unsigned loc) | ||
{ | ||
value_set.location_number=loc; | ||
} | ||
|
||
template<typename VST> | ||
inline void value_set_read_reference_set( | ||
const VST &value_set, | ||
const exprt &expr, | ||
value_setst::valuest &dest, | ||
const namespacet &ns) | ||
{ | ||
value_set.read_reference_set(expr, dest, ns); | ||
} | ||
|
||
template<typename VST> | ||
inline void value_set_do_end_function( | ||
VST &value_set, const exprt &return_expr, const namespacet &ns) | ||
{ | ||
value_set.do_end_function(return_expr, ns); | ||
} | ||
|
||
template<typename VST> | ||
inline void value_set_apply_code( | ||
VST &value_set, const codet &code, const namespacet &ns) | ||
{ | ||
value_set.apply_code(code, ns); | ||
} | ||
|
||
template<typename VST> | ||
inline void value_set_guard( | ||
VST &value_set, const exprt &guard, const namespacet &ns) | ||
{ | ||
value_set.guard(guard, ns); | ||
} | ||
|
||
template<typename VST> | ||
inline void value_set_do_function_call( | ||
VST &value_set, | ||
const irep_idt &function, | ||
const exprt::operandst &arguments, | ||
const namespacet &ns) | ||
{ | ||
value_set.do_function_call(function, arguments, ns); | ||
} | ||
|
||
template<class VST> | ||
class value_set_domaint:public domain_baset | ||
{ | ||
|
@@ -25,23 +96,23 @@ class value_set_domaint:public domain_baset | |
|
||
// overloading | ||
|
||
bool merge(const value_set_domaint &other, locationt to) | ||
bool merge(const value_set_domaint<VST> &other, locationt to) | ||
{ | ||
return value_set.make_union(other.value_set); | ||
return value_set_make_union(value_set, other.value_set); | ||
} | ||
|
||
virtual void output( | ||
const namespacet &ns, | ||
std::ostream &out) const | ||
{ | ||
value_set.output(ns, out); | ||
value_set_output(value_set, ns, out); | ||
} | ||
|
||
virtual void initialize( | ||
const namespacet &ns, | ||
locationt l) | ||
{ | ||
value_set.clear(); | ||
value_set_clear(value_set); | ||
value_set.location_number=l->location_number; | ||
} | ||
|
||
|
@@ -50,7 +121,7 @@ class value_set_domaint:public domain_baset | |
const exprt &expr, | ||
value_setst::valuest &dest) | ||
{ | ||
value_set.read_reference_set(expr, dest, ns); | ||
value_set_read_reference_set(value_set, expr, dest, ns); | ||
} | ||
|
||
virtual void transform( | ||
|
@@ -66,8 +137,8 @@ class value_set_domaint:public domain_baset | |
|
||
case END_FUNCTION: | ||
{ | ||
value_set.do_end_function( | ||
static_analysis_baset::get_return_lhs(to_l), ns); | ||
value_set_do_end_function( | ||
value_set, static_analysis_baset::get_return_lhs(to_l), ns); | ||
break; | ||
} | ||
|
||
|
@@ -77,19 +148,20 @@ class value_set_domaint:public domain_baset | |
case ASSIGN: | ||
case DECL: | ||
case DEAD: | ||
value_set.apply_code(from_l->code, ns); | ||
value_set_apply_code(value_set, from_l->code, ns); | ||
break; | ||
|
||
case ASSUME: | ||
value_set.guard(from_l->guard, ns); | ||
value_set_guard(value_set, from_l->guard, ns); | ||
break; | ||
|
||
case FUNCTION_CALL: | ||
{ | ||
const code_function_callt &code= | ||
to_code_function_call(from_l->code); | ||
|
||
value_set.do_function_call(to_l->function, code.arguments(), ns); | ||
value_set_do_function_call( | ||
value_set, to_l->function, code.arguments(), ns); | ||
} | ||
break; | ||
|
||
|