@@ -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+
340416static 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-
20062006void goto_check_ct::goto_check (
20072007 const irep_idt &function_identifier,
20082008 goto_functiont &goto_function)
0 commit comments