Fixing Tests

test-suite/output/Extraction_ffi.ouf → test-suite/output/Extraction_ffi.out

@@ -5,14 +5,14 @@ external ax_fun: nat -> nat = "my_c_fun"
 (** val exact_fun : nat -> nat **)
 
 let exact_fun a =
-  add a (S O)
+  add (ax_fun a) (S O)
 (** User defined extraction *)
 (** val exact_fun : nat -> nat **)
 
 external exact_fun: nat -> nat = "my_exact_c_fun"
-(** User defined extraction *)
-(** val exact_fun : nat -> nat **)
+(** val exact_fun2 : nat -> nat **)
 
-let exact_fun = my_exact_c_fun
+let exact_fun2 a =
+  add (ax_fun a) (S O)
 
-let _ = Stdlib.Callback.register "call_exact_fun" exact_fun
+let _ = Stdlib.Callback.register "call_exact_fun" exact_fun2

test-suite/output/Extraction_ffi.v

@@ -5,21 +5,23 @@ From Coq Require Extraction.
 (* Define an axiomatic function. *)
 Axiom ax_fun : nat -> nat.
 
-(* Define a fully specified function *)
-Definition exact_fun (a : nat) := a + 1.
+(* Define a fully specified function*)
+Definition exact_fun (a : nat) := (ax_fun a) + 1.
+
+(* Define duplicate of the fully specified function*)
+Definition exact_fun2 (a : nat) := (ax_fun a) + 1.
 
 (* ax_fun shall be a FFI call to the C function my_c_fun *)
 Extract Foreign Constant ax_fun => "my_c_fun".
 Extraction ax_fun.
 
-(* Extract the defined exact_fun *)
+(* Extract exact_fun *)
 Extraction exact_fun.
 
 (* exact_fun shall now be a FFI call to the C function my_c_fun *)
 Extract Foreign Constant exact_fun => "my_exact_c_fun".
 Extraction exact_fun.
 
-(* Now, exact_fun is an entry point exposed to C *)
-Reset Extraction Foreign.
-Extract Callback "call_exact_fun" exact_fun.
-Extraction exact_fun.
+(* Now, exact_fun is an entry point exposed to C. *)
+Extract Callback "call_exact_fun" exact_fun2.
+Extraction exact_fun2.