CN VIP: Annotate the error tests

tests/cn_vip_testsuite/pointer_from_int_disambiguation_3.error.c

@@ -4,13 +4,24 @@
 #include <string.h>
 #include <stdint.h>
 #include <inttypes.h>
+#include "cn_lemmas.h"
 int y=2, x=1;
-int main() {
+int main()
+/*CN_VIP*//*@ accesses y; accesses x; @*/
+{
   int *p = &x+1;
   int *q = &y;
   uintptr_t i = (uintptr_t)p;
   uintptr_t j = (uintptr_t)q;
-  if (memcmp(&p, &q, sizeof(p)) == 0) {
+  /*CN_VIP*/if (&p == &q) return 0;                                         // CN used to derive disjointness and non-null
+  /*CN_VIP*/if ((uintptr_t)&p + sizeof(uintptr_t) < (uintptr_t)&p) return 0;// constraints from resource ownership, but this
+  /*CN_VIP*/if ((uintptr_t)&q + sizeof(uintptr_t) < (uintptr_t)&q) return 0;// was removed for performance reasons.
+  /*CN_VIP*/unsigned char* p_bytes = owned_int_ptr_to_owned_uchar_arr(&p);
+  /*CN_VIP*/unsigned char* q_bytes = owned_int_ptr_to_owned_uchar_arr(&q);
+  /*CN_VIP*/int result = _memcmp(p_bytes, q_bytes, sizeof(p));
+  /*CN_VIP*//*@ apply byte_ptr_to_int_ptr_ptr(p_bytes); @*/
+  /*CN_VIP*//*@ apply byte_ptr_to_int_ptr_ptr(q_bytes); @*/
+  if (result == 0) {
 #if defined(ANNOT)
     int *r = copy_alloc_id(i, q);
 #else

tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_auto_xy.error.c

@@ -1,13 +1,23 @@
 //CN_VIP #include <stdio.h>
 #include <string.h>
 #include <stddef.h>
+#include <inttypes.h>
+#include "cn_lemmas.h"
 int main() {
   int x=1, y=2;
   int *p = &x;
   int *q = &y;
   ptrdiff_t offset = q - p;
   int *r = p + offset;
-  if (memcmp(&r, &q, sizeof(r)) == 0) {
+  /*CN_VIP*/if (&r == &q) return 0;                                         // CN used to derive disjointness and non-null
+  /*CN_VIP*/if ((uintptr_t)&r + sizeof(uintptr_t) < (uintptr_t)&r) return 0;// constraints from resource ownership, but this
+  /*CN_VIP*/if ((uintptr_t)&q + sizeof(uintptr_t) < (uintptr_t)&q) return 0;// was removed for performance reasons.
+  /*CN_VIP*/unsigned char* r_bytes = owned_int_ptr_to_owned_uchar_arr(&r);
+  /*CN_VIP*/unsigned char* q_bytes = owned_int_ptr_to_owned_uchar_arr(&q);
+  /*CN_VIP*/int result = _memcmp(r_bytes, q_bytes, sizeof(r));
+  /*CN_VIP*//*@ apply byte_ptr_to_int_ptr_ptr(r_bytes); @*/
+  /*CN_VIP*//*@ apply byte_ptr_to_int_ptr_ptr(q_bytes); @*/
+  if (result == 0) {
     *r = 11; // is this free of UB?
     //CN_VIP printf("y=%d *q=%d *r=%d\n",y,*q,*r);
   }

tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_auto_yx.error.c

@@ -1,13 +1,23 @@
 //CN_VIP #include <stdio.h>
 #include <string.h>
 #include <stddef.h>
+#include <inttypes.h>
+#include "cn_lemmas.h"
 int main() {
   int y=2, x=1;
   int *p = &x;
   int *q = &y;
   ptrdiff_t offset = q - p;
   int *r = p + offset;
-  if (memcmp(&r, &q, sizeof(r)) == 0) {
+  /*CN_VIP*/if (&r == &q) return 0;                                         // CN used to derive disjointness and non-null
+  /*CN_VIP*/if ((uintptr_t)&r + sizeof(uintptr_t) < (uintptr_t)&r) return 0;// constraints from resource ownership, but this
+  /*CN_VIP*/if ((uintptr_t)&q + sizeof(uintptr_t) < (uintptr_t)&q) return 0;// was removed for performance reasons.
+  /*CN_VIP*/unsigned char* r_bytes = owned_int_ptr_to_owned_uchar_arr(&r);
+  /*CN_VIP*/unsigned char* q_bytes = owned_int_ptr_to_owned_uchar_arr(&q);
+  /*CN_VIP*/int result = _memcmp(r_bytes, q_bytes, sizeof(r));
+  /*CN_VIP*//*@ apply byte_ptr_to_int_ptr_ptr(r_bytes); @*/
+  /*CN_VIP*//*@ apply byte_ptr_to_int_ptr_ptr(q_bytes); @*/
+  if (result == 0) {
     *r = 11; // is this free of UB?
     //CN_VIP printf("y=%d *q=%d *r=%d\n",y,*q,*r);
   }

tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_global_xy.error.c

@@ -1,13 +1,25 @@
 //CN_VIP #include <stdio.h>
 #include <string.h>
 #include <stddef.h>
+#include <inttypes.h>
+#include "cn_lemmas.h"
 int x=1, y=2;
-int main() {
+int main()
+/*CN_VIP*//*@ accesses y; @*/
+{
   int *p = &x;
   int *q = &y;
   ptrdiff_t offset = q - p;
   int *r = p + offset;
-  if (memcmp(&r, &q, sizeof(r)) == 0) {
+  /*CN_VIP*/if (&r == &q) return 0;                                         // CN used to derive disjointness and non-null
+  /*CN_VIP*/if ((uintptr_t)&r + sizeof(uintptr_t) < (uintptr_t)&r) return 0;// constraints from resource ownership, but this
+  /*CN_VIP*/if ((uintptr_t)&q + sizeof(uintptr_t) < (uintptr_t)&q) return 0;// was removed for performance reasons.
+  /*CN_VIP*/unsigned char* r_bytes = owned_int_ptr_to_owned_uchar_arr(&r);
+  /*CN_VIP*/unsigned char* q_bytes = owned_int_ptr_to_owned_uchar_arr(&q);
+  /*CN_VIP*/int result = _memcmp(r_bytes, q_bytes, sizeof(r));
+  /*CN_VIP*//*@ apply byte_ptr_to_int_ptr_ptr(r_bytes); @*/
+  /*CN_VIP*//*@ apply byte_ptr_to_int_ptr_ptr(q_bytes); @*/
+  if (result == 0) {
     *r = 11; // is this free of UB?
     //CN_VIP printf("y=%d *q=%d *r=%d\n",y,*q,*r);
   }

tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_global_yx.error.c

@@ -1,13 +1,25 @@
 //CN_VIP #include <stdio.h>
 #include <string.h>
 #include <stddef.h>
+#include <inttypes.h>
+#include "cn_lemmas.h"
 int y=2, x=1;
-int main() {
+int main()
+/*CN_VIP*//*@ accesses y; @*/
+{
   int *p = &x;
   int *q = &y;
   ptrdiff_t offset = q - p;
   int *r = p + offset;
-  if (memcmp(&r, &q, sizeof(r)) == 0) {
+  /*CN_VIP*/if (&r == &q) return 0;                                         // CN used to derive disjointness and non-null
+  /*CN_VIP*/if ((uintptr_t)&r + sizeof(uintptr_t) < (uintptr_t)&r) return 0;// constraints from resource ownership, but this
+  /*CN_VIP*/if ((uintptr_t)&q + sizeof(uintptr_t) < (uintptr_t)&q) return 0;// was removed for performance reasons.
+  /*CN_VIP*/unsigned char* r_bytes = owned_int_ptr_to_owned_uchar_arr(&r);
+  /*CN_VIP*/unsigned char* q_bytes = owned_int_ptr_to_owned_uchar_arr(&q);
+  /*CN_VIP*/int result = _memcmp(r_bytes, q_bytes, sizeof(r));
+  /*CN_VIP*//*@ apply byte_ptr_to_int_ptr_ptr(r_bytes); @*/
+  /*CN_VIP*//*@ apply byte_ptr_to_int_ptr_ptr(q_bytes); @*/
+  if (result == 0) {
     *r = 11; // is this free of UB?
     //CN_VIP printf("y=%d *q=%d *r=%d\n",y,*q,*r);
   }

tests/cn_vip_testsuite/provenance_basic_auto_yx.error.c

@@ -1,11 +1,21 @@
 //CN_VIP #include <stdio.h>
 #include <string.h>
+#include <inttypes.h>
+#include "cn_lemmas.h"
 int main() {
   int y=2, x=1;
   int *p = &x + 1;
   int *q = &y;
   //CN_VIP printf("Addresses: p=%p q=%p\n",(void*)p,(void*)q);
-  if (memcmp(&p, &q, sizeof(p)) == 0) {
+  /*CN_VIP*/if (&p == &q) return 0;                                         // CN used to derive disjointness and non-null
+  /*CN_VIP*/if ((uintptr_t)&p + sizeof(uintptr_t) < (uintptr_t)&p) return 0;// constraints from resource ownership, but this
+  /*CN_VIP*/if ((uintptr_t)&q + sizeof(uintptr_t) < (uintptr_t)&q) return 0;// was removed for performance reasons.
+  /*CN_VIP*/unsigned char* p_bytes = owned_int_ptr_to_owned_uchar_arr(&p);
+  /*CN_VIP*/unsigned char* q_bytes = owned_int_ptr_to_owned_uchar_arr(&q);
+  /*CN_VIP*/int result = _memcmp(p_bytes, q_bytes, sizeof(p));
+  /*CN_VIP*//*@ apply byte_ptr_to_int_ptr_ptr(p_bytes); @*/
+  /*CN_VIP*//*@ apply byte_ptr_to_int_ptr_ptr(q_bytes); @*/
+  if (result == 0) {
     *p = 11;  // does this have undefined behaviour?
     //CN_VIP printf("x=%d y=%d *p=%d *q=%d\n",x,y,*p,*q);
   }

tests/cn_vip_testsuite/provenance_basic_global_yx.error.c

@@ -1,11 +1,23 @@
 //CN_VIP #include <stdio.h>
 #include <string.h>
+#include <inttypes.h>
+#include "cn_lemmas.h"
 int y=2, x=1;
-int main() {
+int main()
+/*CN_VIP*//*@ accesses y; @*/
+{
   int *p = &x + 1;
   int *q = &y;
   //CN_VIP printf("Addresses: p=%p q=%p\n",(void*)p,(void*)q);
-  if (memcmp(&p, &q, sizeof(p)) == 0) {
+  /*CN_VIP*/if (&p == &q) return 0;                                         // CN used to derive disjointness and non-null
+  /*CN_VIP*/if ((uintptr_t)&p + sizeof(uintptr_t) < (uintptr_t)&p) return 0;// constraints from resource ownership, but this
+  /*CN_VIP*/if ((uintptr_t)&q + sizeof(uintptr_t) < (uintptr_t)&q) return 0;// was removed for performance reasons.
+  /*CN_VIP*/unsigned char* p_bytes = owned_int_ptr_to_owned_uchar_arr(&p);
+  /*CN_VIP*/unsigned char* q_bytes = owned_int_ptr_to_owned_uchar_arr(&q);
+  /*CN_VIP*/int result = _memcmp(p_bytes, q_bytes, sizeof(p));
+  /*CN_VIP*//*@ apply byte_ptr_to_int_ptr_ptr(p_bytes); @*/
+  /*CN_VIP*//*@ apply byte_ptr_to_int_ptr_ptr(q_bytes); @*/
+  if (result == 0) {
     *p = 11;  // does this have undefined behaviour?
     //CN_VIP printf("x=%d y=%d *p=%d *q=%d\n",x,y,*p,*q);
   }

tests/cn_vip_testsuite/provenance_lost_escape_1.annot.c

@@ -23,8 +23,8 @@ int main()
   /*CN_VIP*/if (&i1 == &i4) return 0;                                         // CN used to derive disjointness and non-null
   /*CN_VIP*/if ((uintptr_t)&i1 + sizeof(uintptr_t) < (uintptr_t)&i1) return 0;// constraints from resource ownership, but this
   /*CN_VIP*/if ((uintptr_t)&i4 + sizeof(uintptr_t) < (uintptr_t)&i4) return 0;// was removed for performance reasons.
-  unsigned char* i1_bytes = owned_uintptr_t_to_owned_uchar_arr(&i1);
-  unsigned char* i4_bytes = owned_uintptr_t_to_owned_uchar_arr(&i4);
+  /*CN_VIP*/unsigned char* i1_bytes = owned_uintptr_t_to_owned_uchar_arr(&i1);
+  /*CN_VIP*/unsigned char* i4_bytes = owned_uintptr_t_to_owned_uchar_arr(&i4);
   /*CN_VIP*/int result = _memcmp(i1_bytes, i4_bytes, sizeof(i1));
   /*CN_VIP*//*@ apply byte_ptr_to_uintptr_t(i1_bytes); @*/
   /*CN_VIP*//*@ apply byte_ptr_to_uintptr_t(i4_bytes); @*/