Update notations

src/semantics/FPEnvironmentClight.v

@@ -116,7 +116,7 @@ Module OUT_TO_TRACE.
     | None => func
     end.
 
-  Definition code_event_optassign (optvar: option c_code)
+  Definition code_event_optssgn (optvar: option c_code)
                                           (func: c_code)
                                           (optparams: option (list c_code)): event :=
     let call := (call_optparams func optparams) in

src/verification/ClightLemmas.v

@@ -201,7 +201,7 @@ Axiom step_arbitrary_call_gen:
       (State f
         (Scall optid (Evar ##func (Tfunction ltypes tres cc_default)) e_p)
           k e le m)
-          [:: (code_event_optassign optvar func optparams)]
+          [:: (code_event_optssgn optvar func optparams)]
       (State f Sskip k e le m).
 
 Lemma exec_arbitrary_call_gen:
@@ -214,7 +214,7 @@ Lemma exec_arbitrary_call_gen:
       (State f
         (Scall optid (Evar ##func (Tfunction ltypes tres cc_default)) e_p)
           k e le m)
-          [:: (code_event_optassign optvar func optparams)]
+          [:: (code_event_optssgn optvar func optparams)]
       (State f Sskip k e le m).
 Proof.
   intros; apply Smallstep.star_one.
@@ -257,7 +257,7 @@ Lemma exec_arbitrary_fun_call:
 Proof.
   move => ge f func k e le m tres ltypes e_p params H.
   replace (code_event _ )
-    with (code_event_optassign None func (Some params)).
+    with (code_event_optssgn None func (Some params)).
   apply (exec_arbitrary_call_gen ge f func k e le m).
   - apply (match_optparams_impl_params H).
   - by right.
@@ -278,7 +278,7 @@ Lemma exec_arbitrary_fun_call_res:
 Proof.
   move => ge f func k e le m tres ltypes e_p params var Hr Hp.
   replace (code_event_assign _ _)
-    with (code_event_optassign (Some var) func (Some params)).
+    with (code_event_optssgn (Some var) func (Some params)).
   apply exec_arbitrary_call_gen; try by [].
   - apply (match_optparams_impl_params Hp).
   - left. by exists var.
@@ -294,7 +294,7 @@ Axiom step_arbitrary_assign_C_code:
   -> step2 ge
       (State f (Sassign (Evar #var type) expr)
           k e le m)
-          [:: (code_event_optassign (Some var) value None)]
+          [:: (code_event_optssgn (Some var) value None)]
       (State f Sskip k e le m).
 
 Lemma exec_arbitrary_assign_C_code:
@@ -303,7 +303,7 @@ Lemma exec_arbitrary_assign_C_code:
   -> Smallstep.star step2 ge
       (State f (Sassign (Evar #var type) expr)
           k e le m)
-          [:: (code_event_optassign (Some var) value None)]
+          [:: (code_event_optssgn (Some var) value None)]
       (State f Sskip k e le m).
 Proof.
   intros. apply Smallstep.star_one.
@@ -336,7 +336,7 @@ Lemma eq_exec_assign_time:
 Proof.
   move => ge f k e le m.
   replace (fp_trace_to_trace [:: reset_time])
-    with [::(code_event_optassign (Some block_time_str)
+    with [::(code_event_optssgn (Some block_time_str)
                                         (string_of_nat 0) None)].
   apply exec_arbitrary_assign_C_code.
   - rewrite //= /cast_possible; split; try by []; try right.

src/verification/FPNavigationModeVerification.v

@@ -234,7 +234,7 @@ forall ps pm pc stmt_cond wp (ge: genv) f k e le m,
 Proof.
   move => ps pm pc stmt_cond wp ge f k e le m Hn.
   replace (fp_trace_to_trace [:: C_CODE _])
-    with [::(code_event_optassign (Some last_wp_var_str)
+    with [::(code_event_optssgn (Some last_wp_var_str)
                                         (string_of_nat wp) None)].
   apply exec_arbitrary_assign_C_code.
   - simpl_eqparam_ex wp.

src/verification/VerifFPToFPC.v

@@ -136,4 +136,6 @@ Section FLIGHT_PLAN.
 
 End FLIGHT_PLAN.
 
+Print Assumptions semantic_preservation.
+
 End FP_TO_C_VERIF.