Replace abort() with assert(0) so that CBMC catches it (#444)

* Replace abort() with assert(0) so that CBMC catches it

* Make AWS_FATAL_ASSERT to be assert when using CBMC

.cbmc-batch/jobs/Makefile.common

@@ -90,6 +90,11 @@ DEFAULT_REMOVE_FUNCTION_BODY += --remove-function-body s_default_free
 DEFAULT_REMOVE_FUNCTION_BODY += --remove-function-body s_default_malloc
 DEFAULT_REMOVE_FUNCTION_BODY += --remove-function-body s_default_realloc
 ################################################################
+# We override abort() to be assert(0), as it is not caught by
+# CBMC as a violation
+ABSTRACTIONS += $(HELPERDIR)/stubs/abort_override_assert_false.c
+DEFAULT_REMOVE_FUNCTION_BODY += --remove-function-body abort
+################################################################
 
 REMOVE_FUNCTION_BODY ?= $(DEFAULT_REMOVE_FUNCTION_BODY)
 REMOVE_FUNCTION_BODY += $(ADDITIONAL_REMOVE_FUNCTION_BODY)

.cbmc-batch/stubs/abort_override_assert_false.c

@@ -0,0 +1,26 @@
+/*
+ * Copyright 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License"). You may not use
+ * this file except in compliance with the License. A copy of the License is
+ * located at
+ *
+ *     http://aws.amazon.com/apache2.0/
+ *
+ * or in the "license" file accompanying this file. This file is distributed on an
+ * "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+ * implied. See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+/**
+ * FUNCTION: abort
+ *
+ * We override abort to be an assert(0) so that it is caught by CBMC
+ */
+
+#include <stdint.h>
+
+void abort() {
+    assert(0);
+}

include/aws/common/assert.h

@@ -38,7 +38,18 @@ void aws_backtrace_print(FILE *fp, void *call_site_data);
 
 AWS_EXTERN_C_END
 
-#if defined(CBMC) || __clang_analyzer__
+#if defined(CBMC)
+#    include <assert.h>
+#    define AWS_ASSERT(cond) assert(cond)
+#elif defined(DEBUG_BUILD) || __clang_analyzer__
+#    define AWS_ASSERT(cond) AWS_FATAL_ASSERT(cond)
+#else
+#    define AWS_ASSERT(cond)
+#endif /*  defined(CBMC) */
+
+#if defined(CBMC)
+#    define AWS_FATAL_ASSERT(cond) AWS_ASSERT(cond)
+#elif __clang_analyzer__
 #    define AWS_FATAL_ASSERT(cond)                                                                                     \
         if (!(cond)) {                                                                                                 \
             abort();                                                                                                   \
@@ -57,16 +68,7 @@ AWS_EXTERN_C_END
                 aws_fatal_assert(#cond, __FILE__, __LINE__);                                                           \
             }
 #    endif /* defined(_MSC_VER) */
-#endif     /* defined(CBMC) || __clang_analyzer__ */
-
-#if defined(CBMC)
-#    include <assert.h>
-#    define AWS_ASSERT(cond) assert(cond)
-#elif defined(DEBUG_BUILD) || __clang_analyzer__
-#    define AWS_ASSERT(cond) AWS_FATAL_ASSERT(cond)
-#else
-#    define AWS_ASSERT(cond)
-#endif /*  defined(CBMC) */
+#endif     /* defined(CBMC) */
 
 /**
  * Define function contracts.