- Misc fixes, some reporting with --check.
This commit is contained in:
		
							parent
							
								
									e902aaa260
								
							
						
					
					
						commit
						cc358c5df3
					
				| @ -1853,7 +1853,8 @@ checkWellFormed (const System sys) | |||||||
| { | { | ||||||
|   int thisRole (Protocol p, Role r) |   int thisRole (Protocol p, Role r) | ||||||
|   { |   { | ||||||
|     return WellFormedRole (sys, p, r); |     WellFormedRole (sys, p, r); | ||||||
|  |     return true; | ||||||
|   } |   } | ||||||
| 
 | 
 | ||||||
|   iterateRoles (sys, thisRole); |   iterateRoles (sys, thisRole); | ||||||
|  | |||||||
| @ -12,11 +12,12 @@ addSTerm (const System sys, Term t, Termlist fromlist, Termlist tolist) | |||||||
| 
 | 
 | ||||||
|   t2 = termLocal (t, fromlist, tolist); |   t2 = termLocal (t, fromlist, tolist); | ||||||
| 
 | 
 | ||||||
|   /*
 |   if (switches.check) | ||||||
|      eprintf ("[ Adding "); |     { | ||||||
|      termPrint (t2); |       eprintf ("[ Adding "); | ||||||
|      eprintf (" to the initial intruder knowledge]\n"); |       termPrint (t2); | ||||||
|    */ |       eprintf (" to the initial intruder knowledge]\n"); | ||||||
|  |     } | ||||||
| } | } | ||||||
| 
 | 
 | ||||||
| //! Unfold the term for all possible options
 | //! Unfold the term for all possible options
 | ||||||
|  | |||||||
| @ -491,6 +491,7 @@ WellFormedEvent (Term role, Knowledge know, Roledef rd) | |||||||
| 		    NULL); | 		    NULL); | ||||||
| 	  return NULL; | 	  return NULL; | ||||||
| 	} | 	} | ||||||
|  |       return know; | ||||||
|     } |     } | ||||||
|   if (rd->type == CLAIM) |   if (rd->type == CLAIM) | ||||||
|     { |     { | ||||||
| @ -500,7 +501,12 @@ WellFormedEvent (Term role, Knowledge know, Roledef rd) | |||||||
| 	  wfeError (know, rd, "Claiming role incorrect.", rd->from, role); | 	  wfeError (know, rd, "Claiming role incorrect.", rd->from, role); | ||||||
| 	  return NULL; | 	  return NULL; | ||||||
| 	} | 	} | ||||||
|  |       return know; | ||||||
|     } |     } | ||||||
|   // Unknown, false
 |   // Unknown, false
 | ||||||
|  |   globalError++; | ||||||
|  |   roledefPrint (rd); | ||||||
|  |   globalError--; | ||||||
|  |   error ("I don't know this event"); | ||||||
|   return NULL; |   return NULL; | ||||||
| } | } | ||||||
|  | |||||||
		Loading…
	
		Reference in New Issue
	
	Block a user