text: /*  Boolector: Satisfiability Modulo Theories (SMT) solver.
   *
   *  Copyright (C) 2007-2021 by the authors listed in the AUTHORS file.
   *
   *  This file is part of Boolector.
   *  See COPYING for more information on using this software.
   */
  
  #include "btorabort.h"
  
  #include "btorexit.h"
  #include "btortypes.h"
  #include "utils/btormem.h"
  
  #include <assert.h>
  #include <stdio.h>
  
  #define BUFFER_LEN 255
  
  void
  btor_abort_fun (const char* msg)
  {
    fflush (stdout);
    fflush (stderr);
    fprintf (stderr, "%s", msg);
    fflush (stderr);
    exit (BTOR_ERR_EXIT);
  }
  
  void
  btor_abort_warn (
      bool abort, const char *filename, const char *fun, const char *fmt, ...)
  {
    size_t i;
    const char* warning = "WARNING: ";
    char *s, *e, *p;
    /* do not allocate on heap, since in case of an abort due to mem out heap
     * allocation might fail */
    char buffer[BUFFER_LEN];
    va_list list;
  
    e = strrchr (filename, '.');
    s = strrchr (filename, '/');
    s = s ? s + 1 : (char *) filename;
  
    i = 0;
    buffer[i++] = '[';
    for (p = s; p < e && i < BUFFER_LEN; p++) buffer[i++] = *p;
  
    assert (i <= BUFFER_LEN);
    i += snprintf (buffer+i, BUFFER_LEN - i, "] %s: ", fun);
  
    if (!abort)
    {
      assert (i <= BUFFER_LEN);
      i += snprintf (buffer+i, BUFFER_LEN -i, "%s", warning);
    }
    va_start (list, fmt);
    assert (i <= BUFFER_LEN);
    i += vsnprintf (buffer+i, BUFFER_LEN - i, fmt, list);
    va_end (list);
  
    assert (i <= BUFFER_LEN);
    snprintf (buffer+i, BUFFER_LEN - i, "\n");
    if (abort)
      btor_abort_callback.abort_fun (buffer);
    else
    {
      fflush (stdout);
      fflush (stderr);
      fprintf (stderr, "%s\n", buffer);
      fflush (stderr);
    }
  }
  