update a few more installed in examples/ for shared memory

CakeML · Mar 11, 2024 · e61fd9a · e61fd9a
1 parent 11a2259
commit e61fd9a
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/examples/pseudo_bool/array/compilation/proofs/cnfProofScript.sml b/examples/pseudo_bool/array/compilation/proofs/cnfProofScript.sml
@@ -47,7 +47,8 @@ val installed_x64_def = Define `
         code cbspace
         data data_sp
         cfg.lab_conf.ffi_names
-        (heap_regs x64_backend_config.stack_conf.reg_names) mc ms
+        (heap_regs x64_backend_config.stack_conf.reg_names) mc
+        cfg.lab_conf.shmem_extra ms
     `;
 
 val cake_pb_cnf_code_def = Define `

diff --git a/examples/xlrup_checker/array/compilation/proofs/xlrupProofScript.sml b/examples/xlrup_checker/array/compilation/proofs/xlrupProofScript.sml
@@ -47,7 +47,8 @@ val installed_x64_def = Define `
         code cbspace
         data data_sp
         cfg.lab_conf.ffi_names
-        (heap_regs x64_backend_config.stack_conf.reg_names) mc ms
+        (heap_regs x64_backend_config.stack_conf.reg_names) mc
+        cfg.lab_conf.shmem_extra ms
     `;
 
 val cake_xlrup_code_def = Define `