update talk demo 3

examples/proofs/talk_demo3/generated_code.v

@@ -41,40 +41,47 @@ 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_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 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 of struct [list_node]. *)
   Program Definition struct_list_node := {|
@@ -133,32 +140,35 @@ Section code.
     f_code := (
       <[ "#0" :=
         "node1" <-{ void* }
-          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) ]))) ;
+          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) ]))) ;
         locinfo: loc_31 ;
-        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) ;
+        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) ;
         locinfo: loc_32 ;
-        LocInfoE loc_64 ((LocInfoE loc_65 (!{void*} (LocInfoE loc_66 ("node1")))) at{struct_list_node} "next") <-{ void* }
-          LocInfoE loc_67 (NULL) ;
+        LocInfoE loc_71 ((LocInfoE loc_72 (!{void*} (LocInfoE loc_73 ("node1")))) at{struct_list_node} "next") <-{ void* }
+          LocInfoE loc_74 (NULL) ;
         "node2" <-{ void* }
-          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) ]))) ;
+          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) ]))) ;
         locinfo: loc_34 ;
-        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) ;
+        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) ;
         locinfo: loc_35 ;
-        LocInfoE loc_50 ((LocInfoE loc_51 (!{void*} (LocInfoE loc_52 ("node2")))) at{struct_list_node} "next") <-{ void* }
-          LocInfoE loc_53 (NULL) ;
+        LocInfoE loc_57 ((LocInfoE loc_58 (!{void*} (LocInfoE loc_59 ("node2")))) at{struct_list_node} "next") <-{ void* }
+          LocInfoE loc_60 (NULL) ;
         locinfo: loc_36 ;
-        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)))))
+        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)))))
         then
-        Goto "#1"
+        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" :=

examples/talk_demo3.c

@@ -33,9 +33,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); */
 }