From 8a32d754c7b45f6fb970ca2bb35e54c9b0289d26 Mon Sep 17 00:00:00 2001
From: Remi Delmas <delmasrd@amazon.com>
Date: Tue, 21 Jan 2025 01:16:29 -0500
Subject: [PATCH] Add tests for assumption uniqueness checking

---
 .../main.c                                    | 20 ++++++++++++++++
 .../test.desc                                 | 11 +++++++++
 .../main.c                                    | 20 ++++++++++++++++
 .../test.desc                                 | 10 ++++++++
 .../main.c                                    | 22 ++++++++++++++++++
 .../test.desc                                 | 11 +++++++++
 .../main.c                                    | 22 ++++++++++++++++++
 .../test.desc                                 | 10 ++++++++
 .../main.c                                    | 22 ++++++++++++++++++
 .../test.desc                                 | 10 ++++++++
 .../main.c                                    | 20 ++++++++++++++++
 .../test.desc                                 | 11 +++++++++
 .../main.c                                    | 20 ++++++++++++++++
 .../test.desc                                 | 10 ++++++++
 .../main.c                                    | 22 ++++++++++++++++++
 .../test.desc                                 | 11 +++++++++
 .../main.c                                    | 23 +++++++++++++++++++
 .../test.desc                                 | 10 ++++++++
 .../main.c                                    | 17 ++++++++++++++
 .../test.desc                                 | 11 +++++++++
 .../main.c                                    | 17 ++++++++++++++
 .../test.desc                                 | 14 +++++++++++
 .../main.c                                    | 22 ++++++++++++++++++
 .../test.desc                                 | 11 +++++++++
 24 files changed, 377 insertions(+)
 create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/main.c
 create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/test.desc
 create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/main.c
 create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/test.desc
 create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/main.c
 create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/test.desc
 create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/main.c
 create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/test.desc
 create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_pass/main.c
 create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_pass/test.desc
 create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_fail/main.c
 create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_fail/test.desc
 create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_pass/main.c
 create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_pass/test.desc
 create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_fail/main.c
 create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_fail/test.desc
 create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_pass/main.c
 create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_pass/test.desc
 create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_fail/main.c
 create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_fail/test.desc
 create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_pass/main.c
 create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_pass/test.desc
 create mode 100644 regression/contracts-dfcc/test_pointer_predicate_requires_in_range_in_range_fail/main.c
 create mode 100644 regression/contracts-dfcc/test_pointer_predicate_requires_in_range_in_range_fail/test.desc

diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/main.c
new file mode 100644
index 00000000000..7fbd6198160
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/main.c
@@ -0,0 +1,20 @@
+void foo(int *x, int *y)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_requires(*x == 0)
+__CPROVER_requires(__CPROVER_pointer_equals(y, sizeof(int)) && __CPROVER_pointer_equals(y, x))
+__CPROVER_assigns(*y)
+__CPROVER_ensures(*y == 1)
+__CPROVER_ensures(*x == 1)
+// clang-format on
+{
+  *y = 1;
+}
+
+int main()
+{
+  int *x;
+  int *y;
+  foo(x, y);
+  return 0;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/test.desc
new file mode 100644
index 00000000000..53ebf307343
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/test.desc
@@ -0,0 +1,11 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[__CPROVER_contracts_pointer_equals.assertion.\d+\] line \d+ __CPROVER_pointer_equals does not conflict with other predicate: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Tests that assuming the more than one pointer predicate on the same target pointer
+at the same time triggers a failure.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/main.c
new file mode 100644
index 00000000000..d59373da733
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/main.c
@@ -0,0 +1,20 @@
+void foo(int *x, int *y)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_requires(*x == 0)
+__CPROVER_requires(__CPROVER_pointer_equals(y, x) || __CPROVER_pointer_equals(y, x))
+__CPROVER_assigns(*y)
+__CPROVER_ensures(*y == 1)
+__CPROVER_ensures(*x == 1 || *x == 0)
+// clang-format on
+{
+  *y = 1;
+}
+
+int main()
+{
+  int *x;
+  int *y;
+  foo(x, y);
+  return 0;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/test.desc
new file mode 100644
index 00000000000..a84c35bb4db
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/test.desc
@@ -0,0 +1,10 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFULL$
+--
+--
+Tests that a same pointer can be the target of multiple pointer predicates as
+long as they do not apply at the same time.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/main.c
new file mode 100644
index 00000000000..1baed0c514f
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/main.c
@@ -0,0 +1,22 @@
+void foo(int *x, int *y)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_requires(*x == 0)
+__CPROVER_requires(
+  __CPROVER_pointer_in_range_dfcc(x, y, x) &&
+  __CPROVER_pointer_equals(y, x))
+__CPROVER_assigns(*y)
+__CPROVER_ensures(*y == 1)
+__CPROVER_ensures(*x == 1)
+// clang-format on
+{
+  *y = 1;
+}
+
+int main()
+{
+  int *x;
+  int *y;
+  foo(x, y);
+  return 0;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/test.desc
new file mode 100644
index 00000000000..436d8c30564
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/test.desc
@@ -0,0 +1,11 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[__CPROVER_contracts_pointer_in_range_dfcc.assertion.\d+\] line \d+ __CPROVER_pointer_in_range_dfcc does not conflict with other predicate: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Tests that assuming the more than one pointer predicate on the same target pointer
+at the same time triggers a failure.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/main.c
new file mode 100644
index 00000000000..1baed0c514f
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/main.c
@@ -0,0 +1,22 @@
+void foo(int *x, int *y)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_requires(*x == 0)
+__CPROVER_requires(
+  __CPROVER_pointer_in_range_dfcc(x, y, x) &&
+  __CPROVER_pointer_equals(y, x))
+__CPROVER_assigns(*y)
+__CPROVER_ensures(*y == 1)
+__CPROVER_ensures(*x == 1)
+// clang-format on
+{
+  *y = 1;
+}
+
+int main()
+{
+  int *x;
+  int *y;
+  foo(x, y);
+  return 0;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/test.desc
new file mode 100644
index 00000000000..a84c35bb4db
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/test.desc
@@ -0,0 +1,10 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFULL$
+--
+--
+Tests that a same pointer can be the target of multiple pointer predicates as
+long as they do not apply at the same time.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_pass/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_pass/main.c
new file mode 100644
index 00000000000..1a4cb7173c7
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_pass/main.c
@@ -0,0 +1,22 @@
+void foo(int *x, int *y)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_requires(*x == 0)
+__CPROVER_requires(
+  __CPROVER_pointer_in_range_dfcc(x, y, x) &&
+  __CPROVER_pointer_in_range_dfcc(x, y, x))
+__CPROVER_assigns(*y)
+__CPROVER_ensures(*y == 1)
+__CPROVER_ensures(*x == 1)
+// clang-format on
+{
+  *y = 1;
+}
+
+int main()
+{
+  int *x;
+  int *y;
+  foo(x, y);
+  return 0;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_pass/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_pass/test.desc
new file mode 100644
index 00000000000..a84c35bb4db
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_pass/test.desc
@@ -0,0 +1,10 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFULL$
+--
+--
+Tests that a same pointer can be the target of multiple pointer predicates as
+long as they do not apply at the same time.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_fail/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_fail/main.c
new file mode 100644
index 00000000000..9ccae900abe
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_fail/main.c
@@ -0,0 +1,20 @@
+void foo(int *x, int *y)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_requires(*x == 0)
+__CPROVER_requires(__CPROVER_is_fresh(y, sizeof(int)) && __CPROVER_pointer_equals(y, x))
+__CPROVER_assigns(*y)
+__CPROVER_ensures(*y == 1)
+__CPROVER_ensures(*x == 1 || *x == 0)
+// clang-format on
+{
+  *y = 1;
+}
+
+int main()
+{
+  int *x;
+  int *y;
+  foo(x, y);
+  return 0;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_fail/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_fail/test.desc
new file mode 100644
index 00000000000..53ebf307343
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_fail/test.desc
@@ -0,0 +1,11 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[__CPROVER_contracts_pointer_equals.assertion.\d+\] line \d+ __CPROVER_pointer_equals does not conflict with other predicate: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Tests that assuming the more than one pointer predicate on the same target pointer
+at the same time triggers a failure.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_pass/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_pass/main.c
new file mode 100644
index 00000000000..2a8f24a3e55
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_pass/main.c
@@ -0,0 +1,20 @@
+void foo(int *x, int *y)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_requires(*x == 0)
+__CPROVER_requires(__CPROVER_is_fresh(y, sizeof(int)) || __CPROVER_pointer_equals(y, x))
+__CPROVER_assigns(*y)
+__CPROVER_ensures(*y == 1)
+__CPROVER_ensures(*x == 1 || *x == 0)
+// clang-format on
+{
+  *y = 1;
+}
+
+int main()
+{
+  int *x;
+  int *y;
+  foo(x, y);
+  return 0;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_pass/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_pass/test.desc
new file mode 100644
index 00000000000..a84c35bb4db
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_pass/test.desc
@@ -0,0 +1,10 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFULL$
+--
+--
+Tests that a same pointer can be the target of multiple pointer predicates as
+long as they do not apply at the same time.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_fail/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_fail/main.c
new file mode 100644
index 00000000000..066174498c7
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_fail/main.c
@@ -0,0 +1,22 @@
+void foo(int *x, int *y)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_requires(*x == 0)
+__CPROVER_requires(
+  __CPROVER_is_fresh(y, sizeof(int)) &&
+  __CPROVER_pointer_in_range_dfcc(x, y, x))
+__CPROVER_assigns(*y)
+__CPROVER_ensures(*y == 1)
+__CPROVER_ensures(*x == 1 || *x == 0)
+// clang-format on
+{
+  *y = 1;
+}
+
+int main()
+{
+  int *x;
+  int *y;
+  foo(x, y);
+  return 0;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_fail/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_fail/test.desc
new file mode 100644
index 00000000000..436d8c30564
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_fail/test.desc
@@ -0,0 +1,11 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[__CPROVER_contracts_pointer_in_range_dfcc.assertion.\d+\] line \d+ __CPROVER_pointer_in_range_dfcc does not conflict with other predicate: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Tests that assuming the more than one pointer predicate on the same target pointer
+at the same time triggers a failure.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_pass/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_pass/main.c
new file mode 100644
index 00000000000..0afd193f786
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_pass/main.c
@@ -0,0 +1,23 @@
+void foo(int *x, int *y)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_requires(*x == 0)
+__CPROVER_requires(x[SIZE-1] == 0)
+__CPROVER_requires(
+  __CPROVER_is_fresh(y, sizeof(int)) ||
+  __CPROVER_pointer_in_range_dfcc(x, y, x))
+__CPROVER_assigns(*y)
+__CPROVER_ensures(*y == 1)
+__CPROVER_ensures(*x == 1 || *x == 0)
+// clang-format on
+{
+  *y = 1;
+}
+
+int main()
+{
+  int *x;
+  int *y;
+  foo(x, y);
+  return 0;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_pass/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_pass/test.desc
new file mode 100644
index 00000000000..a84c35bb4db
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_pass/test.desc
@@ -0,0 +1,10 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFULL$
+--
+--
+Tests that a same pointer can be the target of multiple pointer predicates as
+long as they do not apply at the same time.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_fail/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_fail/main.c
new file mode 100644
index 00000000000..cc39fa82856
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_fail/main.c
@@ -0,0 +1,17 @@
+void foo(int *x)
+  // clang-format off
+__CPROVER_requires(
+  __CPROVER_is_fresh(x, sizeof(int)) && __CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_assigns(*x)
+__CPROVER_ensures(*x == 0)
+// clang-format on
+{
+  *x = 0;
+}
+
+int main()
+{
+  int *x;
+  foo(x);
+  return 0;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_fail/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_fail/test.desc
new file mode 100644
index 00000000000..fd41201b4fb
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_fail/test.desc
@@ -0,0 +1,11 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[__CPROVER_contracts_is_fresh.assertion.\d+\] line \d+ __CPROVER_is_fresh does not conflict with other predicate: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Tests that assuming the more than one pointer predicate on the same target pointer
+at the same time triggers a failure.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_pass/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_pass/main.c
new file mode 100644
index 00000000000..e338a05dd25
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_pass/main.c
@@ -0,0 +1,17 @@
+void foo(int *x)
+  // clang-format off
+__CPROVER_requires(
+  __CPROVER_is_fresh(x, sizeof(int)) || __CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_assigns(*x)
+__CPROVER_ensures(*x == 0)
+// clang-format on
+{
+  *x = 0;
+}
+
+int main()
+{
+  int *x;
+  foo(x);
+  return 0;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_pass/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_pass/test.desc
new file mode 100644
index 00000000000..9d72851c220
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_pass/test.desc
@@ -0,0 +1,14 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFULL$
+--
+--
+Tests that a same pointer can be the target of multiple pointer predicates as
+long as they do not apply at the same time.
+- `x` is fresh and inialized to 0
+- `y` is equal to `x`if select is true, or fresh otherwise
+- foo assigns y to 1
+- x is equal to 1 if select is true, 0 otherwise
diff --git a/regression/contracts-dfcc/test_pointer_predicate_requires_in_range_in_range_fail/main.c b/regression/contracts-dfcc/test_pointer_predicate_requires_in_range_in_range_fail/main.c
new file mode 100644
index 00000000000..1a4cb7173c7
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_requires_in_range_in_range_fail/main.c
@@ -0,0 +1,22 @@
+void foo(int *x, int *y)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_requires(*x == 0)
+__CPROVER_requires(
+  __CPROVER_pointer_in_range_dfcc(x, y, x) &&
+  __CPROVER_pointer_in_range_dfcc(x, y, x))
+__CPROVER_assigns(*y)
+__CPROVER_ensures(*y == 1)
+__CPROVER_ensures(*x == 1)
+// clang-format on
+{
+  *y = 1;
+}
+
+int main()
+{
+  int *x;
+  int *y;
+  foo(x, y);
+  return 0;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_requires_in_range_in_range_fail/test.desc b/regression/contracts-dfcc/test_pointer_predicate_requires_in_range_in_range_fail/test.desc
new file mode 100644
index 00000000000..436d8c30564
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_requires_in_range_in_range_fail/test.desc
@@ -0,0 +1,11 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[__CPROVER_contracts_pointer_in_range_dfcc.assertion.\d+\] line \d+ __CPROVER_pointer_in_range_dfcc does not conflict with other predicate: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Tests that assuming the more than one pointer predicate on the same target pointer
+at the same time triggers a failure.