Records what a forall2t/exists2t binds while its body is walked, so the index fold in dereference_expr_nonscalar leaves the bound variable alone: the rename callback carries no quantifier context and would substitute the like-named program variable's SSA value (rename_quantified guards the same concern at the renaming layer, #7024). More...

Public Member Functions
	quantifier_scopet (dereferencet &deref, const expr2tc &expr)
	quantifier_scopet (const quantifier_scopet &)=delete
quantifier_scopet &	operator= (const quantifier_scopet &)=delete
	~quantifier_scopet ()

Detailed Description

Records what a forall2t/exists2t binds while its body is walked, so the index fold in dereference_expr_nonscalar leaves the bound variable alone: the rename callback carries no quantifier context and would substitute the like-named program variable's SSA value (rename_quantified guards the same concern at the renaming layer, #7024).

Constructing one over any other expression does nothing.

Constructor & Destructor Documentation

◆ quantifier_scopet() [1/2]

dereferencet::quantifier_scopet::quantifier_scopet	(	dereferencet &	deref,
		const expr2tc &	expr )

inline

◆ quantifier_scopet() [2/2]

dereferencet::quantifier_scopet::quantifier_scopet ( const quantifier_scopet & )

delete

◆ ~quantifier_scopet()

dereferencet::quantifier_scopet::~quantifier_scopet ( )

inline

Member Function Documentation

◆ operator=()

quantifier_scopet & dereferencet::quantifier_scopet::operator= ( const quantifier_scopet & )