BUGFIX: Auto-claim naming scheme was context dependent.
The automatic mechanism to assign labels to claims was dependent on the context. In practice, a claim could get a different label when analyzed in isolation compared to when analyzed in parallel with some other protocols. This caused problems for the multi-protocol analysis.
This commit is contained in:
parent
810fc9eece
commit
a03f06ea41
@ -466,7 +466,7 @@ isClaimlabelUsed (const System sys, const Term label)
|
||||
//! Generate a fresh claim label
|
||||
Term
|
||||
generateFreshClaimlabel (const System sys, const Protocol protocol,
|
||||
const Role role, const Term claim)
|
||||
const Role role, const Term claim, const int n)
|
||||
{
|
||||
Term label;
|
||||
|
||||
@ -489,13 +489,16 @@ claimCreate (const System sys, const Protocol protocol, const Role role,
|
||||
const Term claim, Term label, const Term msg, const int lineno)
|
||||
{
|
||||
Claimlist cl;
|
||||
int len;
|
||||
|
||||
len = roledef_length (role->roledef);
|
||||
|
||||
/* generate full unique label */
|
||||
/* is the label empty or used? */
|
||||
if (label == NULL || isClaimlabelUsed (sys, label))
|
||||
{
|
||||
/* simply generate a fresh one */
|
||||
label = generateFreshClaimlabel (sys, protocol, role, claim);
|
||||
label = generateFreshClaimlabel (sys, protocol, role, claim, len);
|
||||
}
|
||||
|
||||
// Assert: label is unique, add claimlist info
|
||||
@ -606,7 +609,18 @@ commEvent (int event, Tac tc)
|
||||
* This can be a weird choice if it is a read or send, because in that case
|
||||
* we cannot chain them anymore and the send-read correspondence is lost.
|
||||
*/
|
||||
label = freshTermPrefix (thisRole->nameterm);
|
||||
int n;
|
||||
Roledef rd;
|
||||
|
||||
n = 1;
|
||||
for (rd = thisRole->roledef; rd != NULL; rd = rd->next)
|
||||
{
|
||||
if (rd->type == CLAIM)
|
||||
{
|
||||
n++;
|
||||
}
|
||||
}
|
||||
label = intTermPrefix (n, thisRole->nameterm);
|
||||
}
|
||||
else
|
||||
{
|
||||
|
54
src/symbol.c
54
src/symbol.c
@ -291,6 +291,60 @@ symbolNextFree (Symbol prefixsymbol)
|
||||
return NULL;
|
||||
}
|
||||
|
||||
//! Return symbol according to integer
|
||||
Symbol
|
||||
symbolFromInt (int n, Symbol prefixsymbol)
|
||||
{
|
||||
char *prefixstr;
|
||||
int len;
|
||||
|
||||
if (!(n <= 9999))
|
||||
{
|
||||
error ("Can only make symbol from int when smaller than 10000");
|
||||
}
|
||||
|
||||
if (prefixsymbol != NULL)
|
||||
{
|
||||
prefixstr = (char *) prefixsymbol->text;
|
||||
len = strlen (prefixstr);
|
||||
}
|
||||
else
|
||||
{
|
||||
prefixstr = "";
|
||||
len = 0;
|
||||
}
|
||||
|
||||
/*
|
||||
* The construction below (variable buffer length) is not allowed in ISO C90
|
||||
*/
|
||||
char buffer[len + 5]; // thus we must enforce a maximum of 9.999 (allowing for storage of \0 )
|
||||
Symbol symb;
|
||||
int slen;
|
||||
|
||||
slen = sprintf (buffer, "%s%i", prefixstr, n);
|
||||
buffer[slen] = EOS;
|
||||
symb = lookup (buffer);
|
||||
if (symb == NULL)
|
||||
{
|
||||
char *newstring;
|
||||
// Copy the buffer to something that will survive
|
||||
/**
|
||||
* Memory leak: although this routine should not be called recursively, it will never de-allocate this memory.
|
||||
* Thus, some precaution is necessary.
|
||||
* [x][CC]
|
||||
*/
|
||||
newstring = (char *) malloc (slen + 1);
|
||||
memcpy (newstring, buffer, slen + 1);
|
||||
|
||||
/* This persistent string can be used to return a fresh symbol */
|
||||
|
||||
symb = symbolSysConst (newstring);
|
||||
}
|
||||
|
||||
return symb;
|
||||
|
||||
}
|
||||
|
||||
//! Fix all the unset keylevels
|
||||
void
|
||||
symbol_fix_keylevels (void)
|
||||
|
@ -67,6 +67,7 @@ void symbolPrintAll (void);
|
||||
Symbol symbolSysConst (const char *str);
|
||||
void symbol_fix_keylevels (void);
|
||||
Symbol symbolNextFree (Symbol prefixsymbol);
|
||||
Symbol symbolFromInt (int n, Symbol prefixsymbol);
|
||||
|
||||
void eprintf (char *fmt, ...);
|
||||
void veprintf (const char *fmt, va_list args);
|
||||
|
16
src/term.c
16
src/term.c
@ -1386,6 +1386,22 @@ freshTermPrefix (Term prefixterm)
|
||||
return makeTermType (GLOBAL, freshsymbol, -1);
|
||||
}
|
||||
|
||||
//! Generate a term from an int, prefixed with the string of the given term.
|
||||
Term
|
||||
intTermPrefix (const int n, Term prefixterm)
|
||||
{
|
||||
Symbol prefixsymbol;
|
||||
Symbol freshsymbol;
|
||||
|
||||
prefixsymbol = NULL;
|
||||
if (prefixterm != NULL && realTermLeaf (prefixterm))
|
||||
{
|
||||
prefixsymbol = TermSymb (prefixterm);
|
||||
}
|
||||
freshsymbol = symbolFromInt (n, prefixsymbol);
|
||||
return makeTermType (GLOBAL, freshsymbol, -1);
|
||||
}
|
||||
|
||||
//! Determine whether a term is a functor
|
||||
int
|
||||
isTermFunctionName (Term t)
|
||||
|
@ -201,6 +201,7 @@ void term_set_keylevels (const Term term);
|
||||
void termPrintDiff (Term t1, Term t2);
|
||||
int isLeafNameEqual (Term t1, Term t2);
|
||||
Term freshTermPrefix (Term prefixterm);
|
||||
Term intTermPrefix (const int n, Term prefixterm);
|
||||
int isTermFunctionName (Term t);
|
||||
Term getTermFunction (Term t);
|
||||
unsigned int termHidelevel (const Term tsmall, Term tbig);
|
||||
|
Loading…
Reference in New Issue
Block a user