@@ -340,6 +340,82 @@ class goto_check_ct
340
340
named_check_statust match_named_check (const irep_idt &named_check) const ;
341
341
};
342
342
343
+ // / Allows to:
344
+ // / - override a Boolean flag with a new value via `set_flag`
345
+ // / - set a Boolean flag to false via `disable_flag`, such that
346
+ // / previous `set_flag` are overridden and future `set_flag` are ignored.
347
+ // /
348
+ // / A flag's initial value (before any `set_flag` or `disable_flag`) is restored
349
+ // / when the entire object goes out of scope.
350
+ class flag_resett
351
+ {
352
+ public:
353
+ explicit flag_resett (const goto_programt::instructiont &_instruction)
354
+ : instruction(_instruction)
355
+ {
356
+ }
357
+
358
+ // / \brief Store the current value of \p flag and
359
+ // / then set its value to \p new_value.
360
+ // /
361
+ // / - calling `set_flag` after `disable_flag` is a no-op
362
+ // / - calling `set_flag` twice triggers an INVARIANT
363
+ void set_flag (bool &flag, bool new_value, const irep_idt &flag_name)
364
+ {
365
+ // make this a no-op if the flag is disabled
366
+ if (disabled_flags.find (&flag) != disabled_flags.end ())
367
+ return ;
368
+
369
+ // detect double sets
370
+ INVARIANT (
371
+ flags_to_reset.find (&flag) == flags_to_reset.end (),
372
+ " Flag " + id2string (flag_name) + " set twice at \n " +
373
+ instruction.source_location ().pretty ());
374
+ if (flag != new_value)
375
+ {
376
+ flags_to_reset[&flag] = flag;
377
+ flag = new_value;
378
+ }
379
+ }
380
+
381
+ // / Sets the given flag to false, overriding any previous value.
382
+ // /
383
+ // / - calling `disable_flag` after `set_flag` overrides the set value
384
+ // / - calling `disable_flag` twice triggers an INVARIANT
385
+ void disable_flag (bool &flag, const irep_idt &flag_name)
386
+ {
387
+ INVARIANT (
388
+ disabled_flags.find (&flag) == disabled_flags.end (),
389
+ " Flag " + id2string (flag_name) + " disabled twice at \n " +
390
+ instruction.source_location ().pretty ());
391
+
392
+ disabled_flags.insert (&flag);
393
+
394
+ // If the flag has not already been set,
395
+ // we store its current value in the reset map.
396
+ // Otherwise, the reset map already holds
397
+ // the initial value we want to reset it to, keep it as is.
398
+ if (flags_to_reset.find (&flag) == flags_to_reset.end ())
399
+ flags_to_reset[&flag] = flag;
400
+
401
+ // set the flag to false in all cases.
402
+ flag = false ;
403
+ }
404
+
405
+ // / \brief Restore the values of all flags that have been
406
+ // / modified via `set_flag`.
407
+ ~flag_resett ()
408
+ {
409
+ for (const auto &flag_pair : flags_to_reset)
410
+ *flag_pair.first = flag_pair.second ;
411
+ }
412
+
413
+ private:
414
+ const goto_programt::instructiont &instruction;
415
+ std::map<bool *, bool > flags_to_reset;
416
+ std::set<bool *> disabled_flags;
417
+ };
418
+
343
419
static exprt implication (exprt lhs, exprt rhs)
344
420
{
345
421
// rewrite a => (b => c) to (a && b) => c
@@ -1930,82 +2006,6 @@ optionalt<exprt> goto_check_ct::rw_ok_check(exprt expr)
1930
2006
return {};
1931
2007
}
1932
2008
1933
- // / Allows to:
1934
- // / - override a Boolean flag with a new value via `set_flag`
1935
- // / - set a Boolean flag to false via `disable_flag`, such that
1936
- // / previous `set_flag` are overridden and future `set_flag` are ignored.
1937
- // /
1938
- // / A flag's initial value (before any `set_flag` or `disable_flag`) is restored
1939
- // / when the entire object goes out of scope.
1940
- class flag_resett
1941
- {
1942
- public:
1943
- explicit flag_resett (const goto_programt::instructiont &_instruction)
1944
- : instruction(_instruction)
1945
- {
1946
- }
1947
-
1948
- // / \brief Store the current value of \p flag and
1949
- // / then set its value to \p new_value.
1950
- // /
1951
- // / - calling `set_flag` after `disable_flag` is a no-op
1952
- // / - calling `set_flag` twice triggers an INVARIANT
1953
- void set_flag (bool &flag, bool new_value, const irep_idt &flag_name)
1954
- {
1955
- // make this a no-op if the flag is disabled
1956
- if (disabled_flags.find (&flag) != disabled_flags.end ())
1957
- return ;
1958
-
1959
- // detect double sets
1960
- INVARIANT (
1961
- flags_to_reset.find (&flag) == flags_to_reset.end (),
1962
- " Flag " + id2string (flag_name) + " set twice at \n " +
1963
- instruction.source_location ().pretty ());
1964
- if (flag != new_value)
1965
- {
1966
- flags_to_reset[&flag] = flag;
1967
- flag = new_value;
1968
- }
1969
- }
1970
-
1971
- // / Sets the given flag to false, overriding any previous value.
1972
- // /
1973
- // / - calling `disable_flag` after `set_flag` overrides the set value
1974
- // / - calling `disable_flag` twice triggers an INVARIANT
1975
- void disable_flag (bool &flag, const irep_idt &flag_name)
1976
- {
1977
- INVARIANT (
1978
- disabled_flags.find (&flag) == disabled_flags.end (),
1979
- " Flag " + id2string (flag_name) + " disabled twice at \n " +
1980
- instruction.source_location ().pretty ());
1981
-
1982
- disabled_flags.insert (&flag);
1983
-
1984
- // If the flag has not already been set,
1985
- // we store its current value in the reset map.
1986
- // Otherwise, the reset map already holds
1987
- // the initial value we want to reset it to, keep it as is.
1988
- if (flags_to_reset.find (&flag) == flags_to_reset.end ())
1989
- flags_to_reset[&flag] = flag;
1990
-
1991
- // set the flag to false in all cases.
1992
- flag = false ;
1993
- }
1994
-
1995
- // / \brief Restore the values of all flags that have been
1996
- // / modified via `set_flag`.
1997
- ~flag_resett ()
1998
- {
1999
- for (const auto &flag_pair : flags_to_reset)
2000
- *flag_pair.first = flag_pair.second ;
2001
- }
2002
-
2003
- private:
2004
- const goto_programt::instructiont &instruction;
2005
- std::map<bool *, bool > flags_to_reset;
2006
- std::set<bool *> disabled_flags;
2007
- };
2008
-
2009
2009
void goto_check_ct::goto_check (
2010
2010
const irep_idt &function_identifier,
2011
2011
goto_functiont &goto_function)
0 commit comments