- New todo priority.

This commit is contained in:
ccremers 2006-08-07 18:10:05 +00:00
parent 8bff33dc82
commit cbe6307e8a

View File

@ -1,3 +1,9 @@
- Add --filter-claim and --filter-label switches; parse as symbols, and
turn into (global?) terms, add to switches termlists. Later check them
using two new term functions:
const char *termSymbolString(Term t);
int termSymbolEqual(Term t1, Term t2);
Iteration through the termlist should be done by hand.
- --check is slightly f***ed up because there is no good semantics for - --check is slightly f***ed up because there is no good semantics for
the --disable intruder check. As a result, it is now too strict can the --disable intruder check. As a result, it is now too strict can
cause correct protocols to fail. Fix. cause correct protocols to fail. Fix.
@ -33,14 +39,6 @@
Now that I think of it; XML should be a plain state probably, and we Now that I think of it; XML should be a plain state probably, and we
could add a switch to also output more detailed attack things (is could add a switch to also output more detailed attack things (is
that relevant?) that relevant?)
- Add --filter-claim and --filter-label switches; parse as symbols, and
turn into (global?) terms, add to switches termlists. Later check them
using two new term functions:
const char *termSymbolString(Term t);
int termSymbolEqual(Term t1, Term t2);
Iteration through the termlist should be done by hand.
- Maybe add warning for type of matching in the output, maybe stderr.
Maybe all state-space bounding info should be displayed.
- SConstruct file should check whether ctags actually exists (avoiding - SConstruct file should check whether ctags actually exists (avoiding
errors) errors)
- Proof output should be XML, with an external converter to dot format. - Proof output should be XML, with an external converter to dot format.