/*
  square_root2: A demonstration/test program for the GEF (General Exception-
  Handling Facility) library.
  Demonstrates the use of programming by contract.
  Copyright (C) 1998-2006 Bruce W. Bigby, bbigby@alum.MIT.edu

  This program is free software; you can redistribute it and/or
  modify it under the terms of the GNU General Public License
  as published by the Free Software Foundation; either version 2
  of the License, or (at your option) any later version.

  This program is distributed in the hope that it will be useful,
  but WITHOUT ANY WARRANTY; without even the implied warranty of
  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  GNU General Public License for more details.

  You should have received a copy of the GNU General Public License
  along with this program; if not, write to the Free Software
  Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.
*/

#include <stdio.h>
#include <stdlib.h>
#include <math.h>
#ifdef GEF_POSIX
#include <signal.h>
#endif

#ifdef GEF_POSIX
#ifdef GEF_PTHREADS
#include <gef/pthreads.h>
#else
#include <gef/posix.h>
#endif
#else
#include <gef/ansi.h>
#endif


/* #define USE_GEF_EXCEPTION_CODES */

#ifndef USE_GEF_EXCEPTION_CODES
#define EXCEPT_UNHANDLED_EXCEPTION 1
#define EXCEPT_INSUFFICIENT_MEMORY 2
#define EXCEPT_ASSERTION_VIOLATION 3
#define EXCEPT_PRECONDITION_VIOLATION 4
#define EXCEPT_POSTCONDITION_VIOLATION 5
#define EXCEPT_PREINVARIANT_VIOLATION 6
#define EXCEPT_POSTINVARIANT_VIOLATION 7
#endif

#define EXCEPT_OS_VIOLATION         8
#define EXCEPT_ARITHMETIC_VIOLATION 9

#ifndef USE_GEF_EXCEPTION_CODES
static
void
InsufficientMemory() {
    gef_throw((void*) EXCEPT_INSUFFICIENT_MEMORY);
}

static
void
AssertionViolation(const char* expString, const char* fileName, const char* function, int lineNumber) {
    /* Can only transfer fileName and lineNumber info via a pointer to a */
    /* structure.  For now, simply throw the integer value,              */
    fprintf(stderr, "Assertion Violation\n");
    fprintf(stderr, "Assertion: %s\nFilename: %s\nFunction: %s\nLine number: %d\n",
        expString, fileName, function, lineNumber);
    gef_throw((void*) EXCEPT_ASSERTION_VIOLATION);
}

static
void
PreconditionViolation(const char* expString, const char* fileName, const char* function, int lineNumber) {
    /*
      Can only transfer fileName and lineNumber info via a pointer to a
       structure.  For now, simply throw the integer value.
       */
    fprintf(stderr, "Precondition Violation\n");
    fprintf(stderr, "Assertion: %s\nFilename: %s\nFunction: %s\nLine number: %d\n",
        expString, fileName, function, lineNumber);
    gef_throw((void*) EXCEPT_PRECONDITION_VIOLATION);
}

static
void
PostconditionViolation(const char* expString, const char* fileName, const char* function, int lineNumber) {
    /*
      Can only transfer fileName and lineNumber info via a pointer to a
       structure.  For now, simply throw the integer value.
       */
    fprintf(stderr, "Postcondition Violation\n");
    fprintf(stderr, "Assertion: %s\nFilename: %s\nFunction: %s\nLine number: %d\n",
        expString, fileName, function, lineNumber);
    gef_throw((void*) EXCEPT_POSTCONDITION_VIOLATION);
}

static
void
PreInvariantViolation(const char* expString, const char* fileName, const char* function, int lineNumber) {
    /*
      Can only transfer fileName and lineNumber info via a pointer to a
       structure.  For now, simply throw the integer value.
       */
    fprintf(stderr, "Pre-Invariant Violation\n");
    fprintf(stderr, "Assertion: %s\nFilename: %s\nFunction: %s\nLine number: %d\n",
        expString, fileName, function, lineNumber);
    gef_throw((void*) EXCEPT_PREINVARIANT_VIOLATION);
}

static
void
PostInvariantViolation(const char* expString, const char* fileName, const char* function, int lineNumber) {
    /*
      Can only transfer fileName and lineNumber info via a pointer to a
       structure.  For now, simply throw the integer value.
       */
    fprintf(stderr, "Post-Invariant Violation\n");
    fprintf(stderr, "Assertion: %s\nFilename: %s\nFunction: %s\nLine number: %d\n",
        expString, fileName, function, lineNumber);
    gef_throw((void*) EXCEPT_POSTINVARIANT_VIOLATION);
}

static
void
UnhandledException(void* exceptionID) {
    fprintf(stderr, "\tUnhandled exception, %d, occurred, while executing process, %d.\n",((int) exceptionID), (int) getpid());
}
#endif

#ifdef GEF_POSIX
static
void*
OSSignalToException(int signum) {
    switch (signum) {
    case SIGFPE:
        return((void*) EXCEPT_ARITHMETIC_VIOLATION);
    default:
        return((void*) EXCEPT_OS_VIOLATION);
    }
}
#endif

int
matherr(struct exception* e) {
    gef_throw((void*) EXCEPT_ARITHMETIC_VIOLATION);
}

static
double
SquareRoot(double number) {
    double answer;
    gef_volatile_try_with_postconditions {
        answer = sqrt(number);
    } gef_preconditions {
        gef_assert_precondition(number >= 0.0);
    } gef_postconditions {
        gef_assert_postcondition(fabs(number - answer * answer) < 0.0001);
    } gef_end;
    return(answer);
}

int
main(int argc, char** argv) {
    double answer;
    double number;
    int exitCode = 0;
#ifdef GEF_POSIX
    sigset_t osSignalSet;
#endif
    GEFAttr_t gefAttrs;

    /* Configure GEF for process. */
    GEFInitialize(&argc, &argv);

    if (argc != 2) {
        fprintf(stderr, "Usage: %s decimal\n", argv[0]);
        exit(1);
    }

#ifdef GEF_POSIX
    sigemptyset(&osSignalSet);
    sigaddset(&osSignalSet, SIGFPE);
    GEFInitializeSignals(osSignalSet);
#endif
    /* Configure GEF for thread */
    GEFAttr_Init(&gefAttrs);
#ifndef USE_GEF_EXCEPTION_CODES
    GEFAttr_SetAssertionViolation(&gefAttrs, AssertionViolation);
    GEFAttr_SetPreconditionViolation(&gefAttrs, PreconditionViolation);
    GEFAttr_SetPostconditionViolation(&gefAttrs, PostconditionViolation);
    GEFAttr_SetPreInvariantViolation(&gefAttrs, PreInvariantViolation);
    GEFAttr_SetPostInvariantViolation(&gefAttrs, PostInvariantViolation);
    GEFAttr_SetUnhandledException(&gefAttrs, UnhandledException);
    GEFAttr_SetOutOfMemory(&gefAttrs, InsufficientMemory);
#endif

#ifdef GEF_POSIX
    GEFAttr_SetOSSignalToException(&gefAttrs, OSSignalToException);
#endif
    /* You still need to make the call to GEFInitializeThread, even when you do not compile with PTHREADS */
    GEFInitializeThread(gefAttrs);
    gef_enable_assertions;
    gef_volatile_try {
        number = atof(argv[1]);
        answer = SquareRoot(number);
        printf("%.2f\n",  answer);
    } gef_preconditions {
        gef_assert_precondition(argc == 2);
    } gef_catch(exception) {
        switch ((int) exception) {
        case EXCEPT_ARITHMETIC_VIOLATION:
            fprintf(stderr, "%s: Cannot produce square root of %.2f!\n", argv[0], number);
            exitCode = 1;
            gef_break;
#ifndef USE_GEF_EXCEPTION_CODES
        case EXCEPT_ASSERTION_VIOLATION:
            fprintf(stderr, "%s: Assertion violation!\n", argv[0]);
            exitCode = 1;
            gef_break;
        case EXCEPT_PRECONDITION_VIOLATION:
            fprintf(stderr, "%s: Precondition violation!\n", argv[0]);
            exitCode = 1;
            gef_break;
        case EXCEPT_POSTCONDITION_VIOLATION:
            fprintf(stderr, "%s: Postcondition violation!\n", argv[0]);
            exitCode = 1;
            gef_break;
        case EXCEPT_PREINVARIANT_VIOLATION:
            fprintf(stderr, "%s: Pre-Invariant violation!\n", argv[0]);
            exitCode = 1;
            gef_break;
        case EXCEPT_POSTINVARIANT_VIOLATION:
            fprintf(stderr, "%s: Post-Invariant violation!\n", argv[0]);
            exitCode = 1;
            gef_break;
#else
        case GEF_EXCEPTION_ASSERTION_VIOLATION:
            fprintf(stderr, "%s: Assertion violation!\n", argv[0]);
            exitCode = 1;
            gef_break;
        case GEF_EXCEPTION_PRECONDITION_VIOLATION:
            fprintf(stderr, "%s: Precondition violation!\n", argv[0]);
            exitCode = 1;
            gef_break;
        case GEF_EXCEPTION_POSTCONDITION_VIOLATION:
            fprintf(stderr, "%s: Postcondition violation!\n", argv[0]);
            exitCode = 1;
            gef_break;
        case GEF_EXCEPTION_PREINVARIANT_VIOLATION:
            fprintf(stderr, "%s: Pre-Invariant violation!\n", argv[0]);
            exitCode = 1;
            gef_break;
        case GEF_EXCEPTION_POSTINVARIANT_VIOLATION:
            fprintf(stderr, "%s: PostInvariant violation!\n", argv[0]);
            exitCode = 1;
            gef_break;
#endif
        default: break;
        }
    } gef_end;
    exit(exitCode);
}