Add string.h to memcpy_s.c and remove casts in the implementation

Signed-off-by: Hernan Ponce de Leon <[email protected]>

benchmarks/c/miscellaneous/memcpy_s.c

@@ -1,5 +1,6 @@
 #include <assert.h>
 #include <stddef.h>
+#include <string.h>
 
 int main()
 {
@@ -22,12 +23,13 @@ int main()
     b[1] = 6;
     b[2] = 7;
 
-    // count > dest
-    ret = memcpy_s(b, 3*sizeof(int), a, 4*sizeof(int));
+    // count > destsz
+    ret = memcpy_s(b, 2*sizeof(int), a, 4*sizeof(int));
     assert(ret > 0);
     assert(b[0] == 0);
     assert(b[1] == 0);
-    assert(b[2] == 0);
+    // only [dest, dest+destsz) is zeroed
+    assert(b[2] == 7);
     b[0] = 5;
     b[1] = 6;
     b[2] = 7;

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java

@@ -1358,17 +1358,13 @@ private List<Event> inlineMemCpyS(FunctionCall call) {
         final Expression srcIsNull = expressions.makeEQ(src, nullExpr);
         // We assume RSIZE_MAX = 2^64-1
         final Expression rsize_max = expressions.makeValue(BigInteger.ONE.shiftLeft(64).subtract(BigInteger.ONE), types.getArchType());
-        final Expression invalidDestsz = expressions.makeGT(
-                expressions.makeCast(destszExpr, types.getArchType()), rsize_max, false);
-        final Expression countGtMax = expressions.makeGT(
-                expressions.makeCast(countExpr, types.getArchType()), rsize_max, false);
+        final Expression invalidDestsz = expressions.makeGT(destszExpr, rsize_max, false);
+        final Expression countGtMax = expressions.makeGT(countExpr, rsize_max, false);
         final Expression countGtdestszExpr = expressions.makeGT(countExpr, destszExpr, false);
         final Expression invalidCount = expressions.makeOr(countGtMax, countGtdestszExpr);
-        // src and dest are pointers (int64), count is usually interpreted as int32, thus the cast
-        final Expression countExprCast = expressions.makeCast(countExpr, types.getArchType());
         final Expression overlap = expressions.makeAnd(
-                expressions.makeGTE(expressions.makeAdd(src, countExprCast), dest, false),
-                expressions.makeGTE(expressions.makeAdd(dest, countExprCast), src, false));
+                expressions.makeGTE(expressions.makeAdd(src, countExpr), dest, false),
+                expressions.makeGTE(expressions.makeAdd(dest, countExpr), src, false));
 
         final List<Event> replacement = new ArrayList<>();