Fix example proof scripts that were broken by function renames (#955).

.github/ci.sh

@@ -170,7 +170,7 @@ install_system_deps() {
 test_dist() {
   find_java
   pushd intTests
-  for t in test0001 test0019_jss_switch_statement test_crucible_jvm test_ecdsa test_examples test_issue108 test_tutorial1 test_tutorial2 test_tutorial_w4; do echo $t >> disabled_tests.txt; done
+  for t in test0001 test0019_jss_switch_statement test_crucible_jvm test_ecdsa test_issue108 test_tutorial1 test_tutorial2 test_tutorial_w4; do echo $t >> disabled_tests.txt; done
   env
   LOUD=true ./runtests.sh
   sh -c "! grep '<failure>' results.xml"

examples/llvm/struct.saw

@@ -12,22 +12,22 @@ let ptr_to_fresh n ty = do {
 
 let set_spec = do {
     (x, px) <- ptr_to_fresh "x" (llvm_array 2 (llvm_int 32));
-    po <- alloc_init (llvm_struct "struct.s") (llvm_struct [px]);
+    po <- alloc_init (llvm_struct "struct.s") (llvm_struct_value [px]);
     llvm_execute_func [po];
-    llvm_points_to po (llvm_struct [px]);
+    llvm_points_to po (llvm_struct_value [px]);
     llvm_points_to px (llvm_term {{ [0, 0] : [2][32] }});
 };
 
 let add_spec = do {
     (x, px) <- ptr_to_fresh "x" (llvm_array 2 (llvm_int 32));
-    po <- alloc_init (llvm_struct "struct.s") (llvm_struct [px]);
+    po <- alloc_init (llvm_struct "struct.s") (llvm_struct_value [px]);
     llvm_execute_func [po];
     llvm_return (llvm_term {{ x@0 + x@1 }});
 };
 
 let id_spec = do {
     (x, px) <- ptr_to_fresh "x" (llvm_array 2 (llvm_int 32));
-    po <- alloc_init (llvm_struct "struct.s") (llvm_struct [px]);
+    po <- alloc_init (llvm_struct "struct.s") (llvm_struct_value [px]);
     llvm_execute_func [po];
     llvm_return po;
 };

examples/salsa20/salsa.saw

@@ -89,7 +89,7 @@ let s20_encrypt32 n = do {
 };
 
 let main : TopLevel () = do {
-    m      <- load_module "salsa20.bc";
+    m      <- llvm_load_module "salsa20.bc";
     qr     <- llvm_verify m "s20_quarterround" []      false quarterround_setup   abc;
     rr     <- llvm_verify m "s20_rowround"     [qr]    false rowround_setup       abc;
     cr     <- llvm_verify m "s20_columnround"  [qr]    false columnround_setup    abc;