Handle MSVC's __noop in type checker

The documentation states that it does not generate any code other than
`0`. Hence, don't maintain a library function, but instead discard the
expression in the type checker.

Author: tautschnig

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-library/__noop-01/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/main.c

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

regression/cbmc/noop1/test.desc

@@ -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/noop2/main.c

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

…ression/cbmc-library/__noop-01/test.desc regression/cbmc/noop2/test.descregression/cbmc-library/__noop-01/test.desc renamed to regression/cbmc/noop2/test.desc regression/cbmc-library/__noop-01/test.desc renamed to regression/cbmc/noop2/test.desc

@@ -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/ansi_c_internal_additions.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()))