crucible-llvm: Skip llvm.experimental.noalias.scope.decl and llvm.dbg.assign

crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs

@@ -1942,6 +1942,8 @@ callFunction defSet instr tailCall_ fnTy fn args assign_f
                  , "llvm.dbg.declare"
                  , "llvm.dbg.addr"
                  , "llvm.dbg.value"
+                 , "llvm.dbg.assign" -- Added in LLVM 16
+                 , "llvm.experimental.noalias.scope.decl" -- Added in LLVM 12
                  , "llvm.lifetime.start"
                  , "llvm.lifetime.start.p0"
                  , "llvm.lifetime.start.p0i8"

crux-llvm/test-data/golden/T1196.c

@@ -0,0 +1,14 @@
+void foo(int* restrict p0, int* restrict p1) {
+	*p0 = *p1;
+}
+
+__attribute__((noinline)) void test_inline_foo(int* p0, int* p1) {
+	foo(p0, p1);
+}
+
+int main(void) {
+    int p0 = 0;
+    int p1 = 1;
+    test_inline_foo(&p0, &p1);
+    return 0;
+}

crux-llvm/test-data/golden/T1196.z3.good

@@ -0,0 +1 @@
+[Crux] Overall status: Valid.

crux-llvm/test-data/golden/T1204.c

@@ -0,0 +1,8 @@
+__attribute__((noinline)) int foo(int x[2]) {
+  return x[0];
+}
+
+int main(void) {
+  int x[2] = { 0, 0 };
+  return foo(x);
+}

crux-llvm/test-data/golden/T1204.z3.good

@@ -0,0 +1 @@
+[Crux] Overall status: Valid.