Changeset 2831 for extracted

Timestamp:

Mar 8, 2013, 11:38:27 PM (8 years ago)

Author:

sacerdot

Message:

...

File:

• extracted/joint_LTL_LIN_semantics.ml (modified) (2 diffs)

extracted/joint_LTL_LIN_semantics.ml

@@ -252 +252 @@
     Joint_semantics.setup_call = (fun x x0 x1 st ->
     Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st));
-    Joint_semantics.fetch_external_args = (assert false (* absurd case *));
+    Joint_semantics.fetch_external_args = (fun x -> assert false (* absurd case *));
     Joint_semantics.set_result = (Obj.magic ltl_lin_set_result);
     Joint_semantics.call_args_for_main = (Obj.magic Nat.O);
@@ -261 +261 @@
         (List.map
           (SemanticsUtils.hwreg_retrieve (Obj.magic st.Joint_semantics.regs))
-          I8051.registerRets))); Joint_semantics.eval_ext_seq = (assert false
+          I8051.registerRets))); Joint_semantics.eval_ext_seq = (fun x -> assert false
     (* absurd case *)); Joint_semantics.pop_frame = (fun x x0 x1 x2 st ->
     Joint_semantics.pop_ra lTL_LIN_state st) }