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

- Fixed some Doxygen documentation errors.

Browse Source
This commit is contained in:
ccremers 2006-03-08 12:38:39 +00:00
parent 1678577ce0
commit 2830c8e8ff
2 changed files with 10 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
src/modelchecker.c
View File

@ -32,13 +32,13 @@
Some forward declarations. Some forward declarations.
*/ */
__inline__ int traverseSimple (const System oldsys); int traverseSimple (const System oldsys);
__inline__ int traverseNonReads (const System oldsys); int traverseNonReads (const System oldsys);
__inline__ int traversePOR4 (const System oldsys); int traversePOR4 (const System oldsys);
__inline__ int traversePOR5 (const System oldsys); int traversePOR5 (const System oldsys);
__inline__ int traversePOR6 (const System oldsys); int traversePOR6 (const System oldsys);
__inline__ int traversePOR7 (const System oldsys); int traversePOR7 (const System oldsys);
__inline__ int traversePOR8 (const System oldsys); int traversePOR8 (const System oldsys);
int propertyCheck (const System sys); int propertyCheck (const System sys);
int executeTry (const System sys, int run); int executeTry (const System sys, int run);
int claimSecrecy (const System sys, const Term t); int claimSecrecy (const System sys, const Term t);

6
src/prune_theorems.c
View File

@ -357,7 +357,7 @@ prune_theorems (const System sys)
b = bl->data; b = bl->data;
// Check for "Hidden" interm goals // Check for "Hidden" interm goals
//!@TODO in the future, this can be subsumed by adding TERM_Hidden to the hidelevel constructs //! @todo in the future, this can be subsumed by adding TERM_Hidden to the hidelevel constructs
if (termInTerm (b->term, TERM_Hidden)) if (termInTerm (b->term, TERM_Hidden))
{ {
// Prune the state: we can never meet this // Prune the state: we can never meet this
@ -376,7 +376,7 @@ prune_theorems (const System sys)
// Check for SK-type function occurrences // Check for SK-type function occurrences
//!@todo Needs a LEMMA, although this seems to be quite straightforward to prove. //!@todo Needs a LEMMA, although this seems to be quite straightforward to prove.
// The idea is that functions are never sent as a whole, but only used in applications. // The idea is that functions are never sent as a whole, but only used in applications.
//!@TODO Subsumed by hidelevel lemma later //! @todo Subsumed by hidelevel lemma later
if (isTermFunctionName (b->term)) if (isTermFunctionName (b->term))
{ {
if (!inKnowledge (sys->know, b->term)) if (!inKnowledge (sys->know, b->term))
@ -397,7 +397,7 @@ prune_theorems (const System sys)
// Check for encryption levels // Check for encryption levels
/* /*
* if (switches.match < 2 * if (switches.match < 2
*!@TODO Doesn't work yet as desired for Tickets. Prove lemma first. *! @todo Doesn't work yet as desired for Tickets. Prove lemma first.
*/ */
if (switches.experimental & 2) if (switches.experimental & 2)
{ {