diff --git a/src/compiler.c b/src/compiler.c index 270ab9d..8a9d093 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -850,6 +850,30 @@ normalDeclaration (Tac tc) levelDeclareConst (tc); if (level < 2 && tc->t3.tac == NULL) 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; case TAC_SECRET: levelDeclareConst (tc); diff --git a/src/parser.y b/src/parser.y index 4be7a29..c6469be 100644 --- a/src/parser.y +++ b/src/parser.y @@ -45,6 +45,7 @@ int yylex(void); %token CLAIMT %token VAR %token CONST +%token FRESH %token RUN %token SECRET %token COMPROMISED @@ -221,16 +222,22 @@ knowsdecl : KNOWS termlist ';' declaration : secretpref CONST basictermlist typeinfo1 ';' { Tac t = tacCreate(TAC_CONST); - t->t1.tac = $3; - t->t2.tac = $4; - t->t3.tac = $1; + t->t1.tac = $3; // names + t->t2.tac = $4; // type + 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; } | secretpref VAR basictermlist typeinfoN ';' { Tac t = tacCreate(TAC_VAR); t->t1.tac = $3; t->t2.tac = $4; - t->t3.tac = $1; + t->t3.tac = $1; // obsolete: should not even occur at the global level $$ = t; } | SECRET basictermlist typeinfo1 ';' diff --git a/src/scanner.l b/src/scanner.l index 77b6c2c..1690a98 100644 --- a/src/scanner.l +++ b/src/scanner.l @@ -162,6 +162,7 @@ recv { return RECVT; } send { return SENDT; } var { return VAR; } const { return CONST; } +fresh { return FRESH; } claim { return CLAIMT; } run { return RUN; } secret { return SECRET; } diff --git a/src/tac.h b/src/tac.h index c6b6a16..6183d16 100644 --- a/src/tac.h +++ b/src/tac.h @@ -34,6 +34,7 @@ enum tactypes TAC_ENCRYPT, TAC_VAR, TAC_CONST, + TAC_FRESH, TAC_READ, TAC_SEND, TAC_CLAIM,