- This version seems to compile.
This commit is contained in:
parent
4c3450697a
commit
ef32b1e0e5
@ -1,6 +1,9 @@
|
|||||||
#! /bin/sh
|
#! /bin/sh
|
||||||
|
|
||||||
aclocal \
|
set -x
|
||||||
&& automake --gnu --add-missing \
|
aclocal -I config
|
||||||
&& autoconf
|
libtoolize --force --copy
|
||||||
|
autoheader
|
||||||
|
automake --add-missing --copy --foreign
|
||||||
|
autoconf
|
||||||
|
|
||||||
|
23
configure.in
23
configure.in
@ -1,29 +1,36 @@
|
|||||||
AC_INIT(main.c)
|
AC_INIT(src/main.c)
|
||||||
AM_INIT_AUTOMAKE(Scyther, 0.2, ccremers@win.tue.nl)
|
AM_INIT_AUTOMAKE(Scyther, 0.2, ccremers@win.tue.nl)
|
||||||
AC_CONFIG_SRCDIR([src/modelchecker.c])
|
AC_CONFIG_AUX_DIR(config)
|
||||||
|
AM_CONFIG_HEADER(config.h)
|
||||||
|
AC_CONFIG_SRCDIR(src)
|
||||||
|
|
||||||
|
for top_builddir in . .. ../.. $ac_auxdir $ac_auxdir/..; do
|
||||||
|
test -f $top_builddir/configure && break
|
||||||
|
done
|
||||||
|
AC_PROG_LIBTOOL
|
||||||
|
|
||||||
dnl find and test the C compiler
|
dnl find and test the C compiler
|
||||||
AC_PROG_CC
|
AC_PROG_CC
|
||||||
AC_LANG_C
|
AC_LANG_C
|
||||||
AC_PROG_INSTALL
|
AC_PROG_INSTALL=$ac_aux_dir
|
||||||
|
|
||||||
AC_PROG_MAKE_SET
|
AC_PROG_MAKE_SET
|
||||||
|
|
||||||
# Checks for header files.
|
# Checks for header files.
|
||||||
AC_HEADER_STDC
|
AC_HEADER_STDC
|
||||||
AC_CHECK_HEADERS([limits.h malloc.h stddef.h stdlib.h strings.h unistd.h])
|
AC_CHECK_HEADERS([limits.h malloc.h stddef.h stdlib.h strings.h unistd.h])
|
||||||
|
|
||||||
# Checks for library functions.
|
# Checks for library functions.
|
||||||
AC_FUNC_MALLOC
|
AC_FUNC_MALLOC
|
||||||
AC_FUNC_REALLOC
|
AC_FUNC_REALLOC
|
||||||
|
|
||||||
AC_CHECK_LIB(argtable2, arg_parse,,AC_MSG_ERROR(Scyther requires the argtable2 package (LGPL). Get it from http://argtable.sourceforge.net/))
|
AC_CHECK_LIB(argtable2, arg_parse,,AC_MSG_ERROR(Scyther requires the argtable2 package (LGPL). Get it from http://argtable.sourceforge.net/))
|
||||||
AC_PROG_YACC
|
AC_PROG_YACC
|
||||||
AM_PROG_LEX
|
AC_PROG_LEX
|
||||||
|
#AC_DECL_YYTEXT
|
||||||
|
|
||||||
VERSION="0.0.1"
|
VERSION="0.0.1"
|
||||||
AC_SUBST(VERSION)
|
AC_SUBST(ac_aux_dir)
|
||||||
AC_CONFIG_AUX_DIR(config)
|
SUBDIRS = src
|
||||||
|
|
||||||
dnl read Makefile.in and write Makefile
|
dnl read Makefile.in and write Makefile
|
||||||
AC_OUTPUT(Makefile)
|
AC_OUTPUT(Makefile src/Makefile)
|
||||||
|
87
src/Makefile
87
src/Makefile
@ -1,87 +0,0 @@
|
|||||||
#
|
|
||||||
# Scyther Makefile
|
|
||||||
#
|
|
||||||
|
|
||||||
#
|
|
||||||
# DEBUG or optimization settings: uncomment a single line:
|
|
||||||
#
|
|
||||||
CFLAGS = -g3 -D DEBUG # default usage, for e.g. with valgrind
|
|
||||||
#CFLAGS = -g3 -D DEBUG -pg # for code profiling with gprof
|
|
||||||
#CFLAGS = -O3 -static -finline-functions -fomit-frame-pointer
|
|
||||||
|
|
||||||
#
|
|
||||||
# Compiler and linkage
|
|
||||||
#
|
|
||||||
CC = gcc
|
|
||||||
# Note that these paths must include the path to the argtable library.
|
|
||||||
CPPFLAGS = -I/scratch/ccremers/include -I/usr/local/include -Wall
|
|
||||||
LDFLAGS = -L/scratch/ccremers/lib -L/usr/local/lib
|
|
||||||
LOADLIBS = -lfl
|
|
||||||
LDLIBS = -largtable2
|
|
||||||
OPTIONS = ${CPPFLAGS} ${CFLAGS} ${LDFLAGS}
|
|
||||||
|
|
||||||
#
|
|
||||||
# Module set for the modelchecker
|
|
||||||
#
|
|
||||||
MODULES=memory.o terms.o termlists.o symbols.o knowledge.o runs.o modelchecker.o \
|
|
||||||
report.o debug.o mgu.o substitutions.o \
|
|
||||||
match_basic.o \
|
|
||||||
match_clp.o constraints.o \
|
|
||||||
output.o latex.o \
|
|
||||||
varbuf.o tracebuf.o attackminimize.o \
|
|
||||||
tac.o parser.o compiler.o
|
|
||||||
|
|
||||||
#
|
|
||||||
# Dependencies
|
|
||||||
#
|
|
||||||
MODELCHECKER = ${MODULES} main.o
|
|
||||||
|
|
||||||
all: scyther tags
|
|
||||||
|
|
||||||
${Target}.o: ${Target}.c
|
|
||||||
$(CC) $(OPTIONS) ${Target}.c -c
|
|
||||||
|
|
||||||
scanner.c: scanner.l
|
|
||||||
flex scanner.l
|
|
||||||
cp lex.yy.c scanner.c
|
|
||||||
|
|
||||||
tok.h: parser.c
|
|
||||||
|
|
||||||
parser.c: parser.y
|
|
||||||
bison -d -v parser.y
|
|
||||||
cp parser.tab.c parser.c
|
|
||||||
cmp -s parser.tab.h tok.h || cp parser.tab.h tok.h
|
|
||||||
cmp -s parser.tab.h parser.h || cp parser.tab.h parser.h
|
|
||||||
|
|
||||||
tags: *.c *.h
|
|
||||||
ctags *.c *.h
|
|
||||||
|
|
||||||
modules: $(MODULES)
|
|
||||||
|
|
||||||
scyther: scanner.o $(MODELCHECKER)
|
|
||||||
$(CC) $(OPTIONS) $(MODELCHECKER) -o scyther $(LOADLIBS) $(LDLIBS)
|
|
||||||
|
|
||||||
ptestmain.o scanner.o : tok.h
|
|
||||||
|
|
||||||
#
|
|
||||||
# Cleanup
|
|
||||||
#
|
|
||||||
clean:
|
|
||||||
rm -f *.o
|
|
||||||
rm -f scyther
|
|
||||||
rm -f scanner.c
|
|
||||||
rm -f parser.c
|
|
||||||
rm -f tok.h
|
|
||||||
#
|
|
||||||
# Clean and rebuild: 'make new'
|
|
||||||
#
|
|
||||||
new:
|
|
||||||
make clean
|
|
||||||
make all
|
|
||||||
|
|
||||||
#
|
|
||||||
# Make doxygen reference manuals. (in ../refman)
|
|
||||||
#
|
|
||||||
refman: doxyconfig
|
|
||||||
doxygen doxyconfig
|
|
||||||
|
|
@ -4,14 +4,13 @@ AM_CFLAGS = @CFLAGS@
|
|||||||
|
|
||||||
bin_PROGRAMS = scyther
|
bin_PROGRAMS = scyther
|
||||||
scyther_SOURCES = main.c \
|
scyther_SOURCES = main.c \
|
||||||
|
scanner.l parser.y \
|
||||||
memory.c terms.c termlists.c symbols.c \
|
memory.c terms.c termlists.c symbols.c \
|
||||||
knowledge.c runs.c modelchecker.c \
|
knowledge.c runs.c modelchecker.c \
|
||||||
report.c debug.c mgu.c substitutions.c \
|
report.c debug.c mgu.c substitutions.c \
|
||||||
match_basic.c match_clp.c constraints.c \
|
match_basic.c match_clp.c constraints.c \
|
||||||
output.c latex.c varbuf.c tracebuf.c \
|
output.c latex.c varbuf.c tracebuf.c \
|
||||||
attackminimize.c tac.c \
|
attackminimize.c tac.c \
|
||||||
compiler.c \
|
compiler.c
|
||||||
scanner.l parser.y
|
|
||||||
scyther_LDADD = @LEXLIB@
|
scyther_LDADD = @LEXLIB@
|
||||||
|
|
||||||
|
|
@ -912,7 +912,7 @@ attackDisplayLatex (System sys)
|
|||||||
|
|
||||||
/* put out computed widths */
|
/* put out computed widths */
|
||||||
|
|
||||||
printf ("\\setlength{\\envinstdist}{0.5\\maxmscall}\n");
|
printf ("\\setlength{\\envinstdist}{0.7\\maxmscall}\n");
|
||||||
printf ("\\setlength{\\instdist}{\\maxmscall}\n");
|
printf ("\\setlength{\\instdist}{\\maxmscall}\n");
|
||||||
printf ("\\setlength{\\actionwidth}{\\maxmscaction}\n");
|
printf ("\\setlength{\\actionwidth}{\\maxmscaction}\n");
|
||||||
printf ("\\setlength{\\instwidth}{\\maxmscinst}\n");
|
printf ("\\setlength{\\instwidth}{\\maxmscinst}\n");
|
||||||
|
@ -36,7 +36,7 @@
|
|||||||
#include "symbols.h"
|
#include "symbols.h"
|
||||||
#include "pheading.h"
|
#include "pheading.h"
|
||||||
#include "symbols.h"
|
#include "symbols.h"
|
||||||
#include "parser.h"
|
#include "parser.tab.h"
|
||||||
#include "tac.h"
|
#include "tac.h"
|
||||||
#include "compiler.h"
|
#include "compiler.h"
|
||||||
#include "latex.h"
|
#include "latex.h"
|
||||||
|
@ -1,6 +1,6 @@
|
|||||||
%{
|
%{
|
||||||
#include "pheading.h"
|
#include "pheading.h"
|
||||||
#include "scanner.c"
|
/* #include "lex.yy.c" */
|
||||||
#include "tac.h"
|
#include "tac.h"
|
||||||
|
|
||||||
struct tacnode* spdltac;
|
struct tacnode* spdltac;
|
||||||
|
Loading…
Reference in New Issue
Block a user