Skip to content

Commit 1144e48

Browse files
committed
Move flag_resett class to the top to enable use in other methods
No changes in behaviour, just code motion. Upcoming commits will use this class in `check_rec`.
1 parent bfdbce9 commit 1144e48

File tree

1 file changed

+76
-76
lines changed

1 file changed

+76
-76
lines changed

src/analyses/goto_check_c.cpp

Lines changed: 76 additions & 76 deletions
Original file line numberDiff line numberDiff line change
@@ -337,6 +337,82 @@ class goto_check_ct
337337
named_check_statust match_named_check(const irep_idt &named_check) const;
338338
};
339339

340+
/// Allows to:
341+
/// - override a Boolean flag with a new value via `set_flag`
342+
/// - set a Boolean flag to false via `disable_flag`, such that
343+
/// previous `set_flag` are overridden and future `set_flag` are ignored.
344+
///
345+
/// A flag's initial value (before any `set_flag` or `disable_flag`) is restored
346+
/// when the entire object goes out of scope.
347+
class flag_resett
348+
{
349+
public:
350+
explicit flag_resett(const goto_programt::instructiont &_instruction)
351+
: instruction(_instruction)
352+
{
353+
}
354+
355+
/// \brief Store the current value of \p flag and
356+
/// then set its value to \p new_value.
357+
///
358+
/// - calling `set_flag` after `disable_flag` is a no-op
359+
/// - calling `set_flag` twice triggers an INVARIANT
360+
void set_flag(bool &flag, bool new_value, const irep_idt &flag_name)
361+
{
362+
// make this a no-op if the flag is disabled
363+
if(disabled_flags.find(&flag) != disabled_flags.end())
364+
return;
365+
366+
// detect double sets
367+
INVARIANT(
368+
flags_to_reset.find(&flag) == flags_to_reset.end(),
369+
"Flag " + id2string(flag_name) + " set twice at \n" +
370+
instruction.source_location().pretty());
371+
if(flag != new_value)
372+
{
373+
flags_to_reset[&flag] = flag;
374+
flag = new_value;
375+
}
376+
}
377+
378+
/// Sets the given flag to false, overriding any previous value.
379+
///
380+
/// - calling `disable_flag` after `set_flag` overrides the set value
381+
/// - calling `disable_flag` twice triggers an INVARIANT
382+
void disable_flag(bool &flag, const irep_idt &flag_name)
383+
{
384+
INVARIANT(
385+
disabled_flags.find(&flag) == disabled_flags.end(),
386+
"Flag " + id2string(flag_name) + " disabled twice at \n" +
387+
instruction.source_location().pretty());
388+
389+
disabled_flags.insert(&flag);
390+
391+
// If the flag has not already been set,
392+
// we store its current value in the reset map.
393+
// Otherwise, the reset map already holds
394+
// the initial value we want to reset it to, keep it as is.
395+
if(flags_to_reset.find(&flag) == flags_to_reset.end())
396+
flags_to_reset[&flag] = flag;
397+
398+
// set the flag to false in all cases.
399+
flag = false;
400+
}
401+
402+
/// \brief Restore the values of all flags that have been
403+
/// modified via `set_flag`.
404+
~flag_resett()
405+
{
406+
for(const auto &flag_pair : flags_to_reset)
407+
*flag_pair.first = flag_pair.second;
408+
}
409+
410+
private:
411+
const goto_programt::instructiont &instruction;
412+
std::map<bool *, bool> flags_to_reset;
413+
std::set<bool *> disabled_flags;
414+
};
415+
340416
static exprt implication(exprt lhs, exprt rhs)
341417
{
342418
// rewrite a => (b => c) to (a && b) => c
@@ -1927,82 +2003,6 @@ optionalt<exprt> goto_check_ct::rw_ok_check(exprt expr)
19272003
return {};
19282004
}
19292005

1930-
/// Allows to:
1931-
/// - override a Boolean flag with a new value via `set_flag`
1932-
/// - set a Boolean flag to false via `disable_flag`, such that
1933-
/// previous `set_flag` are overridden and future `set_flag` are ignored.
1934-
///
1935-
/// A flag's initial value (before any `set_flag` or `disable_flag`) is restored
1936-
/// when the entire object goes out of scope.
1937-
class flag_resett
1938-
{
1939-
public:
1940-
explicit flag_resett(const goto_programt::instructiont &_instruction)
1941-
: instruction(_instruction)
1942-
{
1943-
}
1944-
1945-
/// \brief Store the current value of \p flag and
1946-
/// then set its value to \p new_value.
1947-
///
1948-
/// - calling `set_flag` after `disable_flag` is a no-op
1949-
/// - calling `set_flag` twice triggers an INVARIANT
1950-
void set_flag(bool &flag, bool new_value, const irep_idt &flag_name)
1951-
{
1952-
// make this a no-op if the flag is disabled
1953-
if(disabled_flags.find(&flag) != disabled_flags.end())
1954-
return;
1955-
1956-
// detect double sets
1957-
INVARIANT(
1958-
flags_to_reset.find(&flag) == flags_to_reset.end(),
1959-
"Flag " + id2string(flag_name) + " set twice at \n" +
1960-
instruction.source_location().pretty());
1961-
if(flag != new_value)
1962-
{
1963-
flags_to_reset[&flag] = flag;
1964-
flag = new_value;
1965-
}
1966-
}
1967-
1968-
/// Sets the given flag to false, overriding any previous value.
1969-
///
1970-
/// - calling `disable_flag` after `set_flag` overrides the set value
1971-
/// - calling `disable_flag` twice triggers an INVARIANT
1972-
void disable_flag(bool &flag, const irep_idt &flag_name)
1973-
{
1974-
INVARIANT(
1975-
disabled_flags.find(&flag) == disabled_flags.end(),
1976-
"Flag " + id2string(flag_name) + " disabled twice at \n" +
1977-
instruction.source_location().pretty());
1978-
1979-
disabled_flags.insert(&flag);
1980-
1981-
// If the flag has not already been set,
1982-
// we store its current value in the reset map.
1983-
// Otherwise, the reset map already holds
1984-
// the initial value we want to reset it to, keep it as is.
1985-
if(flags_to_reset.find(&flag) == flags_to_reset.end())
1986-
flags_to_reset[&flag] = flag;
1987-
1988-
// set the flag to false in all cases.
1989-
flag = false;
1990-
}
1991-
1992-
/// \brief Restore the values of all flags that have been
1993-
/// modified via `set_flag`.
1994-
~flag_resett()
1995-
{
1996-
for(const auto &flag_pair : flags_to_reset)
1997-
*flag_pair.first = flag_pair.second;
1998-
}
1999-
2000-
private:
2001-
const goto_programt::instructiont &instruction;
2002-
std::map<bool *, bool> flags_to_reset;
2003-
std::set<bool *> disabled_flags;
2004-
};
2005-
20062006
void goto_check_ct::goto_check(
20072007
const irep_idt &function_identifier,
20082008
goto_functiont &goto_function)

0 commit comments

Comments
 (0)