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