- Filtered out uninteresting claim events in attack descriptions. This
was already being done in the script by Gijs. I only added it to make the XML output more readable for humans.
This commit is contained in:
		
							parent
							
								
									8b51593cf5
								
							
						
					
					
						commit
						ffaf0d2ded
					
				
							
								
								
									
										44
									
								
								src/xmlout.c
									
									
									
									
									
								
							
							
						
						
									
										44
									
								
								src/xmlout.c
									
									
									
									
									
								
							| @ -30,6 +30,7 @@ extern Term TERM_Function;	// from termlist.c | |||||||
|  * Global/static stuff. |  * Global/static stuff. | ||||||
|  */ |  */ | ||||||
| static int xmlindent;		// indent level for xml elements in output
 | static int xmlindent;		// indent level for xml elements in output
 | ||||||
|  | static Term only_claim_label;	// if NULL, show all claims in xml event lists. Otherwise, only this one.
 | ||||||
| 
 | 
 | ||||||
| /*
 | /*
 | ||||||
|  * Default external interface: init/done |  * Default external interface: init/done | ||||||
| @ -41,6 +42,7 @@ xmlOutInit (void) | |||||||
| { | { | ||||||
|   printf ("<scyther>\n"); |   printf ("<scyther>\n"); | ||||||
|   xmlindent = 1; |   xmlindent = 1; | ||||||
|  |   only_claim_label = NULL; | ||||||
| } | } | ||||||
| 
 | 
 | ||||||
| //! Close up
 | //! Close up
 | ||||||
| @ -270,6 +272,32 @@ isProtocolInvolved (const System sys, const Protocol p) | |||||||
|   return 0; |   return 0; | ||||||
| } | } | ||||||
| 
 | 
 | ||||||
|  | //! Determine whether to show an event
 | ||||||
|  | int | ||||||
|  | isEventInteresting (const Roledef rd) | ||||||
|  | { | ||||||
|  |   if (rd->type != CLAIM) | ||||||
|  |     { | ||||||
|  |       return 1; | ||||||
|  |     } | ||||||
|  |   else | ||||||
|  |     { | ||||||
|  |       // A claim
 | ||||||
|  |       if (only_claim_label == NULL) | ||||||
|  | 	{ | ||||||
|  | 	  return 1; | ||||||
|  | 	} | ||||||
|  |       else | ||||||
|  | 	{ | ||||||
|  | 	  if (isTermEqual (only_claim_label, rd->label)) | ||||||
|  | 	    { | ||||||
|  | 	      return 1; | ||||||
|  | 	    } | ||||||
|  | 	} | ||||||
|  |     } | ||||||
|  |   return 0; | ||||||
|  | } | ||||||
|  | 
 | ||||||
| //! Show a single event from a run
 | //! Show a single event from a run
 | ||||||
| /**
 | /**
 | ||||||
|  * run and index will only be output if they are nonnegative. |  * run and index will only be output if they are nonnegative. | ||||||
| @ -281,6 +309,11 @@ isProtocolInvolved (const System sys, const Protocol p) | |||||||
| void | void | ||||||
| xmlOutEvent (const System sys, Roledef rd, const int run, const int index) | xmlOutEvent (const System sys, Roledef rd, const int run, const int index) | ||||||
| { | { | ||||||
|  |   if (!isEventInteresting (rd)) | ||||||
|  |     { | ||||||
|  |       return; | ||||||
|  |     } | ||||||
|  | 
 | ||||||
|   xmlIndentPrint (); |   xmlIndentPrint (); | ||||||
| 
 | 
 | ||||||
|   printf ("<event type=\""); |   printf ("<event type=\""); | ||||||
| @ -568,6 +601,8 @@ xmlOutTrace (const System sys) | |||||||
| void | void | ||||||
| xmlOutSemitrace (const System sys) | xmlOutSemitrace (const System sys) | ||||||
| { | { | ||||||
|  |   Term buffer_only_claim_label; | ||||||
|  | 
 | ||||||
|   xmlIndentPrint (); |   xmlIndentPrint (); | ||||||
|   printf ("<attack"); |   printf ("<attack"); | ||||||
|   /* add trace length attribute */ |   /* add trace length attribute */ | ||||||
| @ -576,6 +611,7 @@ xmlOutSemitrace (const System sys) | |||||||
|   xmlindent++; |   xmlindent++; | ||||||
| 
 | 
 | ||||||
|   /* mention the broken claim */ |   /* mention the broken claim */ | ||||||
|  |   buffer_only_claim_label = only_claim_label; | ||||||
|   if (sys->current_claim != NULL) |   if (sys->current_claim != NULL) | ||||||
|     { |     { | ||||||
|       xmlPrint ("<broken>"); |       xmlPrint ("<broken>"); | ||||||
| @ -584,6 +620,11 @@ xmlOutSemitrace (const System sys) | |||||||
|       xmlOutTerm ("label", sys->current_claim->label); |       xmlOutTerm ("label", sys->current_claim->label); | ||||||
|       xmlindent--; |       xmlindent--; | ||||||
|       xmlPrint ("</broken>"); |       xmlPrint ("</broken>"); | ||||||
|  |       only_claim_label = sys->current_claim->label; | ||||||
|  |     } | ||||||
|  |   else | ||||||
|  |     { | ||||||
|  |       only_claim_label = NULL; | ||||||
|     } |     } | ||||||
|   /* any global information about the system */ |   /* any global information about the system */ | ||||||
|   xmlOutSysInfo (sys); |   xmlOutSysInfo (sys); | ||||||
| @ -595,4 +636,7 @@ xmlOutSemitrace (const System sys) | |||||||
|   xmlPrint ("</semitrace>"); |   xmlPrint ("</semitrace>"); | ||||||
|   xmlindent--; |   xmlindent--; | ||||||
|   xmlPrint ("</attack>"); |   xmlPrint ("</attack>"); | ||||||
|  | 
 | ||||||
|  |   /* restore only claim buffer */ | ||||||
|  |   only_claim_label = buffer_only_claim_label; | ||||||
| } | } | ||||||
|  | |||||||
		Loading…
	
		Reference in New Issue
	
	Block a user