From bdd5274e072da364c97741f245f318865fdd4888 Mon Sep 17 00:00:00 2001 From: Gene Cooperman Date: Mon, 7 Oct 2024 11:33:00 -0400 Subject: [PATCH] McMini 1.0.0 release --- COPYING.md | 2 +- Makefile.in | 5 +- NEWS | 11 ++++ VERSION | 1 + configure | 44 +++++++-------- configure.ac | 9 ++-- include/config.h.in | 127 +++++++++++++++++++++++++++++++++++++++++++- 7 files changed, 170 insertions(+), 29 deletions(-) create mode 100644 NEWS create mode 100644 VERSION diff --git a/COPYING.md b/COPYING.md index e3e6c97f..68ccf3ec 100644 --- a/COPYING.md +++ b/COPYING.md @@ -1,5 +1,5 @@ McMini is a program that does model checking on a target MultiThreaded Program. -Copyright (C) 2022, Maxwell Pirtle, Luka Jovanovic, Gene Cooperman +Copyright (C) 2022-2024, Maxwell Pirtle, Luka Jovanovic, Gene Cooperman (pirtle.m@northeastern.edu, jovanovic.l@northeastern.edu, gene@ccs.neu.edu) This program is free software: you can redistribute it and/or modify diff --git a/Makefile.in b/Makefile.in index 77bbf1d1..64d97fd5 100644 --- a/Makefile.in +++ b/Makefile.in @@ -35,7 +35,7 @@ test/program/producer_consumer: test/program/producer_consumer.c cd test/program && make producer_consumer check: all test/program/producer_consumer - ./mcmini test/program/producer_consumer --quiet + ./mcmini -f -m 5 test/program/producer_consumer 2 2 0 # If McMini was already built, first do: 'make clean' check-gdb: debug test/program/producer_consumer @@ -46,7 +46,8 @@ check-gdb: debug test/program/producer_consumer echo After 15 seconds, GDB will start, but it may not work properly.;\ sleep 15; \ fi - gdb -x gdbinit --args ./mcmini test/program/producer_consumer --quiet + # gdb -x gdbinit --args -f -m 5 --quiet ./mcmini test/program/producer_consumer + mcmini-gdb -f -m 5 --quiet test/program/producer_consumer mcmini: src/launch.c libmcmini.so ${CC} -g3 -O0 -Iinclude -o $@ $< diff --git a/NEWS b/NEWS new file mode 100644 index 00000000..b3015832 --- /dev/null +++ b/NEWS @@ -0,0 +1,11 @@ +McMini NEWS -- history of user-visible changes. + +McMini is distributed at https://github.com/mcminickpt/mcmini +Please send "Issues" to the github site. +Please note also the extensive documentation of McMini at: + https://mcmini-doc.readthedocs.io/ + +Version 1.0.0 release notes (Oct. 8, 2024) +============================================ +This is the first formal release. Please see the "mcmini-doc" +documentation, above, for details. diff --git a/VERSION b/VERSION new file mode 100644 index 00000000..3eefcb9d --- /dev/null +++ b/VERSION @@ -0,0 +1 @@ +1.0.0 diff --git a/configure b/configure index 003a5ba3..8779eac2 100755 --- a/configure +++ b/configure @@ -1,8 +1,8 @@ #! /bin/sh # Guess values for system-dependent variables and create Makefiles. -# Generated by GNU Autoconf 2.71 for McMini 1.0. +# Generated by GNU Autoconf 2.71 for McMini 1.0.0. # -# Report bugs to . +# Report bugs to . # # # Copyright (C) 1992-1996, 1998-2017, 2020-2021 Free Software Foundation, @@ -267,11 +267,10 @@ then : printf "%s\n" "$0: be upgraded to zsh 4.3.4 or later." else printf "%s\n" "$0: Please tell bug-autoconf@gnu.org and -$0: pirtle.m@northeastern.edu,jovanovic.l@northeastern.edu,gene@ccs.neu.edu -$0: about your system, including any error possibly output -$0: before this message. Then install a modern shell, or -$0: manually run the script under such a shell if you do -$0: have one." +$0: https://github.com/mcminickpt/mcmini/issues about your +$0: system, including any error possibly output before this +$0: message. Then install a modern shell, or manually run +$0: the script under such a shell if you do have one." fi exit 1 fi @@ -611,10 +610,10 @@ MAKEFLAGS= # Identity of this package. PACKAGE_NAME='McMini' PACKAGE_TARNAME='mcmini' -PACKAGE_VERSION='1.0' -PACKAGE_STRING='McMini 1.0' -PACKAGE_BUGREPORT='pirtle.m@northeastern.edu,jovanovic.l@northeastern.edu,gene@ccs.neu.edu' -PACKAGE_URL='https://github.com/mcminickpt/mcmini.git' +PACKAGE_VERSION='1.0.0' +PACKAGE_STRING='McMini 1.0.0' +PACKAGE_BUGREPORT='https://github.com/mcminickpt/mcmini/issues' +PACKAGE_URL='https://github.com/mcminickpt/mcmini ; https://mcmini-doc.readthedocs.io/' ac_unique_file="src/launch.c" # Factoring default headers for most tests. @@ -1279,7 +1278,7 @@ if test "$ac_init_help" = "long"; then # Omit some internal or obsolete options to make the list less imposing. # This message is too long to be a string in the A/UX 3.1 sh. cat <<_ACEOF -\`configure' configures McMini 1.0 to adapt to many kinds of systems. +\`configure' configures McMini 1.0.0 to adapt to many kinds of systems. Usage: $0 [OPTION]... [VAR=VALUE]... @@ -1345,7 +1344,7 @@ fi if test -n "$ac_init_help"; then case $ac_init_help in - short | recursive ) echo "Configuration of McMini 1.0:";; + short | recursive ) echo "Configuration of McMini 1.0.0:";; esac cat <<\_ACEOF @@ -1371,8 +1370,8 @@ Some influential environment variables: Use these variables to override the choices made by `configure' or to help it to find libraries and programs with nonstandard names/locations. -Report bugs to . -McMini home page: . +Report bugs to . +McMini home page: . _ACEOF ac_status=$? fi @@ -1436,7 +1435,7 @@ fi test -n "$ac_init_help" && exit $ac_status if $ac_init_version; then cat <<\_ACEOF -McMini configure 1.0 +McMini configure 1.0.0 generated by GNU Autoconf 2.71 Copyright (C) 2021 Free Software Foundation, Inc. @@ -1888,7 +1887,7 @@ cat >config.log <<_ACEOF This file contains any messages produced by compilers while running configure, to aid debugging if configure makes a mistake. -It was created by McMini $as_me 1.0, which was +It was created by McMini $as_me 1.0.0, which was generated by GNU Autoconf 2.71. Invocation command line was $ $0$ac_configure_args_raw @@ -2865,6 +2864,9 @@ ac_compiler_gnu=$ac_cv_c_compiler_gnu + + + ac_config_headers="$ac_config_headers include/config.h" @@ -5946,7 +5948,7 @@ cat >>$CONFIG_STATUS <<\_ACEOF || ac_write_fail=1 # report actual input values of CONFIG_FILES etc. instead of their # values after options handling. ac_log=" -This file was extended by McMini $as_me 1.0, which was +This file was extended by McMini $as_me 1.0.0, which was generated by GNU Autoconf 2.71. Invocation command line was CONFIG_FILES = $CONFIG_FILES @@ -6002,8 +6004,8 @@ $config_files Configuration headers: $config_headers -Report bugs to . -McMini home page: ." +Report bugs to . +McMini home page: ." _ACEOF ac_cs_config=`printf "%s\n" "$ac_configure_args" | sed "$ac_safe_unquote"` @@ -6011,7 +6013,7 @@ ac_cs_config_escaped=`printf "%s\n" "$ac_cs_config" | sed "s/^ //; s/'/'\\\\\\\\ cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1 ac_cs_config='$ac_cs_config_escaped' ac_cs_version="\\ -McMini config.status 1.0 +McMini config.status 1.0.0 configured by $0, generated by GNU Autoconf 2.71, with options \\"\$ac_cs_config\\" diff --git a/configure.ac b/configure.ac index f4bb4d92..965c0726 100644 --- a/configure.ac +++ b/configure.ac @@ -1,8 +1,11 @@ -# -*- Autoconf -*- -# Process this file with autoconf to produce a configure script. +AC_INIT([McMini], + m4_esyscmd([tr -d '\n' < VERSION]), + [https://github.com/mcminickpt/mcmini/issues], + [mcmini], + [https://github.com/mcminickpt/mcmini ; https://mcmini-doc.readthedocs.io/]) + AC_PREREQ([2.71]) -AC_INIT([McMini],[1.0],[pirtle.m@northeastern.edu,jovanovic.l@northeastern.edu,gene@ccs.neu.edu],[mcmini],[https://github.com/mcminickpt/mcmini.git]) AC_CONFIG_SRCDIR([src/launch.c]) AC_CONFIG_HEADERS([include/config.h]) diff --git a/include/config.h.in b/include/config.h.in index 82ab056b..ed581f30 100644 --- a/include/config.h.in +++ b/include/config.h.in @@ -1,10 +1,83 @@ /* include/config.h.in. Generated from configure.ac by autoheader. */ +/* Use debugging flags "-Wall -g3 -O0" */ +#undef DEBUG + /* Define to 1 if you have process_vm_readv and process_vm_writev. */ #undef HAS_PROCESS_VM -/* define if the compiler supports basic C++14 syntax */ -#undef HAVE_CXX11 +/* Define to 1 if you have the `atexit' function. */ +#undef HAVE_ATEXIT + +/* Define to 1 if you have the header file. */ +#undef HAVE_FCNTL_H + +/* Define to 1 if you have the `fork' function. */ +#undef HAVE_FORK + +/* Define to 1 if you have the `ftruncate' function. */ +#undef HAVE_FTRUNCATE + +/* Define to 1 if you have the `getpagesize' function. */ +#undef HAVE_GETPAGESIZE + +/* Define to 1 if you have the header file. */ +#undef HAVE_INTTYPES_H + +/* Define to 1 if your system has a GNU libc compatible `malloc' function, and + to 0 otherwise. */ +#undef HAVE_MALLOC + +/* Define to 1 if you have a working `mmap' system call. */ +#undef HAVE_MMAP + +/* Define to 1 if you have the `setenv' function. */ +#undef HAVE_SETENV + +/* Define to 1 if you have the header file. */ +#undef HAVE_STDINT_H + +/* Define to 1 if you have the header file. */ +#undef HAVE_STDIO_H + +/* Define to 1 if you have the header file. */ +#undef HAVE_STDLIB_H + +/* Define to 1 if you have the header file. */ +#undef HAVE_STRINGS_H + +/* Define to 1 if you have the header file. */ +#undef HAVE_STRING_H + +/* Define to 1 if you have the `strtoul' function. */ +#undef HAVE_STRTOUL + +/* Define to 1 if you have the header file. */ +#undef HAVE_SYS_PARAM_H + +/* Define to 1 if you have the header file. */ +#undef HAVE_SYS_STAT_H + +/* Define to 1 if you have the header file. */ +#undef HAVE_SYS_TYPES_H + +/* Define to 1 if you have the header file. */ +#undef HAVE_UNISTD_H + +/* Define to 1 if you have the `vfork' function. */ +#undef HAVE_VFORK + +/* Define to 1 if you have the header file. */ +#undef HAVE_VFORK_H + +/* Define to 1 if `fork' works. */ +#undef HAVE_WORKING_FORK + +/* Define to 1 if `vfork' works. */ +#undef HAVE_WORKING_VFORK + +/* Define to 1 if the system has the type `_Bool'. */ +#undef HAVE__BOOL /* Define to the address where bug reports for this package should be sent. */ #undef PACKAGE_BUGREPORT @@ -23,3 +96,53 @@ /* Define to the version of this package. */ #undef PACKAGE_VERSION + +/* Define to 1 if all of the C90 standard headers exist (not just the ones + required in a freestanding environment). This macro is provided for + backward compatibility; new code need not use it. */ +#undef STDC_HEADERS + +/* Define for Solaris 2.5.1 so the uint32_t typedef from , + , or is not used. If the typedef were allowed, the + #define below would cause a syntax error. */ +#undef _UINT32_T + +/* Define for Solaris 2.5.1 so the uint64_t typedef from , + , or is not used. If the typedef were allowed, the + #define below would cause a syntax error. */ +#undef _UINT64_T + +/* Define to rpl_malloc if the replacement function should be used. */ +#undef malloc + +/* Define as a signed integer type capable of holding a process identifier. */ +#undef pid_t + +/* Define to the equivalent of the C99 'restrict' keyword, or to + nothing if this is not supported. Do not define if restrict is + supported only directly. */ +#undef restrict +/* Work around a bug in older versions of Sun C++, which did not + #define __restrict__ or support _Restrict or __restrict__ + even though the corresponding Sun C compiler ended up with + "#define restrict _Restrict" or "#define restrict __restrict__" + in the previous line. This workaround can be removed once + we assume Oracle Developer Studio 12.5 (2016) or later. */ +#if defined __SUNPRO_CC && !defined __RESTRICT && !defined __restrict__ +# define _Restrict +# define __restrict__ +#endif + +/* Define to `unsigned int' if does not define. */ +#undef size_t + +/* Define to the type of an unsigned integer type of width exactly 32 bits if + such a type exists and the standard includes do not define it. */ +#undef uint32_t + +/* Define to the type of an unsigned integer type of width exactly 64 bits if + such a type exists and the standard includes do not define it. */ +#undef uint64_t + +/* Define as `fork' if `vfork' does not work. */ +#undef vfork