Handle MSVC's __noop in type checker

regression/ansi-c/noop1/main.c

@@ -0,0 +1,15 @@
+// this is permitted - __noop yields a compile-time constant 0
+int array[__noop() + 1];
+
+struct S
+{
+  int x;
+};
+
+int main(int argc, char *argv)
+{
+  struct S s;
+  // the arguments to __noop are type checked, and thus the following is not
+  // permitted
+  __noop((char *)s);
+}

regression/ansi-c/noop1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--i386-win32
+type cast from 'struct S' not permitted
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/noop1/main.c

@@ -1,9 +1,7 @@
-#include <assert.h>
-
 int some_function()
 {
   // this will not be executed
-  assert(0);
+  __CPROVER_assert(0, "not executed");
 }
 
 int main()

regression/cbmc/noop1/test.desc

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

regression/cbmc/noop2/main.c

@@ -0,0 +1,6 @@
+int main(int argc, char *argv)
+{
+  int x = 0;
+  __noop(++x);
+  __CPROVER_assert(x == 0, "__noop ignores side effects");
+}

regression/cbmc-library/__noop-01/test.desc → regression/cbmc/noop2/test.desc

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+-win32
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

src/ansi-c/ansi_c_internal_additions.cpp

@@ -295,8 +295,7 @@ void ansi_c_internal_additions(std::string &code)
 
   // this is Visual C/C++ only
   if(config.ansi_c.os==configt::ansi_ct::ost::OS_WIN)
-    code+="int __noop();\n"
-          "int __assume(int);\n";
+    code += "int __assume(int);\n";
 
   // ARM stuff
   if(config.ansi_c.mode==configt::ansi_ct::flavourt::ARM)

src/ansi-c/c_typecheck_expr.cpp

@@ -1884,6 +1884,20 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
       {
         // yes, it's a builtin
       }
+      else if(
+        identifier == "__noop" &&
+        config.ansi_c.mode == configt::ansi_ct::flavourt::VISUAL_STUDIO)
+      {
+        // https://docs.microsoft.com/en-us/cpp/intrinsics/noop
+        // typecheck and discard, just generating 0 instead
+        for(auto &op : expr.arguments())
+          typecheck_expr(op);
+
+        exprt result = from_integer(0, signed_int_type());
+        expr.swap(result);
+
+        return;
+      }
       else if(
         auto gcc_polymorphic = typecheck_gcc_polymorphic_builtin(
           identifier, expr.arguments(), f_op.source_location()))

src/ansi-c/library_check.sh

@@ -10,7 +10,6 @@ for f in "$@"; do
     perl -p -i -e 's/(_mm_.fence)/s$1/' __libcheck.c
     perl -p -i -e 's/(__sync_)/s$1/' __libcheck.c
     perl -p -i -e 's/(__atomic_)/s$1/' __libcheck.c
-    perl -p -i -e 's/(__noop)/s$1/' __libcheck.c
     "$CC" -std=gnu99 -E -include library/cprover.h -D__CPROVER_bool=_Bool -D__CPROVER_thread_local=__thread -DLIBRARY_CHECK -o __libcheck.i __libcheck.c
     "$CC" -S -Wall -Werror -pedantic -Wextra -std=gnu99 __libcheck.i \
       -o __libcheck.s -Wno-unused-label -Wno-unknown-pragmas

src/ansi-c/windows_builtin_headers.h

@@ -1,2 +1 @@
-int __noop();
 int __assume(int);

src/goto-programs/goto_clean_expr.cpp

@@ -387,18 +387,6 @@ void goto_convertt::clean_expr(
         return;
       }
     }
-    else if(statement==ID_function_call)
-    {
-      if(to_side_effect_expr_function_call(expr).function().id()==ID_symbol &&
-         to_symbol_expr(
-           to_side_effect_expr_function_call(expr).
-           function()).get_identifier()=="__noop")
-      {
-        // __noop needs special treatment, as arguments are not
-        // evaluated
-        to_side_effect_expr_function_call(expr).arguments().clear();
-      }
-    }
   }
   else if(expr.id()==ID_forall || expr.id()==ID_exists)
   {

src/goto-programs/goto_convert_function_call.cpp

@@ -53,13 +53,6 @@ void goto_convertt::do_function_call(
 
   clean_expr(new_function, dest, mode);
 
-  // the arguments of __noop do not get evaluated
-  if(new_function.id()==ID_symbol &&
-     to_symbol_expr(new_function).get_identifier()=="__noop")
-  {
-    new_arguments.clear();
-  }
-
   Forall_expr(it, new_arguments)
     clean_expr(*it, dest, mode);