update talk demo

5461c895 · Michael Sammler · 8e7a73c2 · 5461c895 · 5461c895 · 5461c895
Commit 5461c895 authored May 25, 2021 by Michael Sammler
--- a/examples/proofs/talk_demo1/generated_code.v
+++ b/examples/proofs/talk_demo1/generated_code.v
@@ -32,56 +32,56 @@ Section code.
  Definition loc_25 : location_info := LocationInfo file_0 12 6 12 7.
  Definition loc_26 : location_info := LocationInfo file_0 12 6 12 7.
  Definition loc_27 : location_info := LocationInfo file_0 12 11 12 25.
-  Definition loc_30 : location_info := LocationInfo file_0 21 2 21 61.
-  Definition loc_31 : location_info := LocationInfo file_0 22 2 22 17.
-  Definition loc_32 : location_info := LocationInfo file_0 22 18 22 47.
-  Definition loc_33 : location_info := LocationInfo file_0 23 2 23 61.
-  Definition loc_34 : location_info := LocationInfo file_0 24 2 24 17.
-  Definition loc_35 : location_info := LocationInfo file_0 24 18 24 47.
-  Definition loc_36 : location_info := LocationInfo file_0 25 2 25 24.
-  Definition loc_37 : location_info := LocationInfo file_0 26 2 28 3.
-  Definition loc_38 : location_info := LocationInfo file_0 26 30 28 3.
-  Definition loc_39 : location_info := LocationInfo file_0 27 4 27 28.
-  Definition loc_40 : location_info := LocationInfo file_0 27 11 27 26.
-  Definition loc_41 : location_info := LocationInfo file_0 27 11 27 21.
-  Definition loc_42 : location_info := LocationInfo file_0 27 11 27 21.
-  Definition loc_43 : location_info := LocationInfo file_0 27 11 27 16.
-  Definition loc_44 : location_info := LocationInfo file_0 27 11 27 16.
-  Definition loc_45 : location_info := LocationInfo file_0 27 25 27 26.
-  Definition loc_47 : location_info := LocationInfo file_0 26 5 26 28.
-  Definition loc_48 : location_info := LocationInfo file_0 26 5 26 10.
-  Definition loc_49 : location_info := LocationInfo file_0 26 5 26 10.
-  Definition loc_50 : location_info := LocationInfo file_0 26 14 26 28.
-  Definition loc_51 : location_info := LocationInfo file_0 25 2 25 8.
-  Definition loc_52 : location_info := LocationInfo file_0 25 2 25 8.
-  Definition loc_53 : location_info := LocationInfo file_0 25 9 25 15.
-  Definition loc_54 : location_info := LocationInfo file_0 25 10 25 15.
-  Definition loc_55 : location_info := LocationInfo file_0 25 17 25 22.
-  Definition loc_56 : location_info := LocationInfo file_0 25 17 25 22.
-  Definition loc_57 : location_info := LocationInfo file_0 24 18 24 29.
-  Definition loc_58 : location_info := LocationInfo file_0 24 18 24 23.
-  Definition loc_59 : location_info := LocationInfo file_0 24 18 24 23.
-  Definition loc_60 : location_info := LocationInfo file_0 24 32 24 46.
-  Definition loc_61 : location_info := LocationInfo file_0 24 2 24 12.
-  Definition loc_62 : location_info := LocationInfo file_0 24 2 24 7.
-  Definition loc_63 : location_info := LocationInfo file_0 24 2 24 7.
-  Definition loc_64 : location_info := LocationInfo file_0 24 15 24 16.
-  Definition loc_65 : location_info := LocationInfo file_0 23 29 23 60.
-  Definition loc_66 : location_info := LocationInfo file_0 23 29 23 34.
-  Definition loc_67 : location_info := LocationInfo file_0 23 29 23 34.
-  Definition loc_68 : location_info := LocationInfo file_0 23 35 23 59.
-  Definition loc_71 : location_info := LocationInfo file_0 22 18 22 29.
-  Definition loc_72 : location_info := LocationInfo file_0 22 18 22 23.
-  Definition loc_73 : location_info := LocationInfo file_0 22 18 22 23.
-  Definition loc_74 : location_info := LocationInfo file_0 22 32 22 46.
-  Definition loc_75 : location_info := LocationInfo file_0 22 2 22 12.
-  Definition loc_76 : location_info := LocationInfo file_0 22 2 22 7.
-  Definition loc_77 : location_info := LocationInfo file_0 22 2 22 7.
-  Definition loc_78 : location_info := LocationInfo file_0 22 15 22 16.
-  Definition loc_79 : location_info := LocationInfo file_0 21 29 21 60.
-  Definition loc_80 : location_info := LocationInfo file_0 21 29 21 34.
-  Definition loc_81 : location_info := LocationInfo file_0 21 29 21 34.
-  Definition loc_82 : location_info := LocationInfo file_0 21 35 21 59.
+  Definition loc_30 : location_info := LocationInfo file_0 20 2 20 61.
+  Definition loc_31 : location_info := LocationInfo file_0 21 2 21 17.
+  Definition loc_32 : location_info := LocationInfo file_0 21 18 21 47.
+  Definition loc_33 : location_info := LocationInfo file_0 22 2 22 61.
+  Definition loc_34 : location_info := LocationInfo file_0 23 2 23 17.
+  Definition loc_35 : location_info := LocationInfo file_0 23 18 23 47.
+  Definition loc_36 : location_info := LocationInfo file_0 24 2 24 24.
+  Definition loc_37 : location_info := LocationInfo file_0 25 2 27 3.
+  Definition loc_38 : location_info := LocationInfo file_0 25 30 27 3.
+  Definition loc_39 : location_info := LocationInfo file_0 26 4 26 28.
+  Definition loc_40 : location_info := LocationInfo file_0 26 11 26 26.
+  Definition loc_41 : location_info := LocationInfo file_0 26 11 26 21.
+  Definition loc_42 : location_info := LocationInfo file_0 26 11 26 21.
+  Definition loc_43 : location_info := LocationInfo file_0 26 11 26 16.
+  Definition loc_44 : location_info := LocationInfo file_0 26 11 26 16.
+  Definition loc_45 : location_info := LocationInfo file_0 26 25 26 26.
+  Definition loc_47 : location_info := LocationInfo file_0 25 5 25 28.
+  Definition loc_48 : location_info := LocationInfo file_0 25 5 25 10.
+  Definition loc_49 : location_info := LocationInfo file_0 25 5 25 10.
+  Definition loc_50 : location_info := LocationInfo file_0 25 14 25 28.
+  Definition loc_51 : location_info := LocationInfo file_0 24 2 24 8.
+  Definition loc_52 : location_info := LocationInfo file_0 24 2 24 8.
+  Definition loc_53 : location_info := LocationInfo file_0 24 9 24 15.
+  Definition loc_54 : location_info := LocationInfo file_0 24 10 24 15.
+  Definition loc_55 : location_info := LocationInfo file_0 24 17 24 22.
+  Definition loc_56 : location_info := LocationInfo file_0 24 17 24 22.
+  Definition loc_57 : location_info := LocationInfo file_0 23 18 23 29.
+  Definition loc_58 : location_info := LocationInfo file_0 23 18 23 23.
+  Definition loc_59 : location_info := LocationInfo file_0 23 18 23 23.
+  Definition loc_60 : location_info := LocationInfo file_0 23 32 23 46.
+  Definition loc_61 : location_info := LocationInfo file_0 23 2 23 12.
+  Definition loc_62 : location_info := LocationInfo file_0 23 2 23 7.
+  Definition loc_63 : location_info := LocationInfo file_0 23 2 23 7.
+  Definition loc_64 : location_info := LocationInfo file_0 23 15 23 16.
+  Definition loc_65 : location_info := LocationInfo file_0 22 29 22 60.
+  Definition loc_66 : location_info := LocationInfo file_0 22 29 22 34.
+  Definition loc_67 : location_info := LocationInfo file_0 22 29 22 34.
+  Definition loc_68 : location_info := LocationInfo file_0 22 35 22 59.
+  Definition loc_71 : location_info := LocationInfo file_0 21 18 21 29.
+  Definition loc_72 : location_info := LocationInfo file_0 21 18 21 23.
+  Definition loc_73 : location_info := LocationInfo file_0 21 18 21 23.
+  Definition loc_74 : location_info := LocationInfo file_0 21 32 21 46.
+  Definition loc_75 : location_info := LocationInfo file_0 21 2 21 12.
+  Definition loc_76 : location_info := LocationInfo file_0 21 2 21 7.
+  Definition loc_77 : location_info := LocationInfo file_0 21 2 21 7.
+  Definition loc_78 : location_info := LocationInfo file_0 21 15 21 16.
+  Definition loc_79 : location_info := LocationInfo file_0 20 29 20 60.
+  Definition loc_80 : location_info := LocationInfo file_0 20 29 20 34.
+  Definition loc_81 : location_info := LocationInfo file_0 20 29 20 34.
+  Definition loc_82 : location_info := LocationInfo file_0 20 35 20 59.

  (* Definition of struct [list_node]. *)
  Program Definition struct_list_node := {|

--- a/examples/proofs/talk_demo2/generated_code.v
+++ b/examples/proofs/talk_demo2/generated_code.v
@@ -41,47 +41,40 @@ Section code.
  Definition loc_36 : location_info := LocationInfo file_0 29 2 29 24.
  Definition loc_37 : location_info := LocationInfo file_0 30 2 32 3.
  Definition loc_38 : location_info := LocationInfo file_0 30 30 32 3.
-  Definition loc_39 : location_info := LocationInfo file_0 31 4 31 28.
-  Definition loc_40 : location_info := LocationInfo file_0 31 11 31 26.
-  Definition loc_41 : location_info := LocationInfo file_0 31 11 31 21.
-  Definition loc_42 : location_info := LocationInfo file_0 31 11 31 21.
-  Definition loc_43 : location_info := LocationInfo file_0 31 11 31 16.
-  Definition loc_44 : location_info := LocationInfo file_0 31 11 31 16.
-  Definition loc_45 : location_info := LocationInfo file_0 31 25 31 26.
-  Definition loc_47 : location_info := LocationInfo file_0 30 5 30 28.
-  Definition loc_48 : location_info := LocationInfo file_0 30 5 30 10.
-  Definition loc_49 : location_info := LocationInfo file_0 30 5 30 10.
-  Definition loc_50 : location_info := LocationInfo file_0 30 14 30 28.
-  Definition loc_51 : location_info := LocationInfo file_0 29 2 29 8.
-  Definition loc_52 : location_info := LocationInfo file_0 29 2 29 8.
-  Definition loc_53 : location_info := LocationInfo file_0 29 9 29 15.
-  Definition loc_54 : location_info := LocationInfo file_0 29 10 29 15.
-  Definition loc_55 : location_info := LocationInfo file_0 29 17 29 22.
-  Definition loc_56 : location_info := LocationInfo file_0 29 17 29 22.
-  Definition loc_57 : location_info := LocationInfo file_0 28 18 28 29.
-  Definition loc_58 : location_info := LocationInfo file_0 28 18 28 23.
-  Definition loc_59 : location_info := LocationInfo file_0 28 18 28 23.
-  Definition loc_60 : location_info := LocationInfo file_0 28 32 28 46.
-  Definition loc_61 : location_info := LocationInfo file_0 28 2 28 12.
-  Definition loc_62 : location_info := LocationInfo file_0 28 2 28 7.
-  Definition loc_63 : location_info := LocationInfo file_0 28 2 28 7.
-  Definition loc_64 : location_info := LocationInfo file_0 28 15 28 16.
-  Definition loc_65 : location_info := LocationInfo file_0 27 29 27 60.
-  Definition loc_66 : location_info := LocationInfo file_0 27 29 27 34.
-  Definition loc_67 : location_info := LocationInfo file_0 27 29 27 34.
-  Definition loc_68 : location_info := LocationInfo file_0 27 35 27 59.
-  Definition loc_71 : location_info := LocationInfo file_0 26 18 26 29.
-  Definition loc_72 : location_info := LocationInfo file_0 26 18 26 23.
-  Definition loc_73 : location_info := LocationInfo file_0 26 18 26 23.
-  Definition loc_74 : location_info := LocationInfo file_0 26 32 26 46.
-  Definition loc_75 : location_info := LocationInfo file_0 26 2 26 12.
-  Definition loc_76 : location_info := LocationInfo file_0 26 2 26 7.
-  Definition loc_77 : location_info := LocationInfo file_0 26 2 26 7.
-  Definition loc_78 : location_info := LocationInfo file_0 26 15 26 16.
-  Definition loc_79 : location_info := LocationInfo file_0 25 29 25 60.
-  Definition loc_80 : location_info := LocationInfo file_0 25 29 25 34.
-  Definition loc_81 : location_info := LocationInfo file_0 25 29 25 34.
-  Definition loc_82 : location_info := LocationInfo file_0 25 35 25 59.
+  Definition loc_40 : location_info := LocationInfo file_0 30 5 30 28.
+  Definition loc_41 : location_info := LocationInfo file_0 30 5 30 10.
+  Definition loc_42 : location_info := LocationInfo file_0 30 5 30 10.
+  Definition loc_43 : location_info := LocationInfo file_0 30 14 30 28.
+  Definition loc_44 : location_info := LocationInfo file_0 29 2 29 8.
+  Definition loc_45 : location_info := LocationInfo file_0 29 2 29 8.
+  Definition loc_46 : location_info := LocationInfo file_0 29 9 29 15.
+  Definition loc_47 : location_info := LocationInfo file_0 29 10 29 15.
+  Definition loc_48 : location_info := LocationInfo file_0 29 17 29 22.
+  Definition loc_49 : location_info := LocationInfo file_0 29 17 29 22.
+  Definition loc_50 : location_info := LocationInfo file_0 28 18 28 29.
+  Definition loc_51 : location_info := LocationInfo file_0 28 18 28 23.
+  Definition loc_52 : location_info := LocationInfo file_0 28 18 28 23.
+  Definition loc_53 : location_info := LocationInfo file_0 28 32 28 46.
+  Definition loc_54 : location_info := LocationInfo file_0 28 2 28 12.
+  Definition loc_55 : location_info := LocationInfo file_0 28 2 28 7.
+  Definition loc_56 : location_info := LocationInfo file_0 28 2 28 7.
+  Definition loc_57 : location_info := LocationInfo file_0 28 15 28 16.
+  Definition loc_58 : location_info := LocationInfo file_0 27 29 27 60.
+  Definition loc_59 : location_info := LocationInfo file_0 27 29 27 34.
+  Definition loc_60 : location_info := LocationInfo file_0 27 29 27 34.
+  Definition loc_61 : location_info := LocationInfo file_0 27 35 27 59.
+  Definition loc_64 : location_info := LocationInfo file_0 26 18 26 29.
+  Definition loc_65 : location_info := LocationInfo file_0 26 18 26 23.
+  Definition loc_66 : location_info := LocationInfo file_0 26 18 26 23.
+  Definition loc_67 : location_info := LocationInfo file_0 26 32 26 46.
+  Definition loc_68 : location_info := LocationInfo file_0 26 2 26 12.
+  Definition loc_69 : location_info := LocationInfo file_0 26 2 26 7.
+  Definition loc_70 : location_info := LocationInfo file_0 26 2 26 7.
+  Definition loc_71 : location_info := LocationInfo file_0 26 15 26 16.
+  Definition loc_72 : location_info := LocationInfo file_0 25 29 25 60.
+  Definition loc_73 : location_info := LocationInfo file_0 25 29 25 34.
+  Definition loc_74 : location_info := LocationInfo file_0 25 29 25 34.
+  Definition loc_75 : location_info := LocationInfo file_0 25 35 25 59.

  (* Definition of struct [list_node]. *)
  Program Definition struct_list_node := {|
@@ -140,35 +133,32 @@ Section code.
    f_code := (
      <[ "#0" :=
        "node1" <-{ void* }
-          LocInfoE loc_79 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_79 (Call (LocInfoE loc_81 (global_alloc)) [@{expr} LocInfoE loc_82 (i2v (layout_of struct_list_node).(ly_size) size_t) ]))) ;
+          LocInfoE loc_72 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_72 (Call (LocInfoE loc_74 (global_alloc)) [@{expr} LocInfoE loc_75 (i2v (layout_of struct_list_node).(ly_size) size_t) ]))) ;
        locinfo: loc_31 ;
-        LocInfoE loc_75 ((LocInfoE loc_76 (!{void*} (LocInfoE loc_77 ("node1")))) at{struct_list_node} "val") <-{ it_layout i32 }
-          LocInfoE loc_78 (i2v 1 i32) ;
+        LocInfoE loc_68 ((LocInfoE loc_69 (!{void*} (LocInfoE loc_70 ("node1")))) at{struct_list_node} "val") <-{ it_layout i32 }
+          LocInfoE loc_71 (i2v 1 i32) ;
        locinfo: loc_32 ;
-        LocInfoE loc_71 ((LocInfoE loc_72 (!{void*} (LocInfoE loc_73 ("node1")))) at{struct_list_node} "next") <-{ void* }
-          LocInfoE loc_74 (NULL) ;
+        LocInfoE loc_64 ((LocInfoE loc_65 (!{void*} (LocInfoE loc_66 ("node1")))) at{struct_list_node} "next") <-{ void* }
+          LocInfoE loc_67 (NULL) ;
        "node2" <-{ void* }
-          LocInfoE loc_65 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_65 (Call (LocInfoE loc_67 (global_alloc)) [@{expr} LocInfoE loc_68 (i2v (layout_of struct_list_node).(ly_size) size_t) ]))) ;
+          LocInfoE loc_58 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_58 (Call (LocInfoE loc_60 (global_alloc)) [@{expr} LocInfoE loc_61 (i2v (layout_of struct_list_node).(ly_size) size_t) ]))) ;
        locinfo: loc_34 ;
-        LocInfoE loc_61 ((LocInfoE loc_62 (!{void*} (LocInfoE loc_63 ("node2")))) at{struct_list_node} "val") <-{ it_layout i32 }
-          LocInfoE loc_64 (i2v 2 i32) ;
+        LocInfoE loc_54 ((LocInfoE loc_55 (!{void*} (LocInfoE loc_56 ("node2")))) at{struct_list_node} "val") <-{ it_layout i32 }
+          LocInfoE loc_57 (i2v 2 i32) ;
        locinfo: loc_35 ;
-        LocInfoE loc_57 ((LocInfoE loc_58 (!{void*} (LocInfoE loc_59 ("node2")))) at{struct_list_node} "next") <-{ void* }
-          LocInfoE loc_60 (NULL) ;
+        LocInfoE loc_50 ((LocInfoE loc_51 (!{void*} (LocInfoE loc_52 ("node2")))) at{struct_list_node} "next") <-{ void* }
+          LocInfoE loc_53 (NULL) ;
        locinfo: loc_36 ;
-        expr: (LocInfoE loc_36 (Call (LocInfoE loc_52 (global_append)) [@{expr} LocInfoE loc_53 (&(LocInfoE loc_54 ("node1"))) ;
-        LocInfoE loc_55 (use{void*} (LocInfoE loc_56 ("node2"))) ])) ;
-        locinfo: loc_47 ;
-        if: LocInfoE loc_47 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_47 ((LocInfoE loc_48 (use{void*} (LocInfoE loc_49 ("node1")))) !={PtrOp, PtrOp} (LocInfoE loc_50 (NULL)))))
+        expr: (LocInfoE loc_36 (Call (LocInfoE loc_45 (global_append)) [@{expr} LocInfoE loc_46 (&(LocInfoE loc_47 ("node1"))) ;
+        LocInfoE loc_48 (use{void*} (LocInfoE loc_49 ("node2"))) ])) ;
+        locinfo: loc_40 ;
+        if: LocInfoE loc_40 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_40 ((LocInfoE loc_41 (use{void*} (LocInfoE loc_42 ("node1")))) !={PtrOp, PtrOp} (LocInfoE loc_43 (NULL)))))
        then
-        locinfo: loc_39 ;
        Goto "#1"
        else
        Goto "#2"
      ]> $
      <[ "#1" :=
-        locinfo: loc_39 ;
-        assert: (LocInfoE loc_40 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_40 ((LocInfoE loc_41 (use{it_layout i32} (LocInfoE loc_42 ((LocInfoE loc_43 (!{void*} (LocInfoE loc_44 ("node1")))) at{struct_list_node} "val")))) ={IntOp i32, IntOp i32} (LocInfoE loc_45 (i2v 1 i32)))))) ;
        Return (VOID)
      ]> $
      <[ "#2" :=

--- a/examples/proofs/talk_demo3/generated_code.v
+++ b/examples/proofs/talk_demo3/generated_code.v
@@ -41,47 +41,40 @@ Section code.
  Definition loc_36 : location_info := LocationInfo file_0 34 2 34 24.
  Definition loc_37 : location_info := LocationInfo file_0 35 2 37 3.
  Definition loc_38 : location_info := LocationInfo file_0 35 30 37 3.
-  Definition loc_39 : location_info := LocationInfo file_0 36 4 36 28.
-  Definition loc_40 : location_info := LocationInfo file_0 36 11 36 26.
-  Definition loc_41 : location_info := LocationInfo file_0 36 11 36 21.
-  Definition loc_42 : location_info := LocationInfo file_0 36 11 36 21.
-  Definition loc_43 : location_info := LocationInfo file_0 36 11 36 16.
-  Definition loc_44 : location_info := LocationInfo file_0 36 11 36 16.
-  Definition loc_45 : location_info := LocationInfo file_0 36 25 36 26.
-  Definition loc_47 : location_info := LocationInfo file_0 35 5 35 28.
-  Definition loc_48 : location_info := LocationInfo file_0 35 5 35 10.
-  Definition loc_49 : location_info := LocationInfo file_0 35 5 35 10.
-  Definition loc_50 : location_info := LocationInfo file_0 35 14 35 28.
-  Definition loc_51 : location_info := LocationInfo file_0 34 2 34 8.
-  Definition loc_52 : location_info := LocationInfo file_0 34 2 34 8.
-  Definition loc_53 : location_info := LocationInfo file_0 34 9 34 15.
-  Definition loc_54 : location_info := LocationInfo file_0 34 10 34 15.
-  Definition loc_55 : location_info := LocationInfo file_0 34 17 34 22.
-  Definition loc_56 : location_info := LocationInfo file_0 34 17 34 22.
-  Definition loc_57 : location_info := LocationInfo file_0 33 18 33 29.
-  Definition loc_58 : location_info := LocationInfo file_0 33 18 33 23.
-  Definition loc_59 : location_info := LocationInfo file_0 33 18 33 23.
-  Definition loc_60 : location_info := LocationInfo file_0 33 32 33 46.
-  Definition loc_61 : location_info := LocationInfo file_0 33 2 33 12.
-  Definition loc_62 : location_info := LocationInfo file_0 33 2 33 7.
-  Definition loc_63 : location_info := LocationInfo file_0 33 2 33 7.
-  Definition loc_64 : location_info := LocationInfo file_0 33 15 33 16.
-  Definition loc_65 : location_info := LocationInfo file_0 32 29 32 60.
-  Definition loc_66 : location_info := LocationInfo file_0 32 29 32 34.
-  Definition loc_67 : location_info := LocationInfo file_0 32 29 32 34.
-  Definition loc_68 : location_info := LocationInfo file_0 32 35 32 59.
-  Definition loc_71 : location_info := LocationInfo file_0 31 18 31 29.
-  Definition loc_72 : location_info := LocationInfo file_0 31 18 31 23.
-  Definition loc_73 : location_info := LocationInfo file_0 31 18 31 23.
-  Definition loc_74 : location_info := LocationInfo file_0 31 32 31 46.
-  Definition loc_75 : location_info := LocationInfo file_0 31 2 31 12.
-  Definition loc_76 : location_info := LocationInfo file_0 31 2 31 7.
-  Definition loc_77 : location_info := LocationInfo file_0 31 2 31 7.
-  Definition loc_78 : location_info := LocationInfo file_0 31 15 31 16.
-  Definition loc_79 : location_info := LocationInfo file_0 30 29 30 60.
-  Definition loc_80 : location_info := LocationInfo file_0 30 29 30 34.
-  Definition loc_81 : location_info := LocationInfo file_0 30 29 30 34.
-  Definition loc_82 : location_info := LocationInfo file_0 30 35 30 59.
+  Definition loc_40 : location_info := LocationInfo file_0 35 5 35 28.
+  Definition loc_41 : location_info := LocationInfo file_0 35 5 35 10.
+  Definition loc_42 : location_info := LocationInfo file_0 35 5 35 10.
+  Definition loc_43 : location_info := LocationInfo file_0 35 14 35 28.
+  Definition loc_44 : location_info := LocationInfo file_0 34 2 34 8.
+  Definition loc_45 : location_info := LocationInfo file_0 34 2 34 8.
+  Definition loc_46 : location_info := LocationInfo file_0 34 9 34 15.
+  Definition loc_47 : location_info := LocationInfo file_0 34 10 34 15.
+  Definition loc_48 : location_info := LocationInfo file_0 34 17 34 22.
+  Definition loc_49 : location_info := LocationInfo file_0 34 17 34 22.
+  Definition loc_50 : location_info := LocationInfo file_0 33 18 33 29.
+  Definition loc_51 : location_info := LocationInfo file_0 33 18 33 23.
+  Definition loc_52 : location_info := LocationInfo file_0 33 18 33 23.
+  Definition loc_53 : location_info := LocationInfo file_0 33 32 33 46.
+  Definition loc_54 : location_info := LocationInfo file_0 33 2 33 12.
+  Definition loc_55 : location_info := LocationInfo file_0 33 2 33 7.
+  Definition loc_56 : location_info := LocationInfo file_0 33 2 33 7.
+  Definition loc_57 : location_info := LocationInfo file_0 33 15 33 16.
+  Definition loc_58 : location_info := LocationInfo file_0 32 29 32 60.
+  Definition loc_59 : location_info := LocationInfo file_0 32 29 32 34.
+  Definition loc_60 : location_info := LocationInfo file_0 32 29 32 34.
+  Definition loc_61 : location_info := LocationInfo file_0 32 35 32 59.
+  Definition loc_64 : location_info := LocationInfo file_0 31 18 31 29.
+  Definition loc_65 : location_info := LocationInfo file_0 31 18 31 23.
+  Definition loc_66 : location_info := LocationInfo file_0 31 18 31 23.
+  Definition loc_67 : location_info := LocationInfo file_0 31 32 31 46.
+  Definition loc_68 : location_info := LocationInfo file_0 31 2 31 12.
+  Definition loc_69 : location_info := LocationInfo file_0 31 2 31 7.
+  Definition loc_70 : location_info := LocationInfo file_0 31 2 31 7.
+  Definition loc_71 : location_info := LocationInfo file_0 31 15 31 16.
+  Definition loc_72 : location_info := LocationInfo file_0 30 29 30 60.
+  Definition loc_73 : location_info := LocationInfo file_0 30 29 30 34.
+  Definition loc_74 : location_info := LocationInfo file_0 30 29 30 34.
+  Definition loc_75 : location_info := LocationInfo file_0 30 35 30 59.

  (* Definition of struct [list_node]. *)
  Program Definition struct_list_node := {|
@@ -140,35 +133,32 @@ Section code.
    f_code := (
      <[ "#0" :=
        "node1" <-{ void* }
-          LocInfoE loc_79 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_79 (Call (LocInfoE loc_81 (global_alloc)) [@{expr} LocInfoE loc_82 (i2v (layout_of struct_list_node).(ly_size) size_t) ]))) ;
+          LocInfoE loc_72 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_72 (Call (LocInfoE loc_74 (global_alloc)) [@{expr} LocInfoE loc_75 (i2v (layout_of struct_list_node).(ly_size) size_t) ]))) ;
        locinfo: loc_31 ;
-        LocInfoE loc_75 ((LocInfoE loc_76 (!{void*} (LocInfoE loc_77 ("node1")))) at{struct_list_node} "val") <-{ it_layout i32 }
-          LocInfoE loc_78 (i2v 1 i32) ;
+        LocInfoE loc_68 ((LocInfoE loc_69 (!{void*} (LocInfoE loc_70 ("node1")))) at{struct_list_node} "val") <-{ it_layout i32 }
+          LocInfoE loc_71 (i2v 1 i32) ;
        locinfo: loc_32 ;
-        LocInfoE loc_71 ((LocInfoE loc_72 (!{void*} (LocInfoE loc_73 ("node1")))) at{struct_list_node} "next") <-{ void* }
-          LocInfoE loc_74 (NULL) ;
+        LocInfoE loc_64 ((LocInfoE loc_65 (!{void*} (LocInfoE loc_66 ("node1")))) at{struct_list_node} "next") <-{ void* }
+          LocInfoE loc_67 (NULL) ;
        "node2" <-{ void* }
-          LocInfoE loc_65 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_65 (Call (LocInfoE loc_67 (global_alloc)) [@{expr} LocInfoE loc_68 (i2v (layout_of struct_list_node).(ly_size) size_t) ]))) ;
+          LocInfoE loc_58 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_58 (Call (LocInfoE loc_60 (global_alloc)) [@{expr} LocInfoE loc_61 (i2v (layout_of struct_list_node).(ly_size) size_t) ]))) ;
        locinfo: loc_34 ;
-        LocInfoE loc_61 ((LocInfoE loc_62 (!{void*} (LocInfoE loc_63 ("node2")))) at{struct_list_node} "val") <-{ it_layout i32 }
-          LocInfoE loc_64 (i2v 2 i32) ;
+        LocInfoE loc_54 ((LocInfoE loc_55 (!{void*} (LocInfoE loc_56 ("node2")))) at{struct_list_node} "val") <-{ it_layout i32 }
+          LocInfoE loc_57 (i2v 2 i32) ;
        locinfo: loc_35 ;
-        LocInfoE loc_57 ((LocInfoE loc_58 (!{void*} (LocInfoE loc_59 ("node2")))) at{struct_list_node} "next") <-{ void* }
-          LocInfoE loc_60 (NULL) ;
+        LocInfoE loc_50 ((LocInfoE loc_51 (!{void*} (LocInfoE loc_52 ("node2")))) at{struct_list_node} "next") <-{ void* }
+          LocInfoE loc_53 (NULL) ;
        locinfo: loc_36 ;
-        expr: (LocInfoE loc_36 (Call (LocInfoE loc_52 (global_append)) [@{expr} LocInfoE loc_53 (&(LocInfoE loc_54 ("node1"))) ;
-        LocInfoE loc_55 (use{void*} (LocInfoE loc_56 ("node2"))) ])) ;
-        locinfo: loc_47 ;
-        if: LocInfoE loc_47 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_47 ((LocInfoE loc_48 (use{void*} (LocInfoE loc_49 ("node1")))) !={PtrOp, PtrOp} (LocInfoE loc_50 (NULL)))))
+        expr: (LocInfoE loc_36 (Call (LocInfoE loc_45 (global_append)) [@{expr} LocInfoE loc_46 (&(LocInfoE loc_47 ("node1"))) ;
+        LocInfoE loc_48 (use{void*} (LocInfoE loc_49 ("node2"))) ])) ;
+        locinfo: loc_40 ;
+        if: LocInfoE loc_40 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_40 ((LocInfoE loc_41 (use{void*} (LocInfoE loc_42 ("node1")))) !={PtrOp, PtrOp} (LocInfoE loc_43 (NULL)))))
        then
-        locinfo: loc_39 ;
        Goto "#1"
        else
        Goto "#2"
      ]> $
      <[ "#1" :=
-        locinfo: loc_39 ;
-        assert: (LocInfoE loc_40 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_40 ((LocInfoE loc_41 (use{it_layout i32} (LocInfoE loc_42 ((LocInfoE loc_43 (!{void*} (LocInfoE loc_44 ("node1")))) at{struct_list_node} "val")))) ={IntOp i32, IntOp i32} (LocInfoE loc_45 (i2v 1 i32)))))) ;
        Return (VOID)
      ]> $
      <[ "#2" :=

--- a/examples/talk_demo1.c
+++ b/examples/talk_demo1.c
@@ -16,7 +16,6 @@ void append(list_t *l, list_t k) {
  }
 }

-/* [[rc::requires("[alloc_initialized]")]] */
 void test() {
  struct list_node * node1 = alloc(sizeof(struct list_node));
  node1->val = 1; node1->next = NULL;
@@ -26,7 +25,4 @@ void test() {
  if(node1 != NULL) {
    assert(node1->val == 1);
  }
-  /* assert(node1->next->val == 2); */
-  /* free(sizeof(struct list_node), node1->next); */
-  /* free(sizeof(struct list_node), node1); */
 }
--- a/examples/talk_demo2.c
+++ b/examples/talk_demo2.c
@@ -28,9 +28,6 @@ void test() {
  node2->val = 2; node2->next = NULL;
  append(&node1, node2);
  if(node1 != NULL) {
-    assert(node1->val == 1);
+    /* assert(node1->val == 1); */
  }
-  /* assert(node1->next->val == 2); */
-  /* free(sizeof(struct list_node), node1->next); */
-  /* free(sizeof(struct list_node), node1); */
 }
--- a/examples/talk_demo3.c
+++ b/examples/talk_demo3.c
@@ -33,109 +33,9 @@ void test() {
  node2->val = 2; node2->next = NULL;
  append(&node1, node2);
  if(node1 != NULL) {
-    assert(node1->val == 1);
+    /* assert(node1->val == 1); */
  }
  /* assert(node1->next->val == 2); */
  /* free(sizeof(struct list_node), node1->next); */
  /* free(sizeof(struct list_node), node1); */
 }
-
-/*
-typedef struct
-   [[rc::refined_by("u : unit")]]
-   [[rc::ptr_type("list_t : optional<&own<...>, null>")]] list_node {
-  [[rc::field("int<i32>")]]
-  int val;
-  [[rc::field("list_t")]]
-  struct list_node *next;
-} *list_t;
-
-[[rc::args("&own<list_t>", "list_t")]]
-void append(list_t *l, list_t k) {
-  if(*l == NULL) {
-    *l = k;
-  } else {
-    append(&(*l)->next, k);
-  }
-}
-*/
-
-/*
-[[rc::parameters("p : loc")]]
-[[rc::args("p @ &own<list_t>", "list_t")]]
-[[rc::ensures("own p : list_t")]]
-void append(list_t *l, list_t k) {
-  if(*l == NULL) {
-    *l = k;
-  } else {
-    append(&(*l)->next, k);
-  }
-}
- */
-
-/*
-typedef struct
-   [[rc::refined_by("xs : {list Z}")]]
-   [[rc::ptr_type("list_t : {xs <> []} @ optional<&own<...>, null>")]]
-   [[rc::exists("y : Z", "ys : {list Z}")]]
-   [[rc::constraints("{xs = y :: ys}")]]
-list_node {
-  [[rc::field("y @ int<i32>")]]
-  int val;
-  [[rc::field("ys @ list_t")]]
-  struct list_node *next;
-} *list_t;
- */
-
-/*
-[[rc::parameters("p : loc", "xs : {list Z}", "ys : {list Z}")]]
-[[rc::args("p @ &own<xs @ list_t>", "ys @ list_t")]]
-[[rc::ensures("own p : {xs ++ ys} @ list_t")]]
-void append(list_t *l, list_t k) {
-  if(*l == NULL) {
-    *l = k;
-  } else {
-    append(&(*l)->next, k);
-  }
-}
- */
-
-/*
-  if (node1 != NULL) {
-    if (node1->next != NULL) {
-      rc_unfold(node1->next->next);
-      free(sizeof(struct list_node), node1->next);
-    }
-    free(sizeof(struct list_node), node1);
-  }
- */
-
-/*
-typedef struct
-  [[rc::refined_by("xs : {list Z}")]]
-  [[rc::ptr_type("list_t : {xs <> []} @ optional<&own<...>, null>")]]
-  [[rc::exists("y : Z", "ys : {list Z}")]]
-  [[rc::constraints("{xs = y :: ys}")]]
-list_node {
-  [[rc::field("y @ int<i32>")]]
-  int val;