Merge pull request #59 from GaloisInc/bugfix-cn-failing-on-stdio

Don't include stdio.h when using CN

components/mission_protection_system/src/components/actuator.c

@@ -19,10 +19,17 @@
 #include "actuation_logic.h"
 
 #ifdef PLATFORM_HOST
+// CN currently does not support <stdio.h>
+// see https://github.com/rems-project/cerberus/issues/277
+// for details
+#ifdef CN_ENV
+#include "printf.h"
+#else // CN_ENV not defined
 #include <stdio.h>
-#else
+#endif // define CN_ENV
+#else // PLATFORM_HOST not defined
 #include "printf.h"
-#endif
+#endif // ifdef PLATFORM_HOST
 
 #define w1 uint8_t
 #define w2 uint8_t

components/mission_protection_system/src/include/wars.h

@@ -1,5 +1,10 @@
 // general things not yet supported by CN
 
+// define that we are using CN for code checking
+// NOTE: eventually we don't want to differentiate between the checked
+// code and the deployed code
+#define CN_ENV 1
+
 // the simplest workaround for unions (making it a struct) don't make sense if
 // the union is used to access the same data from different perspectives, but if
 // it's just used as a simple sum type it's merely wasteful to use a struct