Merge pull request #7630 from remi-delmas-3000/contracts-is-cprover-symbol

CONTRACTS: is_cprover_symbol utility function

Author: remi-delmas-3000

src/goto-instrument/Makefile

@@ -19,6 +19,7 @@ SRC = accelerate/accelerate.cpp \
       contracts/contracts.cpp \
       contracts/dynamic-frames/dfcc_utils.cpp \
       contracts/dynamic-frames/dfcc_library.cpp \
+      contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp \
       contracts/dynamic-frames/dfcc_is_fresh.cpp \
       contracts/dynamic-frames/dfcc_pointer_in_range.cpp \
       contracts/dynamic-frames/dfcc_is_freeable.cpp \

src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp

@@ -0,0 +1,22 @@
+/*******************************************************************\
+
+Module: Dynamic frame condition checking
+
+Author: Remi Delmas, [email protected]
+
+Date: March 2023
+
+\*******************************************************************/
+
+#include "dfcc_is_cprover_symbol.h"
+
+#include <util/cprover_prefix.h>
+#include <util/prefix.h>
+#include <util/suffix.h>
+
+bool dfcc_is_cprover_symbol(const irep_idt &id)
+{
+  std::string str = id2string(id);
+  return has_prefix(str, CPROVER_PREFIX) || has_prefix(str, "__VERIFIER") ||
+         has_prefix(str, "nondet") || has_suffix(str, "$object");
+}

src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.h

@@ -0,0 +1,22 @@
+/*******************************************************************\
+
+Module: Dynamic frame condition checking
+
+Author: Remi Delmas, [email protected]
+
+Date: March 2023
+
+\*******************************************************************/
+
+/// \file
+
+#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_IS_CPROVER_SYMBOL_H
+#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_IS_CPROVER_SYMBOL_H
+
+#include <util/irep.h>
+
+/// \return True iff the id starts with CPROVER_PREFIX, `__VERIFIER`, `nondet`
+/// or ends with `$object`.
+bool dfcc_is_cprover_symbol(const irep_idt &id);
+
+#endif