cleaned up some tests

examples/concepts/cpp/Arrays.cpp

@@ -3,12 +3,19 @@
 //:: tools silicon
 //:: verdict Pass
 
-//@ requires a != nullptr && size > 0;
+//@ requires size > 0;
 //@ context \pointer(a, size, read);
 //@ requires (\forall int i = 0 .. size; {: a[i] :} == 0);
 //@ ensures \result == b;
 int sumWithLast(int a[], int size, int b) {
 	int sum = a[size-1] + b;
 	//@ assert a[size-1] == 0;
 	return sum;
+}
+
+//@ requires size > 2;
+//@ context \pointer(a, size, write);
+//@ ensures a[2] == 5;
+void writeToArray(int a[], int size) {
+	a[2] = 5;
 }

examples/concepts/cpp/Pointers.cpp

@@ -3,34 +3,10 @@
 //:: tools silicon
 //:: verdict Pass
 
-// Examples taken from https://en.cppreference.com/w/cpp/language/pointer
-
-
-// &x is not supported but I do need it for SYCL buffers
 //@ context \pointer(ints, size, write);
 void test(int ints[], int size, int* p) {
-	//	char x = 'a';
-	//	char* charPtr = &x;
-	// assert *charPtr == x;
-
-	int arr[5];
-	//	int* arrPtr[5] = &arr;
-	// assert arrPtr[4] == arr[4];
-
-// Does not support arrays containing pointers?
-//	int* ptrArr[5];
-//	ptrArr[2] = p;
-
+	int* intsPtr = ints;
+	//@ assert intsPtr == ints;
 
 	void* voidPtr = nullptr;
-
-	int n;
-	//  int* p = &n;
-	//  *p = 10;
-  // assert n == 10;
-
-  if (size >= 4) {
-  	ints[3] = 5;
-  }
-   //@ assert size >= 4 ==> ints[3] == 5;
 }

examples/concepts/cpp/Types.cpp

@@ -7,13 +7,11 @@ void test() {
 	bool aBool = true;
 
 	int anInt = 5;
-	//short aShort = 5;
 	long aLong = 5;
 	double aDouble = 5.1;
 	float aFloat = 5.1;
 
 	char aChar = 'a';
-//	char aCharArray[] = "Hello there";
 
 	void* voidPtr = nullptr;
 }