two further clang builtins

regression/ansi-c/builtin_ia32_undef/main.c

@@ -0,0 +1,11 @@
+int main()
+{
+  #ifdef __clang__
+  long long A __attribute__ ((__vector_size__ (16))) =
+    __builtin_ia32_undef128();
+  long long B __attribute__ ((__vector_size__ (32))) =
+    __builtin_ia32_undef256();
+  long long C __attribute__ ((__vector_size__ (64))) =
+    __builtin_ia32_undef512();
+  #endif
+}

regression/ansi-c/builtin_ia32_undef/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ansi-c/builtin_nontemporal_load_store/main.c

@@ -0,0 +1,8 @@
+int main()
+{
+  #ifdef __clang__
+  int var, value;
+  __builtin_nontemporal_store(1, &var);
+  value = __builtin_nontemporal_load(&var);
+  #endif
+}

regression/ansi-c/builtin_nontemporal_load_store/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--

src/ansi-c/c_typecheck_expr.cpp

@@ -252,7 +252,12 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
   }
   else if(expr.id()==ID_clang_builtin_convertvector)
   {
+    // This has one operand and a type, and acts like a typecast
+    DATA_INVARIANT(expr.operands().size()==1, "clang_builtin_convertvector has one operand");
     typecheck_type(expr.type());
+    typecast_exprt tmp(expr.op0(), expr.type());
+    tmp.add_source_location()=expr.source_location();
+    expr.swap(tmp);
   }
   else if(expr.id()==ID_builtin_offsetof)
     typecheck_expr_builtin_offsetof(expr);
@@ -2192,6 +2197,31 @@ exprt c_typecheck_baset::do_special_functions(
 
     return bswap_expr;
   }
+  else if(identifier=="__builtin_nontemporal_load")
+  {
+    typecheck_function_call_arguments(expr);
+
+    if(expr.arguments().size()!=1)
+    {
+      err_location(f_op);
+      error() << identifier << " expects one operand" << eom;
+      throw 0;
+    }
+
+    // these return the subtype of the argument
+    exprt &ptr_arg=expr.arguments().front();
+
+    if(ptr_arg.type().id()!=ID_pointer)
+    {
+      err_location(f_op);
+      error() << "__builtin_nontemporal_load takes pointer as argument" << eom;
+      throw 0;
+    }
+
+    expr.type()=expr.arguments().front().type().subtype();
+
+    return expr;
+  }
   else if(
     identifier == "__builtin_fpclassify" ||
     identifier == CPROVER_PREFIX "fpclassify")

src/ansi-c/clang_builtin_headers.h

@@ -1,3 +1,10 @@
 __gcc_v4sf __builtin_shufflevector(__gcc_v4sf, __gcc_v4sf, ...);
 
+__gcc_v2di __builtin_ia32_undef128(void);
+__gcc_v4di __builtin_ia32_undef256(void);
+__gcc_v8di __builtin_ia32_undef512(void);
+
+void __builtin_nontemporal_store();
+void __builtin_nontemporal_load();
+
 int __builtin_flt_rounds(void);