Line data    Source code

       1             : /*
       2             :  *
       3             :  */
       4             : 
       5             : #include <aws/common/string.h>
       6             : #include <byte_buf_helper.h>
       7             : #include <seahorn/seahorn.h>
       8             : #include <stddef.h>
       9             : #include <string_helper.h>
      10             : #include <utils.h>
      11             : 
      12           0 : int main(void) {
      13           0 :   struct aws_string *str =
      14           0 :       ensure_string_is_allocated_bounded_length(MAX_STRING_LEN);
      15           0 :   char unsigned const *bytes = str->bytes;
      16           0 :   size_t len = str->len;
      17           0 :   /* Tell CBMC to keep the buffer live after the free */
      18           0 :   /* __CPROVER_allocated_memory(bytes, len); */
      19           0 :   bool nondet_parameter = nd_bool();
      20           0 :   aws_string_destroy_secure(nondet_parameter ? str : NULL);
      21           0 :   if (nondet_parameter) {
      22             :     #ifdef __KLEE__
      23             :     // str (even bytes) becomes a dangling pointer used after free
      24             :     // klee does not allow to access memory after free.
      25             :     #else
      26             :     assert_all_zeroes(bytes, len);
      27           0 :     #endif
      28           0 :   }
      29           0 :   return 0;
      30           0 : }