Line data    Source code

       1             : #include <array_list_helper.h>
       2             : #include <nondet.h>
       3             : #include <priority_queue_helper.h>
       4             : 
       5           0 : int nd_aws_priority_queue_compare_fn(const void *a, const void *b) {
       6           0 :   return nd_int();
       7           0 : }
       8             : 
       9      600000 : void initialize_priority_queue(struct aws_priority_queue *queue) {
      10      600000 :   queue->pred = nd_aws_priority_queue_compare_fn;
      11      600000 :   initialize_bounded_array_list(&queue->container);
      12      600000 :   initialize_bounded_array_list(&queue->backpointers);
      13      600000 : }
      14             : 
      15             : bool aws_priority_queue_is_bounded(struct aws_priority_queue *queue,
      16             :                                    const size_t max_initial_item_allocation,
      17      524179 :                                    const size_t max_item_size) {
      18      524179 :   bool b1 = aws_array_list_is_bounded(
      19      524179 :       &queue->container, max_initial_item_allocation, max_item_size);
      20      524179 :   bool b2 = aws_array_list_is_bounded(&queue->backpointers,
      21      524179 :                                       max_initial_item_allocation,
      22      524179 :                                       sizeof(struct aws_priority_queue_node *));
      23      524179 :   return b1 && b2;
      24      524179 : }