From f1ea5b8dbaefb83e3d4db966068cee4e3bd1649e Mon Sep 17 00:00:00 2001
From: Mario Frank <mario.frank@uni-potsdam.de>
Date: Tue, 14 Nov 2023 15:25:22 +0100
Subject: [PATCH] Extend the tests: 1) Make sure that extraction to JSON fails
 2) Make sure that extracting callbacks can be reverted.

---
 test-suite/failure/extraction_ffi.v  | 7 ++++++-
 test-suite/output/Extraction_ffi.out | 4 ++++
 test-suite/output/Extraction_ffi.v   | 6 +++++-
 3 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/test-suite/failure/extraction_ffi.v b/test-suite/failure/extraction_ffi.v
index c86ffb49ef0d3..f4b0c7eb48346 100644
--- a/test-suite/failure/extraction_ffi.v
+++ b/test-suite/failure/extraction_ffi.v
@@ -21,7 +21,12 @@ Extraction Language Scheme.
 Fail Extract Foreign Constant ax_fun => "my_c_fun".
 Fail Extract Callback "call_my_fun" my_fun.
 
+(* Extraction of foreign constant and callback for JSON must fail *)
+Extraction Language JSON.
+Fail Extract Foreign Constant ax_fun => "my_c_fun".
+Fail Extract Callback "call_my_fun" my_fun.
+
 (* Extraction of foreign constant for already defined ml function must fail. *)
 Extraction Language OCaml.
 Extract Constant ax_fun => "my_ml_fun".
-Fail Extract Foreign Constant ax_fun => "my_c_fun".
\ No newline at end of file
+Fail Extract Foreign Constant ax_fun => "my_c_fun".
diff --git a/test-suite/output/Extraction_ffi.out b/test-suite/output/Extraction_ffi.out
index b7f22c4f2372f..b4325bd171e75 100644
--- a/test-suite/output/Extraction_ffi.out
+++ b/test-suite/output/Extraction_ffi.out
@@ -16,3 +16,7 @@ let exact_fun2 a =
   add (ax_fun a) (S O)
 
 let _ = Stdlib.Callback.register "call_exact_fun" exact_fun2
+(** val exact_fun2 : nat -> nat **)
+
+let exact_fun2 a =
+  add (ax_fun a) (S O)
diff --git a/test-suite/output/Extraction_ffi.v b/test-suite/output/Extraction_ffi.v
index 68b8eaa735d6f..7349bf3192a23 100644
--- a/test-suite/output/Extraction_ffi.v
+++ b/test-suite/output/Extraction_ffi.v
@@ -22,6 +22,10 @@ Extraction exact_fun.
 Extract Foreign Constant exact_fun => "my_exact_c_fun".
 Extraction exact_fun.
 
-(* Now, exact_fun is an entry point exposed to C. *)
+(* Now, exact_fun is an entry point exposed to C *)
 Extract Callback "call_exact_fun" exact_fun2.
 Extraction exact_fun2.
+
+(* Now we make sure that a callback registration can be reverted *)
+Reset Extraction Callback.
+Extraction exact_fun2.