add No_externam_call ( = no Sbuiltin)

src/semantics/FPBigStepClight.v

@@ -334,6 +334,56 @@ Proof.
   by subst.
 Qed.
 
+(** ===================================================== *)
+(** Replacing the Axiom about deterministic external call *)
+(** ===================================================== *)
+
+
+(** No_external_call st state that st doesn't have any direct external call
+    e.i. there is no Sbuiltin.
+    However, Scall are alowed and i don't know if they might have
+    external call *)
+Inductive No_external_call : statement -> Prop :=
+  | NEC_Sskip : No_external_call Sskip
+  | NEC_Sassign : forall x v, No_external_call (Sassign x v)
+  | NEC_Sset : forall x v, No_external_call (Sset x v)
+  (** Scall might be dangerous ! *)
+  | NEC_Scall : forall i e le, No_external_call (Scall i e le)
+  (** No Sbuiltin
+    | NEC_Sbuiltin
+  *)
+  | NEC_Ssequence st1 st2 :
+      No_external_call st1 ->
+      No_external_call st2 ->
+        No_external_call (Ssequence st1 st2)
+  | NEC_Sifthenelse e st1 st2 :
+      No_external_call st1 ->
+      No_external_call st2 ->
+        No_external_call (Sifthenelse e st1 st2)
+  | NEC_Sloop st1 st2 :
+      No_external_call st1 ->
+      No_external_call st2 ->
+        No_external_call (Sloop st1 st2)
+  | NEC_Sbreak : No_external_call Sbreak
+  | NEC_Scontinue : No_external_call Scontinue
+  | NEC_Sreturn : forall e, No_external_call (Sreturn e)
+  | NEC_Sswitch : forall e lst, 
+      No_external_call_labeled lst ->
+        No_external_call (Sswitch e lst)
+  | NEC_Slabel : forall l st,
+      No_external_call st ->
+        No_external_call (Slabel l st)
+  | NEC_Sgoto : forall l, No_external_call (Sgoto l)
+
+with No_external_call_labeled : labeled_statements -> Type :=
+  | NECL_LSnil : No_external_call_labeled LSnil
+  | NECL_LScons : forall l st lst, 
+      No_external_call st ->
+      No_external_call_labeled lst ->
+        No_external_call_labeled (LScons l st lst).
+
+(** ===================================================== *)
+
 (** Axiom that external call are deterministic *)
 (** This axiom state that for every execution of external function from 
     a same memory state with the same argument, than it will produce the same trace*)