#71: itracer is only for debugger

sdasgup3 · May 17, 2018 · 33250c3 · 33250c3
1 parent cbe35d2
commit 33250c3
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 3 deletions.
diff --git a/x86-semantics/semantics/x86-configuration.k b/x86-semantics/semantics/x86-configuration.k
@@ -98,8 +98,12 @@ module X86-CONFIGURATION
     /*@
       The following configuration is used to store the intermediate
       regstate at instruction boundary. Used in debug/testing purposes.
+
+      itracer: For debug purposes
+      regstatequeue: For testing purposes
     */
-    <itracer> .List </itracer>
+
+    // <itracer> .List </itracer>
     <regstatequeue> .List </regstatequeue>
 
   </T>

diff --git a/x86-semantics/semantics/x86-fetch-execute.k b/x86-semantics/semantics/x86-fetch-execute.k
@@ -28,9 +28,8 @@ module X86-FETCH-EXECUTE
   rule
     <k> inforegisters => . ... </k>
       <regstatequeue> ... .List => ListItem(RSMap) </regstatequeue>
-      <itracer> ... .List => ListItem(CMap[iloc( {RSMap["RIP"]}:>MInt )]) </itracer>
+      // <itracer> ... .List => ListItem(CMap[iloc( {RSMap["RIP"]}:>MInt )]) </itracer>
       <regstate> RSMap </regstate>
-      // <text>code(iloc({RSMap["RIP"]}:>MInt) |-> storedInstr(OpC OpR) _:Map) </text>
       <text> code (CMap) </text>
         requires  iloc( {RSMap["RIP"]}:>MInt ) in_keys ( CMap )