Introduced 'fresh' for fresh value generation and added deprecation warning for 'const' usage.

This commit is contained in:
Cas Cremers 2010-01-05 13:45:19 +01:00
parent 519a9d0a81
commit 6d9d89eca2
4 changed files with 37 additions and 4 deletions

View File

@ -850,6 +850,30 @@ normalDeclaration (Tac tc)
levelDeclareConst (tc); levelDeclareConst (tc);
if (level < 2 && tc->t3.tac == NULL) if (level < 2 && tc->t3.tac == NULL)
knowledgeAddTermlist (sys->know, tacTermlist (tc->t1.tac)); knowledgeAddTermlist (sys->know, tacTermlist (tc->t1.tac));
if (level > 0)
{
globalError++;
warning_pre ();
eprintf ("const ");
termlistPrint (tacTermlist (tc->t1.tac));
eprintf
(" usage inside roles is deprecated. Please use 'fresh' instead on line %i.\n",
tc->lineno);
globalError--;
}
break;
case TAC_FRESH:
levelDeclareConst (tc);
if (level < 2)
{
globalError++;
error_pre ();
eprintf ("fresh terms ");
termlistPrint (tacTermlist (tc->t1.tac));
eprintf (" should be declared inside roles,");
errorTac (tc->lineno); // exits Scyther here
globalError--;
}
break; break;
case TAC_SECRET: case TAC_SECRET:
levelDeclareConst (tc); levelDeclareConst (tc);

View File

@ -45,6 +45,7 @@ int yylex(void);
%token CLAIMT %token CLAIMT
%token VAR %token VAR
%token CONST %token CONST
%token FRESH
%token RUN %token RUN
%token SECRET %token SECRET
%token COMPROMISED %token COMPROMISED
@ -221,16 +222,22 @@ knowsdecl : KNOWS termlist ';'
declaration : secretpref CONST basictermlist typeinfo1 ';' declaration : secretpref CONST basictermlist typeinfo1 ';'
{ Tac t = tacCreate(TAC_CONST); { Tac t = tacCreate(TAC_CONST);
t->t1.tac = $3; t->t1.tac = $3; // names
t->t2.tac = $4; t->t2.tac = $4; // type
t->t3.tac = $1; t->t3.tac = $1; // secret?
$$ = t;
}
| FRESH basictermlist typeinfo1 ';'
{ Tac t = tacCreate(TAC_FRESH);
t->t1.tac = $2; // names
t->t2.tac = $3; // type
$$ = t; $$ = t;
} }
| secretpref VAR basictermlist typeinfoN ';' | secretpref VAR basictermlist typeinfoN ';'
{ Tac t = tacCreate(TAC_VAR); { Tac t = tacCreate(TAC_VAR);
t->t1.tac = $3; t->t1.tac = $3;
t->t2.tac = $4; t->t2.tac = $4;
t->t3.tac = $1; t->t3.tac = $1; // obsolete: should not even occur at the global level
$$ = t; $$ = t;
} }
| SECRET basictermlist typeinfo1 ';' | SECRET basictermlist typeinfo1 ';'

View File

@ -162,6 +162,7 @@ recv { return RECVT; }
send { return SENDT; } send { return SENDT; }
var { return VAR; } var { return VAR; }
const { return CONST; } const { return CONST; }
fresh { return FRESH; }
claim { return CLAIMT; } claim { return CLAIMT; }
run { return RUN; } run { return RUN; }
secret { return SECRET; } secret { return SECRET; }

View File

@ -34,6 +34,7 @@ enum tactypes
TAC_ENCRYPT, TAC_ENCRYPT,
TAC_VAR, TAC_VAR,
TAC_CONST, TAC_CONST,
TAC_FRESH,
TAC_READ, TAC_READ,
TAC_SEND, TAC_SEND,
TAC_CLAIM, TAC_CLAIM,