andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

- Many cleanups to make -Wall happy. Next up is pedantic...

Browse Source
This commit is contained in:
ccremers 2007-01-06 14:45:29 +00:00
parent 92090142a0
commit 89c3a20acf
31 changed files with 1871 additions and 1927 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
src/arachne.c
View File

@ -42,6 +42,8 @@
#include "arachne.h"
#include "hidelevel.h"
#include "depend.h"
#include "xmlout.h"
#include "heuristic.h"
extern int *graph;
extern int nodes;
@ -70,7 +72,6 @@ static FILE *attack_stream;
*/
int iterate ();
void printSemiState ();
/*
* Program code
@ -81,7 +82,6 @@ void
arachneInit (const System mysys)
{
Roledef rd;
Termlist tl, know0;
void add_event (int event, Term message)
{
@ -666,7 +666,6 @@ create_decryptor (const Term term, const Term key)
if (term != NULL && isTermEncrypt (term))
{
Roledef rd;
Term tempkey;
int run;
#ifdef DEBUG
@ -692,15 +691,13 @@ create_decryptor (const Term term, const Term key)
return run;
}
else
{
globalError++;
eprintf ("Term for which a decryptor instance is requested: ");
termPrint (term);
eprintf ("\n");
error
("Trying to build a decryptor instance for a non-encrypted term.");
}
error ("Trying to build a decryptor instance for a non-encrypted term.");
return -1;
}
//! Get the priority level of a key that is needed for a term (typical pk/sk distinction)
@ -1085,7 +1082,6 @@ printSemiState ()
{
int run;
int open;
List bl;
int binding_state_print (void *dt)
{
@ -2237,7 +2233,7 @@ iterate_buffer_attacks (void)
}
//! Arachne single claim test
int
void
arachneClaimTest (Claimlist cl)
{
// others we simply test...
@ -2377,11 +2373,8 @@ arachneClaim (Claimlist cl)
}
return true;
}
else
{
return false;
}
}
//! Main code for Arachne
@ -2389,6 +2382,8 @@ arachneClaim (Claimlist cl)
* For this test, we manually set up some stuff.
*
* But later, this will just iterate over all claims.
*
* @TODO what does it return? And is that -1 valid, if nothing is tested?
*/
int
arachne ()
@ -2433,7 +2428,7 @@ arachne ()
if (switches.runs == 0)
{
// No real checking.
return;
return -1;
}
if (sys->maxruns > 0)

4
src/arachne.h
View File

@ -12,5 +12,9 @@ int isTriviallyKnownAtArachne (const System sys, const Term t, const int run,
const int index);
int isTriviallyKnownAfterArachne (const System sys, const Term t,
const int run, const int index);
void arachneOutputAttack ();
void printSemiState ();
int countIntruderActions ();
void role_name_print (const int run);
#endif

14
src/binding.c
View File

@ -14,6 +14,7 @@
#include "arachne.h"
#include "switches.h"
#include "depend.h"
#include "error.h"
#ifndef OSXHOST
#include <malloc.h>
#endif
@ -178,6 +179,8 @@ goal_unbind (const Binding b)
//! Bind a goal as a dummy (block)
/**
* Especially made for tuple expansion
*
* @TODO Weird that this returns a value (always true, otherwise error)
*/
int
binding_block (Binding b)
@ -187,13 +190,14 @@ binding_block (Binding b)
b->blocked = true;
return true;
}
else
{
error ("Trying to block a goal again.");
}
return false;
}
//! Unblock a binding
/*
* @TODO Weird that this returns a value (always true, otherwise error)
*/
int
binding_unblock (Binding b)
{
@ -202,10 +206,8 @@ binding_unblock (Binding b)
b->blocked = false;
return true;
}
else
{
error ("Trying to unblock a non-blocked goal.");
}
return false;
}

7
src/claim.c
View File

@ -18,6 +18,8 @@
#include "specialterm.h"
#include "switches.h"
#include "color.h"
#include "cost.h"
#include "timer.h"
//! When none of the runs match
#define MATCH_NONE 0
@ -39,6 +41,10 @@ extern int attack_leastcost;
// Debugging the NI-SYNCH checks
//#define OKIDEBUG
// Forward declaration
int oki_nisynch (const System sys, const int trace_index,
const Termmap role_to_run, const Termmap label_to_index);
/*
* Validity checks for claims
*
@ -367,6 +373,7 @@ oki_nisynch (const System sys, const int trace_index,
* Exception: no claim, no send, no read, what is it?
*/
error ("Unrecognized event type in claim scanner at %i.", trace_index);
return 0;
}
/*

3
src/color.h
View File

@ -6,4 +6,7 @@ extern char *COLOR_Red;
extern char *COLOR_Green;
extern char *COLOR_Bold;
void colorInit (void);
void colorDone (void);
#endif

5
src/compiler.c
View File

@ -16,6 +16,7 @@
#include "hidelevel.h"
#include "debug.h"
#include "intruderknowledge.h"
#include "error.h"
/*
Simple sys pointer as a global. Yields cleaner code although it's against programming standards.
@ -438,7 +439,6 @@ claimCreate (const System sys, const Protocol protocol, const Role role,
const Term claim, Term label, const Term msg)
{
Claimlist cl;
Term labeltuple;
/* generate full unique label */
/* is the label empty or used? */
@ -556,6 +556,7 @@ claimCreate (const System sys, const Protocol protocol, const Role role,
claimvars = claimvars->next;
}
}
return cl;
}
//! Parse a communication event tc of type event, and add a role definition event for it.
@ -1390,7 +1391,6 @@ compute_prec_sets (const System sys)
int size; // temp constant: rolecount * roleeventmax
int rowsize;
int r1, r2, ev1, ev2; // some counters
int i, j;
Claimlist cl;
// Assist: compute index from role, lev
@ -1583,7 +1583,6 @@ compute_prec_sets (const System sys)
cl = sys->claimlist;
while (cl != NULL)
{
Term t;
Roledef rd;
Term label;
int claim_index;

3
src/cost.c
View File

@ -8,6 +8,8 @@
*/
#include "switches.h"
#include "system.h"
#include "binding.h"
#include "error.h"
#include <limits.h>
//************************************************************************
@ -68,4 +70,5 @@ attackCost (const System sys)
return cost;
}
error ("Unknown pruning method (cost function not found)");
return 0;
}

2
src/dotout.c
View File

@ -7,6 +7,7 @@
#include "depend.h"
#include "type.h"
#include "debug.h"
#include "error.h"
extern Protocol INTRUDER; // Pointers, to be set by the Init of arachne.c
extern Role I_M; // Same here.
@ -1645,7 +1646,6 @@ void
dotSemiState (const System mysys)
{
static int attack_number = 0;
int run;
Protocol p;
int *ranks;
int maxrank;

6
src/heuristic.c
View File

@ -7,12 +7,15 @@
*/
#include <float.h>
#include <stdlib.h>
#include "binding.h"
#include "system.h"
#include "specialterm.h"
#include "switches.h"
#include "hidelevel.h"
#include "arachne.h"
#include "error.h"
//! Check whether a binding (goal) is selectable
int
@ -211,8 +214,6 @@ float
weighHidelevel (const System sys, const Term t, const float massknow,
const float massprot)
{
unsigned int hl;
switch (hidelevelFlag (sys, t))
{
case HLFLAG_NONE:
@ -253,6 +254,7 @@ term_constcount (const System sys, Term t)
n++;
}
}
return 1;
}
n = 0;

2
src/intruderknowledge.c
View File

@ -125,7 +125,7 @@ initialIntruderKnowledge (const System sys)
* Hack. Enumerating is not always good (or even desirable).
* If some I knows sk(I), sk should not be in the intruder knowledge.
* But for hash(I), we typically would have h; but if it is never used differently, it would suffice.
* To sommarize, the operational semantics definition is perfectly fine, but maybe a bit strict sometimes.
* To summarize, the operational semantics definition is perfectly fine, but maybe a bit strict sometimes.
*
* The hack is that if function application:
*/

1
src/knowledge.c
View File

@ -10,6 +10,7 @@
#include "knowledge.h"
#include "system.h"
#include "debug.h"
#include "error.h"
/*
* Knowledge stuff

1
src/knowledge.h
View File

@ -56,7 +56,6 @@ Termlist knowledgeNew (const Knowledge oldk, const Knowledge newk);
//! Harnass macro for recursive procedures.
#define mindwipe(k,recurse) \
Termlist tl; \
Term oldsubst; \
int flag; \
if (k != NULL && k->vars != NULL) { \
tl = k->vars; \

4
src/main.c
View File

@ -53,6 +53,8 @@
#include "color.h"
#include "error.h"
#include "claim.h"
#include "arachne.h"
#include "xmlout.h"
//! The global system state pointer
System sys;
@ -75,7 +77,6 @@ int modelCheck (const System sys);
int
main (int argc, char **argv)
{
int nerrors;
int exitcode = EXIT_NOATTACK;
/* initialize symbols */
@ -217,7 +218,6 @@ main (int argc, char **argv)
/* memory clean up? */
strings_cleanup ();
exit:
return exitcode;
}

418
src/parser.c
View File

@ -65,8 +65,7 @@
# define YYTOKENTYPE
/* Put the tokens into the symbol table, so that GDB and other debuggers
know about them. */
enum yytokentype
{
enum yytokentype {
ID = 258,
PROTOCOL = 259,
ROLE = 260,
@ -118,6 +117,7 @@ enum yytokentype
#include "pheading.h"
/* #include "lex.yy.c" */
#include "tac.h"
#include "error.h"
struct tacnode* spdltac;
@ -146,7 +146,7 @@ int yylex (void);
#if ! defined YYSTYPE && ! defined YYSTYPE_IS_DECLARED
typedef union YYSTYPE
#line 13 "parser.y"
#line 14 "parser.y"
{
char* str;
struct tacnode* tac;
@ -154,7 +154,7 @@ typedef union YYSTYPE
int value;
}
/* Line 193 of yacc.c. */
#line 157 "parser.c"
#line 158 "parser.c"
YYSTYPE;
# define yystype YYSTYPE /* obsolescent; will be withdrawn */
# define YYSTYPE_IS_DECLARED 1
@ -167,7 +167,7 @@ YYSTYPE;
/* Line 216 of yacc.c. */
#line 170 "parser.c"
#line 171 "parser.c"
#ifdef short
# undef short
@ -401,7 +401,8 @@ union yyalloc
((unsigned int) (YYX) <= YYMAXUTOK ? yytranslate[YYX] : YYUNDEFTOK)
/* YYTRANSLATE[YYLEX] -- Bison symbol number corresponding to YYLEX. */
static const yytype_uint8 yytranslate[] = {
static const yytype_uint8 yytranslate[] =
{
0, 2, 2, 2, 2, 2, 2, 2, 2, 2,
2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
@ -435,7 +436,8 @@ static const yytype_uint8 yytranslate[] = {
#if YYDEBUG
/* YYPRHS[YYN] -- Index of the first RHS symbol of rule number YYN in
YYRHS. */
static const yytype_uint8 yyprhs[] = {
static const yytype_uint8 yyprhs[] =
{
0, 0, 3, 5, 6, 9, 13, 20, 30, 34,
36, 37, 40, 43, 51, 52, 54, 55, 57, 58,
61, 64, 67, 74, 81, 88, 92, 96, 102, 108,
@ -445,7 +447,8 @@ static const yytype_uint8 yyprhs[] = {
};
/* YYRHS -- A `-1'-separated list of the rules' RHS. */
static const yytype_int8 yyrhs[] = {
static const yytype_int8 yyrhs[] =
{
32, 0, -1, 33, -1, -1, 34, 33, -1, 15,
51, 22, -1, 11, 41, 23, 51, 24, 22, -1,
4, 3, 23, 51, 24, 25, 35, 26, 38, -1,
@ -467,20 +470,22 @@ static const yytype_int8 yyrhs[] = {
};
/* YYRLINE[YYN] -- source line where rule number YYN was defined. */
static const yytype_uint16 yyrline[] = {
0, 69, 69, 74, 75, 79, 85, 92, 100, 106,
113, 114, 116, 120, 132, 133, 138, 139, 144, 145,
147, 149, 153, 160, 167, 176, 184, 191, 198, 205,
211, 217, 225, 228, 236, 240, 248, 252, 258, 263,
264, 269, 277, 279, 285, 289, 295, 297, 301, 303,
307
static const yytype_uint16 yyrline[] =
{
0, 70, 70, 75, 76, 80, 86, 93, 101, 107,
114, 115, 117, 121, 133, 134, 139, 140, 145, 146,
148, 150, 154, 161, 168, 177, 185, 192, 199, 206,
212, 218, 226, 229, 237, 241, 249, 253, 259, 264,
265, 270, 278, 280, 286, 290, 296, 298, 302, 304,
308
};
#endif
#if YYDEBUG || YYERROR_VERBOSE || YYTOKEN_TABLE
/* YYTNAME[SYMBOL-NUM] -- String name of the symbol SYMBOL-NUM.
First, the terminals, then, starting at YYNTOKENS, nonterminals. */
static const char *const yytname[] = {
static const char *const yytname[] =
{
"$end", "error", "$undefined", "ID", "PROTOCOL", "ROLE", "READT",
"SENDT", "CLAIMT", "VAR", "CONST", "RUN", "SECRET", "COMPROMISED",
"INVERSEKEYS", "UNTRUSTED", "USERTYPE", "SINGULAR", "FUNCTION",
@ -496,7 +501,8 @@ static const char *const yytname[] = {
# ifdef YYPRINT
/* YYTOKNUM[YYLEX-NUM] -- Internal token number corresponding to
token YYLEX-NUM. */
static const yytype_uint16 yytoknum[] = {
static const yytype_uint16 yytoknum[] =
{
0, 256, 257, 258, 259, 260, 261, 262, 263, 264,
265, 266, 267, 268, 269, 270, 271, 272, 273, 274,
275, 276, 59, 40, 41, 123, 125, 46, 44, 58,
@ -505,7 +511,8 @@ static const yytype_uint16 yytoknum[] = {
# endif
/* YYR1[YYN] -- Symbol number of symbol that rule YYN derives. */
static const yytype_uint8 yyr1[] = {
static const yytype_uint8 yyr1[] =
{
0, 31, 32, 33, 33, 34, 34, 34, 34, 34,
35, 35, 35, 36, 37, 37, 38, 38, 39, 39,
39, 39, 40, 40, 40, 41, 42, 43, 43, 43,
@ -515,7 +522,8 @@ static const yytype_uint8 yyr1[] = {
};
/* YYR2[YYN] -- Number of symbols composing right hand side of rule YYN. */
static const yytype_uint8 yyr2[] = {
static const yytype_uint8 yyr2[] =
{
0, 2, 1, 0, 2, 3, 6, 9, 3, 1,
0, 2, 2, 7, 0, 1, 0, 1, 0, 2,
2, 2, 6, 6, 6, 3, 3, 5, 5, 4,
@ -527,7 +535,8 @@ static const yytype_uint8 yyr2[] = {
/* YYDEFACT[STATE-NAME] -- Default rule to reduce with in state
STATE-NUM when YYTABLE doesn't specify something else to do. Zero
means the default is an error. */
static const yytype_uint8 yydefact[] = {
static const yytype_uint8 yydefact[] =
{
32, 0, 0, 33, 0, 0, 0, 0, 0, 2,
32, 9, 0, 0, 0, 0, 41, 48, 34, 41,
0, 0, 42, 46, 0, 0, 0, 0, 1, 4,
@ -544,7 +553,8 @@ static const yytype_uint8 yydefact[] = {
};
/* YYDEFGOTO[NTERM-NUM]. */
static const yytype_int8 yydefgoto[] = {
static const yytype_int8 yydefgoto[] =
{
-1, 8, 9, 10, 75, 76, 77, 85, 92, 93,
15, 94, 95, 12, 37, 60, 97, 100, 22, 23,
24, 18, 66
@ -553,7 +563,8 @@ static const yytype_int8 yydefgoto[] = {
/* YYPACT[STATE-NUM] -- Index in YYTABLE of the portion describing
STATE-NUM. */
#define YYPACT_NINF -85
static const yytype_int8 yypact[] = {
static const yytype_int8 yypact[] =
{
75, 1, 10, 17, 0, -1, 0, 0, 24, -85,
75, -85, 9, 4, 15, 8, -85, 16, 7, 14,
0, 0, -85, 18, 21, 0, 28, 29, -85, -85,
@ -570,7 +581,8 @@ static const yytype_int8 yypact[] = {
};
/* YYPGOTO[NTERM-NUM]. */
static const yytype_int8 yypgoto[] = {
static const yytype_int8 yypgoto[] =
{
-85, -85, 97, -85, -71, -85, -85, 11, -84, -85,
-85, -85, 2, -85, 67, -85, -60, -85, 3, -17,
-6, -14, -85
@ -581,7 +593,8 @@ static const yytype_int8 yypgoto[] = {
number is the opposite. If zero, do what YYDEFACT says.
If YYTABLE_NINF, syntax error. */
#define YYTABLE_NINF -19
static const yytype_int8 yytable[] = {
static const yytype_int8 yytable[] =
{
26, 27, 11, 19, 13, 81, 17, 83, 43, 103,
104, 105, 11, 14, 39, 40, 46, 47, 30, 31,
16, 51, 25, 20, 28, 21, 48, 32, 50, 98,
@ -596,7 +609,8 @@ static const yytype_int8 yytable[] = {
118, 119, 120, 111, 61
};
static const yytype_uint8 yycheck[] = {
static const yytype_uint8 yycheck[] =
{
6, 7, 0, 3, 3, 76, 3, 78, 25, 93,
94, 95, 10, 3, 20, 21, 30, 31, 9, 10,
3, 35, 23, 23, 0, 25, 32, 23, 34, 89,
@ -613,7 +627,8 @@ static const yytype_uint8 yycheck[] = {
/* YYSTOS[STATE-NUM] -- The (internal number of the) accessing
symbol of state STATE-NUM. */
static const yytype_uint8 yystos[] = {
static const yytype_uint8 yystos[] =
{
0, 4, 11, 12, 13, 14, 15, 16, 32, 33,
34, 43, 44, 3, 3, 41, 3, 49, 52, 3,
23, 25, 49, 50, 51, 23, 51, 51, 0, 33,
@ -753,8 +768,7 @@ do { \
#if (defined __STDC__ || defined __C99__FUNC__ \
|| defined __cplusplus || defined _MSC_VER)
static void
yy_symbol_value_print (FILE * yyoutput, int yytype,
YYSTYPE const *const yyvaluep)
yy_symbol_value_print (FILE *yyoutput, int yytype, YYSTYPE const * const yyvaluep)
#else
static void
yy_symbol_value_print (yyoutput, yytype, yyvaluep)
@ -858,7 +872,8 @@ yy_reduce_print (yyvsp, yyrule)
{
fprintf (stderr, " $%d = ", yyi + 1);
yy_symbol_print (stderr, yyrhs[yyprhs[yyrule] + yyi],
&(yyvsp[(yyi + 1) - (yynrhs)]));
&(yyvsp[(yyi + 1) - (yynrhs)])
);
fprintf (stderr, "\n");
}
}
@ -895,8 +910,8 @@ int yydebug;
#ifndef YYMAXDEPTH
# define YYMAXDEPTH 10000
#endif
#if YYERROR_VERBOSE
@ -1020,8 +1035,7 @@ yysyntax_error (char *yyresult, int yystate, int yychar)
YYSIZE_T yysize = yysize0;
YYSIZE_T yysize1;
int yysize_overflow = 0;
enum
{ YYERROR_VERBOSE_ARGS_MAXIMUM = 5 };
enum { YYERROR_VERBOSE_ARGS_MAXIMUM = 5 };
char const *yyarg[YYERROR_VERBOSE_ARGS_MAXIMUM];
int yyx;
@ -1193,6 +1207,7 @@ yyparse (void)
#else
int
yyparse ()
#endif
#endif
{
@ -1292,7 +1307,9 @@ yysetstate:
be undefined if yyoverflow is a macro. */
yyoverflow (YY_("memory exhausted"),
&yyss1, yysize * sizeof (*yyssp),
&yyvs1, yysize * sizeof (*yyvsp), &yystacksize);
&yyvs1, yysize * sizeof (*yyvsp),
&yystacksize);
yyss = yyss1;
yyvs = yyvs1;
@ -1439,103 +1456,83 @@ yyreduce:
switch (yyn)
{
case 2:
#line 70 "parser.y"
{
spdltac = (yyvsp[(1) - (1)].tac);;
}
#line 71 "parser.y"
{ spdltac = (yyvsp[(1) - (1)].tac); ;}
break;
case 3:
#line 74 "parser.y"
{
(yyval.tac) = NULL;;
}
#line 75 "parser.y"
{ (yyval.tac) = NULL; ;}
break;
case 4:
#line 76 "parser.y"
{
(yyval.tac) =
tacCat ((yyvsp[(1) - (2)].tac), (yyvsp[(2) - (2)].tac));;
}
#line 77 "parser.y"
{ (yyval.tac) = tacCat((yyvsp[(1) - (2)].tac),(yyvsp[(2) - (2)].tac)); ;}
break;
case 5:
#line 80 "parser.y"
#line 81 "parser.y"
{
Tac t = tacCreate(TAC_UNTRUSTED);
t->t1.tac = (yyvsp[(2) - (3)].tac);
(yyval.tac) = t;
;
}
;}
break;
case 6:
#line 86 "parser.y"
#line 87 "parser.y"
{
Tac t = tacCreate(TAC_RUN);
t->t1.tac = (yyvsp[(2) - (6)].tac);
t->t2.tac = (yyvsp[(4) - (6)].tac);
(yyval.tac) = t;
;
}
;}
break;
case 7:
#line 93 "parser.y"
#line 94 "parser.y"
{
Tac t = tacCreate(TAC_PROTOCOL);
t->t1.sym = (yyvsp[(2) - (9)].symb);
t->t2.tac = (yyvsp[(7) - (9)].tac);
t->t3.tac = (yyvsp[(4) - (9)].tac);
(yyval.tac) = t;
;
}
;}
break;
case 8:
#line 101 "parser.y"
#line 102 "parser.y"
{
Tac t = tacCreate(TAC_USERTYPE);
t->t1.tac = (yyvsp[(2) - (3)].tac);
(yyval.tac) = t;
;
}
;}
break;
case 9:
#line 107 "parser.y"
#line 108 "parser.y"
{
(yyval.tac) = (yyvsp[(1) - (1)].tac);
;
}
;}
break;
case 10:
#line 113 "parser.y"
{
(yyval.tac) = NULL;;
}
#line 114 "parser.y"
{ (yyval.tac) = NULL; ;}
break;
case 11:
#line 115 "parser.y"
{
(yyval.tac) =
tacCat ((yyvsp[(1) - (2)].tac), (yyvsp[(2) - (2)].tac));;
}
#line 116 "parser.y"
{ (yyval.tac) = tacCat((yyvsp[(1) - (2)].tac),(yyvsp[(2) - (2)].tac)); ;}
break;
case 12:
#line 117 "parser.y"
{
(yyval.tac) =
tacCat ((yyvsp[(1) - (2)].tac), (yyvsp[(2) - (2)].tac));;
}
#line 118 "parser.y"
{ (yyval.tac) = tacCat((yyvsp[(1) - (2)].tac),(yyvsp[(2) - (2)].tac)); ;}
break;
case 13:
#line 121 "parser.y"
#line 122 "parser.y"
{
// TODO process singular (0/1)
Tac t = tacCreate(TAC_ROLE);
@ -1543,336 +1540,268 @@ yyreduce:
t->t2.tac = (yyvsp[(5) - (7)].tac);
t->t3.value = (yyvsp[(1) - (7)].value);
(yyval.tac) = t;
;
}
;}
break;
case 14:
#line 132 "parser.y"
{
(yyval.value) = 0;;
}
#line 133 "parser.y"
{ (yyval.value) = 0; ;}
break;
case 15:
#line 134 "parser.y"
{
(yyval.value) = 1;;
}
#line 135 "parser.y"
{ (yyval.value) = 1; ;}
break;
case 16:
#line 138 "parser.y"
{;
}
#line 139 "parser.y"
{ ;}
break;
case 17:
#line 140 "parser.y"
{;
}
#line 141 "parser.y"
{ ;}
break;
case 18:
#line 144 "parser.y"
{
(yyval.tac) = NULL;;
}
#line 145 "parser.y"
{ (yyval.tac) = NULL; ;}
break;
case 19:
#line 146 "parser.y"
{
(yyval.tac) =
tacCat ((yyvsp[(1) - (2)].tac), (yyvsp[(2) - (2)].tac));;
}
#line 147 "parser.y"
{ (yyval.tac) = tacCat((yyvsp[(1) - (2)].tac),(yyvsp[(2) - (2)].tac)); ;}
break;
case 20:
#line 148 "parser.y"
{
(yyval.tac) =
tacCat ((yyvsp[(1) - (2)].tac), (yyvsp[(2) - (2)].tac));;
}
#line 149 "parser.y"
{ (yyval.tac) = tacCat((yyvsp[(1) - (2)].tac),(yyvsp[(2) - (2)].tac)); ;}
break;
case 21:
#line 150 "parser.y"
{
(yyval.tac) =
tacCat ((yyvsp[(1) - (2)].tac), (yyvsp[(2) - (2)].tac));;
}
#line 151 "parser.y"
{ (yyval.tac) = tacCat((yyvsp[(1) - (2)].tac),(yyvsp[(2) - (2)].tac)); ;}
break;
case 22:
#line 154 "parser.y"
{
Tac t = tacCreate (TAC_READ);
#line 155 "parser.y"
{ Tac t = tacCreate(TAC_READ);
t->t1.sym = (yyvsp[(2) - (6)].symb);
/* TODO test here: tac2 should have at least 3 elements */
t->t2.tac = (yyvsp[(4) - (6)].tac);
(yyval.tac) = t;
;
}
;}
break;
case 23:
#line 161 "parser.y"
{
Tac t = tacCreate (TAC_SEND);
#line 162 "parser.y"
{ Tac t = tacCreate(TAC_SEND);
t->t1.sym = (yyvsp[(2) - (6)].symb);
/* TODO test here: tac2 should have at least 3 elements */
t->t2.tac = (yyvsp[(4) - (6)].tac);
(yyval.tac) = t;
;
}
;}
break;
case 24:
#line 169 "parser.y"
{
Tac t = tacCreate (TAC_CLAIM);
#line 170 "parser.y"
{ Tac t = tacCreate(TAC_CLAIM);
t->t1.sym = (yyvsp[(2) - (6)].symb);
t->t2.tac = (yyvsp[(4) - (6)].tac);
(yyval.tac) = t;
;
}
;}
break;
case 25:
#line 177 "parser.y"
{
Tac t = tacCreate (TAC_ROLEREF);
#line 178 "parser.y"
{ Tac t = tacCreate(TAC_ROLEREF);
t->t1.sym = (yyvsp[(1) - (3)].symb);
t->t2.sym = (yyvsp[(3) - (3)].symb);
(yyval.tac) = t;
;
}
;}
break;
case 26:
#line 185 "parser.y"
{
Tac t = tacCreate (TAC_KNOWS);
#line 186 "parser.y"
{ Tac t = tacCreate(TAC_KNOWS);
t->t1.tac = (yyvsp[(2) - (3)].tac);
(yyval.tac) = t;
;
}
;}
break;
case 27:
#line 192 "parser.y"
{
Tac t = tacCreate (TAC_CONST);
#line 193 "parser.y"
{ Tac t = tacCreate(TAC_CONST);
t->t1.tac = (yyvsp[(3) - (5)].tac);
t->t2.tac = (yyvsp[(4) - (5)].tac);
t->t3.tac = (yyvsp[(1) - (5)].tac);
(yyval.tac) = t;
;
}
;}
break;
case 28:
#line 199 "parser.y"
{
Tac t = tacCreate (TAC_VAR);
#line 200 "parser.y"
{ Tac t = tacCreate(TAC_VAR);
t->t1.tac = (yyvsp[(3) - (5)].tac);
t->t2.tac = (yyvsp[(4) - (5)].tac);
t->t3.tac = (yyvsp[(1) - (5)].tac);
(yyval.tac) = t;
;
}
;}
break;
case 29:
#line 206 "parser.y"
{
Tac t = tacCreate (TAC_SECRET);
#line 207 "parser.y"
{ Tac t = tacCreate(TAC_SECRET);
t->t1.tac = (yyvsp[(2) - (4)].tac);
t->t2.tac = (yyvsp[(3) - (4)].tac);
(yyval.tac) = t;
;
}
;}
break;
case 30:
#line 212 "parser.y"
{
Tac t = tacCreate (TAC_INVERSEKEYS);
#line 213 "parser.y"
{ Tac t = tacCreate(TAC_INVERSEKEYS);
t->t1.tac = (yyvsp[(3) - (7)].tac);
t->t2.tac = (yyvsp[(5) - (7)].tac);
(yyval.tac) = t;
;
}
;}
break;
case 31:
#line 218 "parser.y"
{
Tac t = tacCreate (TAC_COMPROMISED);
#line 219 "parser.y"
{ Tac t = tacCreate(TAC_COMPROMISED);
t->t1.tac= (yyvsp[(2) - (3)].tac);
(yyval.tac) = t;
;
}
;}
break;
case 32:
#line 225 "parser.y"
#line 226 "parser.y"
{
(yyval.tac) = NULL;
;
}
;}
break;
case 33:
#line 229 "parser.y"
#line 230 "parser.y"
{
Tac t = tacCreate(TAC_SECRET);
(yyval.tac) = t;
;
}
;}
break;
case 34:
#line 236 "parser.y"
#line 237 "parser.y"
{
Tac t = tacCreate(TAC_UNDEF);
(yyval.tac) = t;
;
}
;}
break;
case 35:
#line 241 "parser.y"
{
Tac t = tacCreate (TAC_STRING);
#line 242 "parser.y"
{ Tac t = tacCreate(TAC_STRING);
t->t1.sym = (yyvsp[(2) - (2)].symb);
(yyval.tac) = t;
;
}
;}
break;
case 36:
#line 248 "parser.y"
#line 249 "parser.y"
{
Tac t = tacCreate(TAC_UNDEF);
(yyval.tac) = t;
;
}
;}
break;
case 37:
#line 253 "parser.y"
#line 254 "parser.y"
{
(yyval.tac) = (yyvsp[(2) - (2)].tac);
;
}
;}
break;
case 38:
#line 259 "parser.y"
{
(yyval.symb) = (yyvsp[(2) - (2)].symb);;
}
#line 260 "parser.y"
{ (yyval.symb) = (yyvsp[(2) - (2)].symb); ;}
break;
case 39:
#line 263 "parser.y"
{
(yyval.symb) = NULL;;
}
#line 264 "parser.y"
{ (yyval.symb) = NULL; ;}
break;
case 40:
#line 265 "parser.y"
{;
}
#line 266 "parser.y"
{ ;}
break;
case 41:
#line 270 "parser.y"
#line 271 "parser.y"
{
Tac t = tacCreate(TAC_STRING);
t->t1.sym = (yyvsp[(1) - (1)].symb);
(yyval.tac) = t;
;
}
;}
break;
case 42:
#line 278 "parser.y"
{;
}
#line 279 "parser.y"
{ ;}
break;
case 43:
#line 280 "parser.y"
#line 281 "parser.y"
{
Tac t = tacCreate(TAC_STRING);
t->t1.sym = (yyvsp[(1) - (4)].symb);
(yyval.tac) =
tacJoin (TAC_ENCRYPT, tacTuple ((yyvsp[(3) - (4)].tac)), t, NULL);
;
}
(yyval.tac) = tacJoin(TAC_ENCRYPT,tacTuple((yyvsp[(3) - (4)].tac)),t,NULL);
;}
break;
case 44:
#line 286 "parser.y"
#line 287 "parser.y"
{
(yyval.tac) =
tacJoin (TAC_ENCRYPT, tacTuple ((yyvsp[(2) - (4)].tac)),
(yyvsp[(4) - (4)].tac), NULL);
;
}
(yyval.tac) = tacJoin(TAC_ENCRYPT,tacTuple((yyvsp[(2) - (4)].tac)),(yyvsp[(4) - (4)].tac),NULL);
;}
break;
case 45:
#line 290 "parser.y"
#line 291 "parser.y"
{
(yyval.tac) = tacTuple((yyvsp[(2) - (3)].tac));
;
}
;}
break;
case 46:
#line 296 "parser.y"
{;
}
#line 297 "parser.y"
{ ;}
break;
case 47:
#line 298 "parser.y"
{
(yyval.tac) =
tacCat ((yyvsp[(1) - (3)].tac), (yyvsp[(3) - (3)].tac));;
}
#line 299 "parser.y"
{ (yyval.tac) = tacCat((yyvsp[(1) - (3)].tac),(yyvsp[(3) - (3)].tac)); ;}
break;
case 48:
#line 302 "parser.y"
{;
}
#line 303 "parser.y"
{ ;}
break;
case 49:
#line 304 "parser.y"
{
(yyval.tac) =
tacCat ((yyvsp[(1) - (3)].tac), (yyvsp[(3) - (3)].tac));;
}
#line 305 "parser.y"
{ (yyval.tac) = tacCat((yyvsp[(1) - (3)].tac),(yyvsp[(3) - (3)].tac)); ;}
break;
case 50:
#line 308 "parser.y"
{;
}
#line 309 "parser.y"
{ ;}
break;
/* Line 1267 of yacc.c. */
#line 1803 "parser.c"
default:
break;
#line 1804 "parser.c"
default: break;
}
YY_SYMBOL_PRINT ("-> $$ =", yyr1[yyn], &yyval, &yyloc);
@ -1958,7 +1887,8 @@ yyerrlab:
}
else
{
yydestruct ("Error: discarding", yytoken, &yylval);
yydestruct ("Error: discarding",
yytoken, &yylval);
yychar = YYEMPTY;
}
}
@ -2013,7 +1943,8 @@ yyerrlab1:
YYABORT;
yydestruct ("Error: popping", yystos[yystate], yyvsp);
yydestruct ("Error: popping",
yystos[yystate], yyvsp);
YYPOPSTACK (1);
yystate = *yyssp;
YY_STACK_PRINT (yyss, yyssp);
@ -2058,14 +1989,16 @@ yyexhaustedlab:
yyreturn:
if (yychar != YYEOF && yychar != YYEMPTY)
yydestruct ("Cleanup: discarding lookahead", yytoken, &yylval);
yydestruct ("Cleanup: discarding lookahead",
yytoken, &yylval);
/* Do not reclaim the symbols of the rule which action triggered
this YYABORT or YYACCEPT. */
YYPOPSTACK (yylen);
YY_STACK_PRINT (yyss, yyssp);
while (yyssp != yyss)
{
yydestruct ("Cleanup: popping", yystos[*yyssp], yyvsp);
yydestruct ("Cleanup: popping",
yystos[*yyssp], yyvsp);
YYPOPSTACK (1);
}
#ifndef yyoverflow
@ -2081,15 +2014,18 @@ yyreturn:
}
#line 313 "parser.y"
#line 314 "parser.y"
//! error handler routing
int
yyerror (char *s)
int yyerror(char *s)
{
extern int yylineno; //!< defined and maintained in lex.c
extern char *yytext; //!< defined and maintained in lex.c
error ("%s at symbol '%s' on line %i.\n", s, yytext, yylineno);
return 0;
}

6
src/parser.h
View File

@ -38,8 +38,7 @@
# define YYTOKENTYPE
/* Put the tokens into the symbol table, so that GDB and other debuggers
know about them. */
enum yytokentype
{
enum yytokentype {
ID = 258,
PROTOCOL = 259,
ROLE = 260,
@ -87,7 +86,7 @@ enum yytokentype
#if ! defined YYSTYPE && ! defined YYSTYPE_IS_DECLARED
typedef union YYSTYPE
#line 13 "parser.y"
#line 14 "parser.y"
{
char* str;
struct tacnode* tac;
@ -103,3 +102,4 @@ YYSTYPE;
#endif
extern YYSTYPE yylval;

2
src/parser.y
View File

@ -2,6 +2,7 @@
#include "pheading.h"
/* #include "lex.yy.c" */
#include "tac.h"
#include "error.h"
struct tacnode* spdltac;
@ -319,6 +320,7 @@ int yyerror(char *s)
extern char *yytext; //!< defined and maintained in lex.c
error ("%s at symbol '%s' on line %i.\n", s, yytext, yylineno);
return 0;
}

7
src/prune_bounds.c
View File

@ -11,6 +11,10 @@
#include "termlist.h"
#include "list.h"
#include "switches.h"
#include "timer.h"
#include "arachne.h"
#include "system.h"
#include "cost.h"
extern int attack_length;
extern int attack_leastcost;
@ -27,9 +31,6 @@ extern int max_encryption_level;
int
prune_bounds (const System sys)
{
Termlist tl;
List bl;
/* prune for time */
if (passed_time_limit ())
{

8
src/prune_theorems.c
View File

@ -13,6 +13,10 @@
#include "binding.h"
#include "specialterm.h"
#include "hidelevel.h"
#include "depend.h"
#include "arachne.h"
#include "error.h"
#include "type.h"
extern Protocol INTRUDER;
extern int proofDepth;
@ -106,9 +110,8 @@ correctLocalOrder (const System sys)
globalError--;
error ("Abort");
}
return true;
}
return true;
}
return iterateLocalToOther (sys, r1, checkTerm);
@ -162,7 +165,6 @@ initiatorAgentsType (const System sys)
int
prune_theorems (const System sys)
{
Termlist tl;
List bl;
int run;

1
src/role.c
View File

@ -11,6 +11,7 @@
#include "knowledge.h"
#include "system.h"
#include "debug.h"
#include "error.h"
#include "role.h"
extern int protocolCount; // from system.c

452
src/scanner.c
View File

@ -385,7 +385,8 @@ struct yy_trans_info
flex_int32_t yy_verify;
flex_int32_t yy_nxt;
};
static yyconst flex_int16_t yy_accept[148] = { 0,
static yyconst flex_int16_t yy_accept[148] =
{ 0,
0, 0, 0, 0, 0, 0, 31, 29, 7, 6,
28, 9, 29, 29, 28, 28, 28, 28, 28, 28,
28, 28, 28, 28, 28, 3, 3, 2, 30, 4,
@ -404,7 +405,8 @@ static yyconst flex_int16_t yy_accept[148] = { 0,
28, 28, 21, 28, 19, 25, 0
} ;
static yyconst flex_int32_t yy_ec[256] = { 0,
static yyconst flex_int32_t yy_ec[256] =
{ 0,
1, 1, 1, 1, 1, 1, 1, 1, 2, 3,
1, 1, 4, 1, 1, 1, 1, 1, 1, 1,
1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
@ -435,14 +437,16 @@ static yyconst flex_int32_t yy_ec[256] = { 0,
1, 1, 1, 1, 1
} ;
static yyconst flex_int32_t yy_meta[36] = { 0,
static yyconst flex_int32_t yy_meta[36] =
{ 0,
1, 1, 2, 1, 3, 4, 1, 1, 1, 3,
1, 1, 3, 3, 3, 3, 3, 3, 3, 3,
3, 3, 3, 3, 3, 3, 3, 3, 3, 3,
3, 3, 3, 3, 3
} ;
static yyconst flex_int16_t yy_base[154] = { 0,
static yyconst flex_int16_t yy_base[154] =
{ 0,
0, 0, 34, 35, 176, 175, 180, 183, 40, 43,
0, 0, 30, 0, 24, 147, 164, 151, 150, 146,
31, 32, 145, 26, 159, 0, 51, 183, 183, 161,
@ -462,7 +466,8 @@ static yyconst flex_int16_t yy_base[154] = { 0,
84, 88, 91
} ;
static yyconst flex_int16_t yy_def[154] = { 0,
static yyconst flex_int16_t yy_def[154] =
{ 0,
147, 1, 148, 148, 149, 149, 147, 147, 147, 147,
150, 151, 147, 150, 150, 150, 150, 150, 150, 150,
150, 150, 150, 150, 150, 152, 152, 147, 147, 147,
@ -482,7 +487,8 @@ static yyconst flex_int16_t yy_def[154] = { 0,
147, 147, 147
} ;
static yyconst flex_int16_t yy_nxt[219] = { 0,
static yyconst flex_int16_t yy_nxt[219] =
{ 0,
8, 9, 10, 9, 11, 8, 12, 8, 13, 11,
8, 14, 11, 11, 11, 15, 11, 11, 16, 11,
17, 18, 19, 11, 11, 11, 11, 20, 21, 22,
@ -509,7 +515,8 @@ static yyconst flex_int16_t yy_nxt[219] = { 0,
147, 147, 147, 147, 147, 147, 147, 147
} ;
static yyconst flex_int16_t yy_chk[219] = { 0,
static yyconst flex_int16_t yy_chk[219] =
{ 0,
1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
@ -537,10 +544,10 @@ static yyconst flex_int16_t yy_chk[219] = { 0,
} ;
/* Table of booleans, true if rule could match eol. */
static yyconst flex_int32_t yy_rule_can_match_eol[31] = { 0,
static yyconst flex_int32_t yy_rule_can_match_eol[31] =
{ 0,
0, 0, 1, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
};
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, };
static yy_state_type yy_last_accepting_state;
static char *yy_last_accepting_cpos;
@ -577,8 +584,7 @@ int yyerror (char *s);
Symbol mkstring(char *name);
struct stringlist
{
struct stringlist {
char* string;
struct stringlist* next;
};
@ -773,10 +779,10 @@ YY_DECL
if ( ! yyout )
yyout = stdout;
if (!YY_CURRENT_BUFFER)
{
if ( ! YY_CURRENT_BUFFER ) {
yyensure_buffer_stack ();
YY_CURRENT_BUFFER_LVALUE = yy_create_buffer (yyin, YY_BUF_SIZE);
YY_CURRENT_BUFFER_LVALUE =
yy_create_buffer(yyin,YY_BUF_SIZE );
}
yy_load_buffer_state( );
@ -810,8 +816,7 @@ YY_DECL
if ( yy_current_state >= 148 )
yy_c = yy_meta[(unsigned int) yy_c];
}
yy_current_state =
yy_nxt[yy_base[yy_current_state] + (unsigned int) yy_c];
yy_current_state = yy_nxt[yy_base[yy_current_state] + (unsigned int) yy_c];
++yy_cp;
}
while ( yy_base[yy_current_state] != 183 );
@ -852,10 +857,13 @@ YY_DECL
YY_RULE_SETUP
#line 62 "scanner.l"
BEGIN(incl);
YY_BREAK case 2:YY_RULE_SETUP
YY_BREAK
case 2:
YY_RULE_SETUP
#line 63 "scanner.l"
/* eat the whitespace */
YY_BREAK case 3:
YY_BREAK
case 3:
/* rule 3 can match eol */
YY_RULE_SETUP
#line 64 "scanner.l"
@ -866,7 +874,8 @@ YY_DECL
exit( 1 );
}
include_stack[include_stack_ptr++] = YY_CURRENT_BUFFER;
include_stack[include_stack_ptr++] =
YY_CURRENT_BUFFER;
/* try to open, using scytherdirs environment variable as well. */
yyin = openFileSearch (yytext, NULL);
@ -880,12 +889,15 @@ YY_DECL
BEGIN(INITIAL);
}
YY_BREAK case 4:YY_RULE_SETUP
YY_BREAK
case 4:
YY_RULE_SETUP
#line 88 "scanner.l"
{ /* eat the closing things */
BEGIN(INITIAL);
}
YY_BREAK case YY_STATE_EOF (INITIAL):
YY_BREAK
case YY_STATE_EOF(INITIAL):
#line 92 "scanner.l"
{
if ( --include_stack_ptr < 0 )
@ -900,7 +912,9 @@ YY_DECL
BEGIN(inclend);
}
}
YY_BREAK case 5:YY_RULE_SETUP
YY_BREAK
case 5:
YY_RULE_SETUP
#line 107 "scanner.l"
{
register int c;
@ -928,129 +942,134 @@ YY_DECL
}
}
}
YY_BREAK case 6:
YY_BREAK
case 6:
/* rule 6 can match eol */
YY_RULE_SETUP
#line 134 "scanner.l"
{
mylineno++;
}
YY_BREAK case 7:
{ mylineno++; }
YY_BREAK
case 7:
/* rule 7 can match eol */
YY_RULE_SETUP
#line 135 "scanner.l"
{
}
YY_BREAK case 8:YY_RULE_SETUP
{ }
YY_BREAK
case 8:
YY_RULE_SETUP
#line 136 "scanner.l"
{
}
YY_BREAK case 9:YY_RULE_SETUP
{ }
YY_BREAK
case 9:
YY_RULE_SETUP
#line 137 "scanner.l"
{
}
YY_BREAK case 10:YY_RULE_SETUP
{ }
YY_BREAK
case 10:
YY_RULE_SETUP
#line 139 "scanner.l"
{
return PROTOCOL;
}
YY_BREAK case 11:YY_RULE_SETUP
{ return PROTOCOL; }
YY_BREAK
case 11:
YY_RULE_SETUP
#line 140 "scanner.l"
{
return ROLE;
}
YY_BREAK case 12:YY_RULE_SETUP
{ return ROLE; }
YY_BREAK
case 12:
YY_RULE_SETUP
#line 141 "scanner.l"
{
return READT;
}
YY_BREAK case 13:YY_RULE_SETUP
{ return READT; }
YY_BREAK
case 13:
YY_RULE_SETUP
#line 142 "scanner.l"
{
return SENDT;
}
YY_BREAK case 14:YY_RULE_SETUP
{ return SENDT; }
YY_BREAK
case 14:
YY_RULE_SETUP
#line 143 "scanner.l"
{
return VAR;
}
YY_BREAK case 15:YY_RULE_SETUP
{ return VAR; }
YY_BREAK
case 15:
YY_RULE_SETUP
#line 144 "scanner.l"
{
return CONST;
}
YY_BREAK case 16:YY_RULE_SETUP
{ return CONST; }
YY_BREAK
case 16:
YY_RULE_SETUP
#line 145 "scanner.l"
{
return CLAIMT;
}
YY_BREAK case 17:YY_RULE_SETUP
{ return CLAIMT; }
YY_BREAK
case 17:
YY_RULE_SETUP
#line 146 "scanner.l"
{
return RUN;
}
YY_BREAK case 18:YY_RULE_SETUP
{ return RUN; }
YY_BREAK
case 18:
YY_RULE_SETUP
#line 147 "scanner.l"
{
return SECRET;
}
YY_BREAK case 19:YY_RULE_SETUP
{ return SECRET; }
YY_BREAK
case 19:
YY_RULE_SETUP
#line 148 "scanner.l"
{
return INVERSEKEYS;
}
YY_BREAK case 20:YY_RULE_SETUP
{ return INVERSEKEYS; }
YY_BREAK
case 20:
YY_RULE_SETUP
#line 149 "scanner.l"
{
return UNTRUSTED;
}
YY_BREAK case 21:YY_RULE_SETUP
{ return UNTRUSTED; }
YY_BREAK
case 21:
YY_RULE_SETUP
#line 150 "scanner.l"
{
return COMPROMISED;
}
YY_BREAK case 22:YY_RULE_SETUP
{ return COMPROMISED; }
YY_BREAK
case 22:
YY_RULE_SETUP
#line 151 "scanner.l"
{
return USERTYPE;
}
YY_BREAK case 23:YY_RULE_SETUP
{ return USERTYPE; }
YY_BREAK
case 23:
YY_RULE_SETUP
#line 152 "scanner.l"
{
return SINGULAR;
}
YY_BREAK case 24:YY_RULE_SETUP
{ return SINGULAR; }
YY_BREAK
case 24:
YY_RULE_SETUP
#line 153 "scanner.l"
{
return FUNCTION;
}
YY_BREAK case 25:YY_RULE_SETUP
{ return FUNCTION; }
YY_BREAK
case 25:
YY_RULE_SETUP
#line 154 "scanner.l"
{
return HASHFUNCTION;
}
YY_BREAK case 26:YY_RULE_SETUP
{ return HASHFUNCTION; }
YY_BREAK
case 26:
YY_RULE_SETUP
#line 155 "scanner.l"
{
return KNOWS;
}
YY_BREAK case 27:YY_RULE_SETUP
{ return KNOWS; }
YY_BREAK
case 27:
YY_RULE_SETUP
#line 156 "scanner.l"
{
return TRUSTED;
}
YY_BREAK case 28:YY_RULE_SETUP
{ return TRUSTED; }
YY_BREAK
case 28:
YY_RULE_SETUP
#line 157 "scanner.l"
{
yylval.symb = mkstring(yytext);
return ID;
}
YY_BREAK case 29:YY_RULE_SETUP
YY_BREAK
case 29:
YY_RULE_SETUP
#line 161 "scanner.l"
{
return yytext[0];
}
YY_BREAK case 30:YY_RULE_SETUP
{ return yytext[0]; }
YY_BREAK
case 30:
YY_RULE_SETUP
#line 165 "scanner.l"
ECHO;
YY_BREAK
@ -1067,6 +1086,7 @@ YY_DECL
/* Undo the effects of YY_DO_BEFORE_ACTION. */
*yy_cp = (yy_hold_char);
YY_RESTORE_YY_MORE_OFFSET
if ( YY_CURRENT_BUFFER_LVALUE->yy_buffer_status == YY_BUFFER_NEW )
{
/* We're scanning a new file or input source. It's
@ -1090,8 +1110,7 @@ YY_DECL
* end-of-buffer state). Contrast this with the test
* in input().
*/
if ((yy_c_buf_p) <=
&YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)])
if ( (yy_c_buf_p) <= &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)] )
{ /* This was really a NUL. */
yy_state_type yy_next_state;
@ -1127,8 +1146,7 @@ YY_DECL
}
}
else
switch (yy_get_next_buffer ())
else switch ( yy_get_next_buffer( ) )
{
case EOB_ACT_END_OF_FILE:
{
@ -1160,7 +1178,8 @@ YY_DECL
}
case EOB_ACT_CONTINUE_SCAN:
(yy_c_buf_p) = (yytext_ptr) + yy_amount_of_matched_text;
(yy_c_buf_p) =
(yytext_ptr) + yy_amount_of_matched_text;
yy_current_state = yy_get_previous_state( );
@ -1182,8 +1201,8 @@ YY_DECL
}
default:
YY_FATAL_ERROR
("fatal flex scanner internal error--no action found");
YY_FATAL_ERROR(
"fatal flex scanner internal error--no action found" );
} /* end of action switch */
} /* end of scanning one token */
} /* end of yylex */
@ -1195,8 +1214,7 @@ YY_DECL
* EOB_ACT_CONTINUE_SCAN - continue scanning from current position
* EOB_ACT_END_OF_FILE - end of file
*/
static int
yy_get_next_buffer (void)
static int yy_get_next_buffer (void)
{
register char *dest = YY_CURRENT_BUFFER_LVALUE->yy_ch_buf;
register char *source = (yytext_ptr);
@ -1204,8 +1222,8 @@ yy_get_next_buffer (void)
int ret_val;
if ( (yy_c_buf_p) > &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars) + 1] )
YY_FATAL_ERROR
("fatal flex scanner internal error--end of buffer missed");
YY_FATAL_ERROR(
"fatal flex scanner internal error--end of buffer missed" );
if ( YY_CURRENT_BUFFER_LVALUE->yy_fill_buffer == 0 )
{ /* Don't try to fill the buffer, so this is an EOF. */
@ -1251,7 +1269,8 @@ yy_get_next_buffer (void)
/* just a shorter name for the current buffer */
YY_BUFFER_STATE b = YY_CURRENT_BUFFER;
int yy_c_buf_p_offset = (int) ((yy_c_buf_p) - b->yy_ch_buf);
int yy_c_buf_p_offset =
(int) ((yy_c_buf_p) - b->yy_ch_buf);
if ( b->yy_is_our_buffer )
{
@ -1271,7 +1290,8 @@ yy_get_next_buffer (void)
b->yy_ch_buf = 0;
if ( ! b->yy_ch_buf )
YY_FATAL_ERROR ("fatal error - scanner input buffer overflow");
YY_FATAL_ERROR(
"fatal error - scanner input buffer overflow" );
(yy_c_buf_p) = &b->yy_ch_buf[yy_c_buf_p_offset];
@ -1301,7 +1321,8 @@ yy_get_next_buffer (void)
else
{
ret_val = EOB_ACT_LAST_MATCH;
YY_CURRENT_BUFFER_LVALUE->yy_buffer_status = YY_BUFFER_EOF_PENDING;
YY_CURRENT_BUFFER_LVALUE->yy_buffer_status =
YY_BUFFER_EOF_PENDING;
}
}
@ -1310,8 +1331,7 @@ yy_get_next_buffer (void)
(yy_n_chars) += number_to_move;
YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)] = YY_END_OF_BUFFER_CHAR;
YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars) + 1] =
YY_END_OF_BUFFER_CHAR;
YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars) + 1] = YY_END_OF_BUFFER_CHAR;
(yytext_ptr) = &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[0];
@ -1320,8 +1340,7 @@ yy_get_next_buffer (void)
/* yy_get_previous_state - get the state just before the EOB char was reached */
static yy_state_type
yy_get_previous_state (void)
static yy_state_type yy_get_previous_state (void)
{
register yy_state_type yy_current_state;
register char *yy_cp;
@ -1342,8 +1361,7 @@ yy_get_previous_state (void)
if ( yy_current_state >= 148 )
yy_c = yy_meta[(unsigned int) yy_c];
}
yy_current_state =
yy_nxt[yy_base[yy_current_state] + (unsigned int) yy_c];
yy_current_state = yy_nxt[yy_base[yy_current_state] + (unsigned int) yy_c];
}
return yy_current_state;
@ -1354,8 +1372,7 @@ yy_get_previous_state (void)
* synopsis
* next_state = yy_try_NUL_trans( current_state );
*/
static yy_state_type
yy_try_NUL_trans (yy_state_type yy_current_state)
static yy_state_type yy_try_NUL_trans (yy_state_type yy_current_state )
{
register int yy_is_jam;
register char *yy_cp = (yy_c_buf_p);
@ -1378,8 +1395,7 @@ yy_try_NUL_trans (yy_state_type yy_current_state)
return yy_is_jam ? 0 : yy_current_state;
}
static void
yyunput (int c, register char *yy_bp)
static void yyunput (int c, register char * yy_bp )
{
register char *yy_cp;
@ -1392,9 +1408,8 @@ yyunput (int c, register char *yy_bp)
{ /* need to shift things up to make room */
/* +2 for EOB chars. */
register int number_to_move = (yy_n_chars) + 2;
register char *dest =
&YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[YY_CURRENT_BUFFER_LVALUE->
yy_buf_size + 2];
register char *dest = &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[
YY_CURRENT_BUFFER_LVALUE->yy_buf_size + 2];
register char *source =
&YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[number_to_move];
@ -1412,8 +1427,7 @@ yyunput (int c, register char *yy_bp)
*--yy_cp = (char) c;
if (c == '\n')
{
if ( c == '\n' ){
--yylineno;
}
@ -1424,12 +1438,11 @@ yyunput (int c, register char *yy_bp)
#ifndef YY_NO_INPUT
#ifdef __cplusplus
static int
yyinput (void)
static int yyinput (void)
#else
static int
input (void)
static int input (void)
#endif
{
int c;
@ -1466,7 +1479,9 @@ input (void)
/* Reset buffer status. */
yyrestart(yyin );
/*FALLTHROUGH*/ case EOB_ACT_END_OF_FILE:
/*FALLTHROUGH*/
case EOB_ACT_END_OF_FILE:
{
if ( yywrap( ) )
return EOF;
@ -1505,14 +1520,13 @@ input (void)
*
* @note This function does not reset the start condition to @c INITIAL .
*/
void
yyrestart (FILE * input_file)
void yyrestart (FILE * input_file )
{
if (!YY_CURRENT_BUFFER)
{
if ( ! YY_CURRENT_BUFFER ){
yyensure_buffer_stack ();
YY_CURRENT_BUFFER_LVALUE = yy_create_buffer (yyin, YY_BUF_SIZE);
YY_CURRENT_BUFFER_LVALUE =
yy_create_buffer(yyin,YY_BUF_SIZE );
}
yy_init_buffer(YY_CURRENT_BUFFER,input_file );
@ -1523,8 +1537,7 @@ yyrestart (FILE * input_file)
* @param new_buffer The new input buffer.
*
*/
void
yy_switch_to_buffer (YY_BUFFER_STATE new_buffer)
void yy_switch_to_buffer (YY_BUFFER_STATE new_buffer )
{
/* TODO. We should be able to replace this entire function body
@ -1555,8 +1568,7 @@ yy_switch_to_buffer (YY_BUFFER_STATE new_buffer)
(yy_did_buffer_switch_on_eof) = 1;
}
static void
yy_load_buffer_state (void)
static void yy_load_buffer_state (void)
{
(yy_n_chars) = YY_CURRENT_BUFFER_LVALUE->yy_n_chars;
(yytext_ptr) = (yy_c_buf_p) = YY_CURRENT_BUFFER_LVALUE->yy_buf_pos;
@ -1570,8 +1582,7 @@ yy_load_buffer_state (void)
*
* @return the allocated buffer state.
*/
YY_BUFFER_STATE
yy_create_buffer (FILE * file, int size)
YY_BUFFER_STATE yy_create_buffer (FILE * file, int size )
{
YY_BUFFER_STATE b;
@ -1599,8 +1610,7 @@ yy_create_buffer (FILE * file, int size)
* @param b a buffer created with yy_create_buffer()
*
*/
void
yy_delete_buffer (YY_BUFFER_STATE b)
void yy_delete_buffer (YY_BUFFER_STATE b )
{
if ( ! b )
@ -1623,8 +1633,8 @@ extern int isatty (int);
* This function is sometimes called more than once on the same buffer,
* such as during a yyrestart() or at EOF.
*/
static void
yy_init_buffer (YY_BUFFER_STATE b, FILE * file)
static void yy_init_buffer (YY_BUFFER_STATE b, FILE * file )
{
int oerrno = errno;
@ -1637,8 +1647,7 @@ yy_init_buffer (YY_BUFFER_STATE b, FILE * file)
* called from yyrestart() or through yy_get_next_buffer.
* In that case, we don't want to reset the lineno or column.
*/
if (b != YY_CURRENT_BUFFER)
{
if (b != YY_CURRENT_BUFFER){
b->yy_bs_lineno = 1;
b->yy_bs_column = 0;
}
@ -1652,8 +1661,7 @@ yy_init_buffer (YY_BUFFER_STATE b, FILE * file)
* @param b the buffer state to be flushed, usually @c YY_CURRENT_BUFFER.
*
*/
void
yy_flush_buffer (YY_BUFFER_STATE b)
void yy_flush_buffer (YY_BUFFER_STATE b )
{
if ( ! b )
return;
@ -1682,8 +1690,7 @@ yy_flush_buffer (YY_BUFFER_STATE b)
* @param new_buffer The new state.
*
*/
void
yypush_buffer_state (YY_BUFFER_STATE new_buffer)
void yypush_buffer_state (YY_BUFFER_STATE new_buffer )
{
if (new_buffer == NULL)
return;
@ -1713,8 +1720,7 @@ yypush_buffer_state (YY_BUFFER_STATE new_buffer)
* The next element becomes the new top.
*
*/
void
yypop_buffer_state (void)
void yypop_buffer_state (void)
{
if (!YY_CURRENT_BUFFER)
return;
@ -1724,8 +1730,7 @@ yypop_buffer_state (void)
if ((yy_buffer_stack_top) > 0)
--(yy_buffer_stack_top);
if (YY_CURRENT_BUFFER)
{
if (YY_CURRENT_BUFFER) {
yy_load_buffer_state( );
(yy_did_buffer_switch_on_eof) = 1;
}
@ -1734,13 +1739,11 @@ yypop_buffer_state (void)
/* Allocates the stack if it does not exist.
* Guarantees space for at least one push.
*/
static void
yyensure_buffer_stack (void)
static void yyensure_buffer_stack (void)
{
int num_to_alloc;
if (!(yy_buffer_stack))
{
if (!(yy_buffer_stack)) {
/* First allocation is just for 2 elements, since we don't know if this
* scanner will even need a stack. We use 2 instead of 1 to avoid an
@ -1748,29 +1751,29 @@ yyensure_buffer_stack (void)
*/
num_to_alloc = 1;
(yy_buffer_stack) = (struct yy_buffer_state**)yyalloc
(num_to_alloc * sizeof (struct yy_buffer_state *));
(num_to_alloc * sizeof(struct yy_buffer_state*)
);
memset ((yy_buffer_stack), 0,
num_to_alloc * sizeof (struct yy_buffer_state *));
memset((yy_buffer_stack), 0, num_to_alloc * sizeof(struct yy_buffer_state*));
(yy_buffer_stack_max) = num_to_alloc;
(yy_buffer_stack_top) = 0;
return;
}
if ((yy_buffer_stack_top) >= ((yy_buffer_stack_max)) - 1)
{
if ((yy_buffer_stack_top) >= ((yy_buffer_stack_max)) - 1){
/* Increase the buffer to prepare for a possible push. */
int grow_size = 8 /* arbitrary grow size */;
num_to_alloc = (yy_buffer_stack_max) + grow_size;
(yy_buffer_stack) = (struct yy_buffer_state**)yyrealloc
((yy_buffer_stack), num_to_alloc * sizeof (struct yy_buffer_state *));
((yy_buffer_stack),
num_to_alloc * sizeof(struct yy_buffer_state*)
);
/* zero only the new slots.*/
memset ((yy_buffer_stack) + (yy_buffer_stack_max), 0,
grow_size * sizeof (struct yy_buffer_state *));
memset((yy_buffer_stack) + (yy_buffer_stack_max), 0, grow_size * sizeof(struct yy_buffer_state*));
(yy_buffer_stack_max) = num_to_alloc;
}
}
@ -1781,8 +1784,7 @@ yyensure_buffer_stack (void)
*
* @return the newly allocated buffer state object.
*/
YY_BUFFER_STATE
yy_scan_buffer (char *base, yy_size_t size)
YY_BUFFER_STATE yy_scan_buffer (char * base, yy_size_t size )
{
YY_BUFFER_STATE b;
@ -1819,8 +1821,7 @@ yy_scan_buffer (char *base, yy_size_t size)
* @note If you want to scan bytes that may contain NUL values, then use
* yy_scan_bytes() instead.
*/
YY_BUFFER_STATE
yy_scan_string (yyconst char *yystr)
YY_BUFFER_STATE yy_scan_string (yyconst char * yystr )
{
return yy_scan_bytes(yystr,strlen(yystr) );
@ -1833,8 +1834,7 @@ yy_scan_string (yyconst char *yystr)
*
* @return the newly allocated buffer state object.
*/
YY_BUFFER_STATE
yy_scan_bytes (yyconst char *yybytes, int _yybytes_len)
YY_BUFFER_STATE yy_scan_bytes (yyconst char * yybytes, int _yybytes_len )
{
YY_BUFFER_STATE b;
char *buf;
@ -1868,8 +1868,7 @@ yy_scan_bytes (yyconst char *yybytes, int _yybytes_len)
#define YY_EXIT_FAILURE 2
#endif
static void
yy_fatal_error (yyconst char *msg)
static void yy_fatal_error (yyconst char* msg )
{
(void) fprintf( stderr, "%s\n", msg );
exit( YY_EXIT_FAILURE );
@ -1897,8 +1896,7 @@ yy_fatal_error (yyconst char *msg)
/** Get the current line number.
*
*/
int
yyget_lineno (void)
int yyget_lineno (void)
{
return yylineno;
@ -1907,8 +1905,7 @@ yyget_lineno (void)
/** Get the input stream.
*
*/
FILE *
yyget_in (void)
FILE *yyget_in (void)
{
return yyin;
}
@ -1916,8 +1913,7 @@ yyget_in (void)
/** Get the output stream.
*
*/
FILE *
yyget_out (void)
FILE *yyget_out (void)
{
return yyout;
}
@ -1925,8 +1921,7 @@ yyget_out (void)
/** Get the length of the current token.
*
*/
int
yyget_leng (void)
int yyget_leng (void)
{
return yyleng;
}
@ -1935,8 +1930,7 @@ yyget_leng (void)
*
*/
char *
yyget_text (void)
char *yyget_text (void)
{
return yytext;
}
@ -1945,8 +1939,7 @@ yyget_text (void)
* @param line_number
*
*/
void
yyset_lineno (int line_number)
void yyset_lineno (int line_number )
{
yylineno = line_number;
@ -1958,32 +1951,27 @@ yyset_lineno (int line_number)
*
* @see yy_switch_to_buffer
*/
void
yyset_in (FILE * in_str)
void yyset_in (FILE * in_str )
{
yyin = in_str ;
}
void
yyset_out (FILE * out_str)
void yyset_out (FILE * out_str )
{
yyout = out_str ;
}
int
yyget_debug (void)
int yyget_debug (void)
{
return yy_flex_debug;
}
void
yyset_debug (int bdebug)
void yyset_debug (int bdebug )
{
yy_flex_debug = bdebug ;
}
static int
yy_init_globals (void)
static int yy_init_globals (void)
{
/* Initialization is the same as for the non-reentrant scanner.
* This function is called from yylex_destroy(), so don't allocate here.
@ -2015,13 +2003,11 @@ yy_init_globals (void)
}
/* yylex_destroy is for both reentrant and non-reentrant scanners. */
int
yylex_destroy (void)
int yylex_destroy (void)
{
/* Pop the buffer stack, destroying each element. */
while (YY_CURRENT_BUFFER)
{
while(YY_CURRENT_BUFFER){
yy_delete_buffer(YY_CURRENT_BUFFER );
YY_CURRENT_BUFFER_LVALUE = NULL;
yypop_buffer_state();
@ -2043,8 +2029,7 @@ yylex_destroy (void)
*/
#ifndef yytext_ptr
static void
yy_flex_strncpy (char *s1, yyconst char *s2, int n)
static void yy_flex_strncpy (char* s1, yyconst char * s2, int n )
{
register int i;
for ( i = 0; i < n; ++i )
@ -2053,8 +2038,7 @@ yy_flex_strncpy (char *s1, yyconst char *s2, int n)
#endif
#ifdef YY_NEED_STRLEN
static int
yy_flex_strlen (yyconst char *s)
static int yy_flex_strlen (yyconst char * s )
{
register int n;
for ( n = 0; s[n]; ++n )
@ -2064,14 +2048,12 @@ yy_flex_strlen (yyconst char *s)
}
#endif
void *
yyalloc (yy_size_t size)
void *yyalloc (yy_size_t size )
{
return (void *) malloc( size );
}
void *
yyrealloc (void *ptr, yy_size_t size)
void *yyrealloc (void * ptr, yy_size_t size )
{
/* The cast to (char *) in the following accommodates both
* implementations that use char* generic pointers, and those
@ -2083,8 +2065,7 @@ yyrealloc (void *ptr, yy_size_t size)
return (void *) realloc( (char *) ptr, size );
}
void
yyfree (void *ptr)
void yyfree (void * ptr )
{
free( (char *) ptr ); /* see yyrealloc() for (char *) cast */
}
@ -2095,8 +2076,7 @@ yyfree (void *ptr)
Symbol
mkstring (char *name)
Symbol mkstring(char *name)
{
Symbol t;
char* s;
@ -2126,14 +2106,12 @@ mkstring (char *name)
return t;
}
void
scanner_cleanup (void)
void scanner_cleanup(void)
{
yy_delete_buffer (YY_CURRENT_BUFFER);
}
void
strings_cleanup (void)
void strings_cleanup(void)
{
Stringlist sl;
while (allocatedStrings != NULL)
@ -2145,8 +2123,7 @@ strings_cleanup (void)
}
}
int
yywrap (void)
int yywrap (void)
{
/* signal true to let lex know that nothing else is coming */
return 1;
@ -2160,3 +2137,4 @@ void mktext(void);
// vim:ft=lex:

1
src/specialterm.c
View File

@ -3,6 +3,7 @@
#include "term.h"
#include "termlist.h"
#include "compiler.h"
#include "error.h"
/*
* Some macros

2
src/specialterm.h
View File

@ -3,6 +3,7 @@
#include "term.h"
#include "termlist.h"
#include "system.h"
/*
* Some declarations in spercialterm.c
@ -25,6 +26,7 @@ extern Term CLAIM_Reachable;
extern Termlist CLAIMS_dep_prec;
void specialTermInit (const System sys);
int isTicketTerm (Term t);
int hasTicketSubterm (Term t);

1
src/states.c
View File

@ -1,4 +1,5 @@
#include "states.h"
#include "symbol.h"
/* States counter operations
*

1
src/switches.c
View File

@ -282,7 +282,6 @@ switcher (const int process, int index, int commandline)
char **argv;
char *arg_pointer;
int arg_index;
//! Check whether there are still n options left
int enough_arguments_left (const int n, char shortopt, char *longopt)

1
src/symbol.c
View File

@ -266,6 +266,7 @@ symbolNextFree (Symbol prefixsymbol)
}
error ("We ran out of numbers (%i) when trying to generate a fresh symbol.",
n);
return NULL;
}
//! Fix all the unset keylevels

2
src/system.c
View File

@ -10,6 +10,7 @@
#include "knowledge.h"
#include "system.h"
#include "debug.h"
#include "error.h"
#include "role.h"
#include "mgu.h"
#include "switches.h"
@ -148,7 +149,6 @@ systemRuns (const System sys)
void
systemDone (const System sys)
{
int run;
int s;
/* clear globals, which were defined in systemStart */

1
src/system.h
View File

@ -212,6 +212,7 @@ int selfResponder (const System sys, const int run);
int selfResponders (const System sys);
int selfInitiator (const System sys, const int run);
int selfInitiators (const System sys);
int enoughAttacks (const System sys);
//! Equality for run structure naming

3
src/tac.c
View File

@ -3,6 +3,7 @@
#include "tac.h"
#include "memory.h"
#include "switches.h"
#include "error.h"
extern int yylineno;
@ -183,6 +184,8 @@ tacTuple (Tac taclist)
error ("Unknown tupling mode (--tupling=%i)", switches.tupling);
}
}
// @TODO this should be considered an error
return NULL;
}
/*

7
src/term.c
View File

@ -16,6 +16,7 @@
#include <string.h>
#include "term.h"
#include "debug.h"
#include "error.h"
#include "ctype.h"
#include "specialterm.h"
@ -866,9 +867,6 @@ termDistance (Term t1, Term t2)
int
termOrder (Term t1, Term t2)
{
char *name1;
char *name2;
t1 = deVar (t1);
t2 = deVar (t2);
if (isTermEqual (t1, t2))
@ -938,6 +936,8 @@ termOrder (Term t1, Term t2)
else
return compR;
}
// @TODO Should be considered an error
return 0;
}
//! Generic term iteration
@ -1177,7 +1177,6 @@ term_constrain_level (const Term term)
{
int vars;
int structure;
int flag;
void tcl_iterate (Term t)
{

3
src/termlist.c
View File

@ -3,6 +3,7 @@
#include "termlist.h"
#include "specialterm.h"
#include "debug.h"
#include "error.h"
/*
* Shared stuff
@ -912,6 +913,8 @@ termlist_to_tuple (Termlist tl)
return termDuplicate (tl->term);
}
}
// @TODO Should be considered an error
return NULL;
}
//! Split a tuple term into termlist components.

3
src/xmlout.c
View File

@ -21,6 +21,7 @@
#include "specialterm.h"
#include "claim.h"
#include "dotout.h"
#include "type.h"
#include "xmlout.h"
@ -614,8 +615,6 @@ xmlOutEvent (const System sys, Roledef rd, const int run, const int index)
// Display any incoming bindings
{
int incomingArrows;
int xmlBindingState (void *dt)
{
Binding b;