Merge branch 'master' of https://github.com/resource-reasoning/jscert_dev

navig.html

@@ -120,7 +120,7 @@
 <span id="run_output"></span>
 Navigation:
 <input type="textbox" id='navigation_step' style="width:3em" value="0"/>
-/<span id="navigation_total"></span>
+/ <span id="navigation_total"></span>
 <input type="button" id='button_reset' value="Reset" />
 <input type="button" id='button_prev' value="Prev" />
 <input type="button" id='button_next' value="Next" />
@@ -163,13 +163,13 @@ $(function() {
 
 <div style="font-size:0.8em">Examples of conditions:
     <ul>
-        <li><pre style = "display:inline">type === "fun" && (v1, true)</pre> (we are at the beginning of a function and v1 is defined)</li>
-        <li><pre style = "display:inline">line === 32 && t.field === "bar"</pre> (we are at line 32 and we are setting the field “bar” of the current location)</li>
-        <li><pre style = "display:inline">heap[0].bar === 12</pre> (the first cell of the heap has a field “bar” defined equal to 12)</li>
+        <li><pre style = "display:inline">X.type === "fun" && (X.v1, true)</pre> (we are at the beginning of a function and v1 is defined in the local interpreter context),</li>
+        <li><pre style = "display:inline">X.line === 32 && X.t.tag === "trm_set" && X.t.field === "bar"</pre> (we are at line 32 and we are setting the field “bar” of the current location),</li>
+        <li><pre style = "display:inline">x.foo === 12</pre> (the program variable has field “foo” equals to 12),</li>
+        <li><pre style = "display:inline">X.heap[0].bar === 12</pre> (the first cell of the heap has a field “bar” defined equal to 12).</li>
     </ul></div>
 
 
-
 </body>
 </html>
 

navig.js

@@ -23,19 +23,20 @@ function stepTo(step) {
 }
 
 // Take a predicate in form of a JavaScript code (string) and returns either true or an error message (string).
-// The predicate can make use of the line, the event type, , the heap, or any local variable of the context ctx.
 function goToPred(pred) {
 
   function check(i){
     var item = datalog[i];
     var jsheap = jsheap_of_heap(item.heap);
-    var obj = {};
+    var obj = jsenv_of_env(jsheap, item.env);
+    var objX = {};
     if (item.ctx !== undefined){
-        obj = jsenv_of_env(jsheap, item.ctx);
+        objX = jsenv_of_env(jsheap, item.ctx);
     }
-    obj.line = item.line;
-    obj.type = item.type;
-    obj.heap = jsheap;
+    objX.line = item.line;
+    objX.type = item.type;
+    objX.heap = jsheap;
+    obj.X = objX; // If we want to change the “X” identifier, just change this line.
     try {
       if (check_pred(pred, obj)){
           stepTo(i);
@@ -86,7 +87,7 @@ $('#text_condition').keypress(function(e){
 	}
 });
 
-$("#button_reach").click(button_reach_handler());
+$("#button_reach").click(button_reach_handler);