From 3c03ce87bdef3bad16f90843a573f526a40b4299 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 18 Feb 2010 11:22:50 +0000 Subject: [PATCH] Missing files from last commit. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1736 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- cudd/LICENSE | 31 +++++++++ cudd/MODIFICATIONS | 154 ++++++++++++++++++++++++++++++++++++++++++++ cudd/util/restart.c | 137 +++++++++++++++++++++++++++++++++++++++ 3 files changed, 322 insertions(+) create mode 100644 cudd/LICENSE create mode 100644 cudd/MODIFICATIONS create mode 100644 cudd/util/restart.c diff --git a/cudd/LICENSE b/cudd/LICENSE new file mode 100644 index 00000000..99c7fbae --- /dev/null +++ b/cudd/LICENSE @@ -0,0 +1,31 @@ +Copyright (c) 1995-2004, Regents of the University of Colorado + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: + +Redistributions of source code must retain the above copyright +notice, this list of conditions and the following disclaimer. + +Redistributions in binary form must reproduce the above copyright +notice, this list of conditions and the following disclaimer in the +documentation and/or other materials provided with the distribution. + +Neither the name of the University of Colorado nor the names of its +contributors may be used to endorse or promote products derived from +this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS +FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE +COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, +INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, +BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; +LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER +CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT +LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN +ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE +POSSIBILITY OF SUCH DAMAGE. diff --git a/cudd/MODIFICATIONS b/cudd/MODIFICATIONS new file mode 100644 index 00000000..da4a8ee2 --- /dev/null +++ b/cudd/MODIFICATIONS @@ -0,0 +1,154 @@ +This file describes the modifications that have been made to this version of CUDD. +It is based on CUDD 2.4.2. Below is a list of the files that have been changed. + + * Makefile + * setup.sh . + * shutdown.sh . + * cudd/cuddAddAbs.c + * cudd/cuddAddApply.c + * cudd/cuddAddNeg.c + * cudd/cuddExport.c + * cudd/cuddSat.c + * cudd/cuddTable.c + * cudd/cudd.h + * cudd/cuddInt.h + * util/Makefile + * util/cpu_time.c + * util/pipefork.c + +The following structural changes have also been made: + + * ddmp/nanotrav/mnemosyne/obj/sis and various doc directories have been removed + * lib directory added with symlinks to lib files + + +Details +------- + +[Makefile] + +* Disabled building of nanotrav/mnemosyne packages (don't need) + +* Default options are for Linux (original makefile is in Makefile.orig) + +------------------ + +[setup.sh] + +* Don't create links for includes we don't use +* Create links for libs too + +------------------ + +[shutdown.sh] + +* Delete lib directory too + +------------------ + +[cudd/cuddAddAbs.c] + +* Added 2 more abstraction functions to do min/max, ie: + Cudd_addMinAbstract() + Cudd_addMaxAbstract() + cuddAddMinAbstractRecur() + cuddAddMaxAbstractRecur() + +* Added another abstraction functions to do "first", ie: + Cudd_addFirstAbstract() + cuddAddFirstAbstractRecur() + +------------------ + +[cudd/cuddAddApply.c] + +* Added the following functions to be used with Cudd_addApply() + Cudd_addEquals() - f op g = 1 if f==g else 0 + Cudd_addNotEquals() - f op g = 1 if f!=g else 0 + Cudd_addGreaterThan() - f op g = 1 if f>g else 0 + Cudd_addGreaterThanEquals() - f op g = 1 if f>=g else 0 + Cudd_addLessThan() - f op g = 1 if f so that MingW version + can specify that it doesn't have it. + diff --git a/cudd/util/restart.c b/cudd/util/restart.c new file mode 100644 index 00000000..b81dcb8c --- /dev/null +++ b/cudd/util/restart.c @@ -0,0 +1,137 @@ +#include +#include "util.h" + +#if (defined(sun) && ! defined(sparc)) || defined(vax) + +#include +#include +#include + +static char *save_stack_base; +static char *stack_lo_addr; +static char *stack_hi_addr; +static int stack_size; + +static int restart_global_flag; +static char *old_file_name; +static char *new_file_name; + +char *util_save_sp; /* set by util_restart_save_state() */ +extern char *sbrk(); + +static void +grow_stack() +{ + int i, space[256]; + + for(i = 0; i < 256; i++) { + space[i] = 0; + } + if ((char *) &i > stack_lo_addr) { + grow_stack(); + } +} + + +/* ARGSUSED */ +static int +handle_sigquit(int sig, int code, struct sigcontext *scp) +{ + if (util_restart_save_state()) { + /* we are restarting ! -- return from signal */ + + } else { + /* copy stack to user data space */ + stack_lo_addr = util_save_sp; + stack_size = stack_hi_addr - stack_lo_addr + 1; + save_stack_base = sbrk(stack_size); + (void) memcpy(save_stack_base, stack_lo_addr, stack_size); + + /* write a new executable */ + (void) fprintf(stderr, "Writing executable %s ...\n", new_file_name); + (void) util_save_image(old_file_name, new_file_name); + + /* terminate if signal was a QUIT */ + if (sig == SIGQUIT) { + (void) _exit(1); + } + } +} + + +static void +restart_program() +{ + (void) fprintf(stderr, "Continuing execution ...\n"); + + /* create the stack */ + grow_stack(); + +#ifdef vax + asm("movl _util_save_sp,sp"); +#endif +#ifdef sun + asm("movl _util_save_sp,sp"); +#endif + + /* copy the stack back from user space */ + (void) memcpy(stack_lo_addr, save_stack_base, stack_size); + + /* remove the sbrk for the stack */ + if (sbrk(-stack_size) < 0) { + perror("sbrk"); + } + + util_restart_restore_state(); /* jump back into handle_sigquit() */ +} + +void +util_restart(char const *old, char const *neW, int interval) +{ + struct itimerval itimer; + +#ifdef vax +#ifdef ultrix + stack_hi_addr = (char *) 0x7fffe3ff; /* ultrix */ +#else + stack_hi_addr = (char *) 0x7fffebff; /* bsd 4.3 */ +#endif +#endif +#ifdef sun + stack_hi_addr = (char *) 0x0effffff; /* Sun OS 3.2, 3.4 */ +#endif + + old_file_name = old; + new_file_name = neW; + + (void) signal(SIGQUIT, handle_sigquit); + + if (interval > 0) { + (void) signal(SIGVTALRM, handle_sigquit); + itimer.it_interval.tv_sec = interval; + itimer.it_interval.tv_usec = 0; + itimer.it_value.tv_sec = interval; + itimer.it_value.tv_usec = 0; + if (setitimer(ITIMER_VIRTUAL, &itimer, (struct itimerval *) 0) < 0) { + perror("setitimer"); + exit(1); + } + } + + if (restart_global_flag) { + restart_program(); + } + restart_global_flag = 1; +} + +#else + +/* ARGSUSED */ +void +util_restart(char const *old, char const *neW, int interval) +{ + (void) fprintf(stderr, + "util_restart: not supported on your operating system/hardware\n"); +} + +#endif