diff --git a/tutorial/proofs/t03_list/generated_code.v b/tutorial/proofs/t03_list/generated_code.v
index ed709d635dd17d53c0bcee10f3920fe696bf2106..5e27f24b4621e27c699b2a15ca046eea6eaa68c9 100644
--- a/tutorial/proofs/t03_list/generated_code.v
+++ b/tutorial/proofs/t03_list/generated_code.v
@@ -6,163 +6,163 @@ Set Default Proof Using "Type".
(* Generated from [tutorial/t03_list.c]. *)
Section code.
Definition file_0 : string := "tutorial/t03_list.c".
- Definition loc_2 : location_info := LocationInfo file_0 124 4 124 25.
- Definition loc_3 : location_info := LocationInfo file_0 125 4 125 42.
- Definition loc_4 : location_info := LocationInfo file_0 126 4 126 42.
- Definition loc_5 : location_info := LocationInfo file_0 127 4 127 42.
- Definition loc_6 : location_info := LocationInfo file_0 129 4 129 28.
- Definition loc_7 : location_info := LocationInfo file_0 131 4 131 15.
- Definition loc_8 : location_info := LocationInfo file_0 132 4 132 15.
- Definition loc_9 : location_info := LocationInfo file_0 133 4 133 15.
- Definition loc_10 : location_info := LocationInfo file_0 135 4 135 29.
- Definition loc_11 : location_info := LocationInfo file_0 136 4 136 29.
- Definition loc_12 : location_info := LocationInfo file_0 137 4 137 29.
- Definition loc_13 : location_info := LocationInfo file_0 139 4 139 29.
- Definition loc_14 : location_info := LocationInfo file_0 141 4 141 25.
- Definition loc_15 : location_info := LocationInfo file_0 143 4 143 29.
- Definition loc_16 : location_info := LocationInfo file_0 145 4 145 23.
- Definition loc_17 : location_info := LocationInfo file_0 146 4 146 23.
- Definition loc_18 : location_info := LocationInfo file_0 147 4 147 23.
- Definition loc_19 : location_info := LocationInfo file_0 149 4 149 28.
- Definition loc_20 : location_info := LocationInfo file_0 151 4 151 32.
- Definition loc_21 : location_info := LocationInfo file_0 152 4 152 32.
- Definition loc_22 : location_info := LocationInfo file_0 153 4 153 32.
- Definition loc_23 : location_info := LocationInfo file_0 155 4 155 32.
- Definition loc_24 : location_info := LocationInfo file_0 156 4 156 32.
- Definition loc_25 : location_info := LocationInfo file_0 157 4 157 32.
- Definition loc_26 : location_info := LocationInfo file_0 157 4 157 8.
- Definition loc_27 : location_info := LocationInfo file_0 157 4 157 8.
- Definition loc_28 : location_info := LocationInfo file_0 157 9 157 23.
- Definition loc_29 : location_info := LocationInfo file_0 157 25 157 30.
- Definition loc_30 : location_info := LocationInfo file_0 157 25 157 30.
- Definition loc_31 : location_info := LocationInfo file_0 156 4 156 8.
- Definition loc_32 : location_info := LocationInfo file_0 156 4 156 8.
- Definition loc_33 : location_info := LocationInfo file_0 156 9 156 23.
- Definition loc_34 : location_info := LocationInfo file_0 156 25 156 30.
- Definition loc_35 : location_info := LocationInfo file_0 156 25 156 30.
- Definition loc_36 : location_info := LocationInfo file_0 155 4 155 8.
- Definition loc_37 : location_info := LocationInfo file_0 155 4 155 8.
- Definition loc_38 : location_info := LocationInfo file_0 155 9 155 23.
- Definition loc_39 : location_info := LocationInfo file_0 155 25 155 30.
- Definition loc_40 : location_info := LocationInfo file_0 155 25 155 30.
- Definition loc_41 : location_info := LocationInfo file_0 153 11 153 30.
- Definition loc_42 : location_info := LocationInfo file_0 153 11 153 17.
- Definition loc_43 : location_info := LocationInfo file_0 153 11 153 17.
- Definition loc_44 : location_info := LocationInfo file_0 153 12 153 17.
- Definition loc_45 : location_info := LocationInfo file_0 153 12 153 17.
- Definition loc_46 : location_info := LocationInfo file_0 153 21 153 30.
- Definition loc_47 : location_info := LocationInfo file_0 153 29 153 30.
- Definition loc_48 : location_info := LocationInfo file_0 152 11 152 30.
- Definition loc_49 : location_info := LocationInfo file_0 152 11 152 17.
- Definition loc_50 : location_info := LocationInfo file_0 152 11 152 17.
- Definition loc_51 : location_info := LocationInfo file_0 152 12 152 17.
- Definition loc_52 : location_info := LocationInfo file_0 152 12 152 17.
- Definition loc_53 : location_info := LocationInfo file_0 152 21 152 30.
- Definition loc_54 : location_info := LocationInfo file_0 152 29 152 30.
- Definition loc_55 : location_info := LocationInfo file_0 151 11 151 30.
- Definition loc_56 : location_info := LocationInfo file_0 151 11 151 17.
- Definition loc_57 : location_info := LocationInfo file_0 151 11 151 17.
- Definition loc_58 : location_info := LocationInfo file_0 151 12 151 17.
- Definition loc_59 : location_info := LocationInfo file_0 151 12 151 17.
- Definition loc_60 : location_info := LocationInfo file_0 151 21 151 30.
- Definition loc_61 : location_info := LocationInfo file_0 151 29 151 30.
- Definition loc_62 : location_info := LocationInfo file_0 149 11 149 26.
- Definition loc_63 : location_info := LocationInfo file_0 149 11 149 19.
- Definition loc_64 : location_info := LocationInfo file_0 149 11 149 19.
- Definition loc_65 : location_info := LocationInfo file_0 149 20 149 25.
- Definition loc_66 : location_info := LocationInfo file_0 149 21 149 25.
- Definition loc_67 : location_info := LocationInfo file_0 147 4 147 9.
- Definition loc_68 : location_info := LocationInfo file_0 147 12 147 22.
- Definition loc_69 : location_info := LocationInfo file_0 147 12 147 15.
- Definition loc_70 : location_info := LocationInfo file_0 147 12 147 15.
- Definition loc_71 : location_info := LocationInfo file_0 147 16 147 21.
- Definition loc_72 : location_info := LocationInfo file_0 147 17 147 21.
- Definition loc_73 : location_info := LocationInfo file_0 146 4 146 9.
- Definition loc_74 : location_info := LocationInfo file_0 146 12 146 22.
- Definition loc_75 : location_info := LocationInfo file_0 146 12 146 15.
- Definition loc_76 : location_info := LocationInfo file_0 146 12 146 15.
- Definition loc_77 : location_info := LocationInfo file_0 146 16 146 21.
- Definition loc_78 : location_info := LocationInfo file_0 146 17 146 21.
- Definition loc_79 : location_info := LocationInfo file_0 145 4 145 9.
- Definition loc_80 : location_info := LocationInfo file_0 145 12 145 22.
- Definition loc_81 : location_info := LocationInfo file_0 145 12 145 15.
- Definition loc_82 : location_info := LocationInfo file_0 145 12 145 15.
- Definition loc_83 : location_info := LocationInfo file_0 145 16 145 21.
- Definition loc_84 : location_info := LocationInfo file_0 145 17 145 21.
- Definition loc_85 : location_info := LocationInfo file_0 143 11 143 27.
- Definition loc_86 : location_info := LocationInfo file_0 143 11 143 17.
- Definition loc_87 : location_info := LocationInfo file_0 143 11 143 17.
- Definition loc_88 : location_info := LocationInfo file_0 143 18 143 23.
- Definition loc_89 : location_info := LocationInfo file_0 143 19 143 23.
- Definition loc_90 : location_info := LocationInfo file_0 143 25 143 26.
- Definition loc_91 : location_info := LocationInfo file_0 141 4 141 8.
- Definition loc_92 : location_info := LocationInfo file_0 141 11 141 24.
- Definition loc_93 : location_info := LocationInfo file_0 141 11 141 18.
- Definition loc_94 : location_info := LocationInfo file_0 141 11 141 18.
- Definition loc_95 : location_info := LocationInfo file_0 141 19 141 23.
- Definition loc_96 : location_info := LocationInfo file_0 141 19 141 23.
- Definition loc_97 : location_info := LocationInfo file_0 139 11 139 27.
- Definition loc_98 : location_info := LocationInfo file_0 139 11 139 17.
- Definition loc_99 : location_info := LocationInfo file_0 139 11 139 17.
- Definition loc_100 : location_info := LocationInfo file_0 139 18 139 23.
- Definition loc_101 : location_info := LocationInfo file_0 139 19 139 23.
- Definition loc_102 : location_info := LocationInfo file_0 139 25 139 26.
- Definition loc_103 : location_info := LocationInfo file_0 137 4 137 8.
- Definition loc_104 : location_info := LocationInfo file_0 137 11 137 28.
- Definition loc_105 : location_info := LocationInfo file_0 137 11 137 15.
- Definition loc_106 : location_info := LocationInfo file_0 137 11 137 15.
- Definition loc_107 : location_info := LocationInfo file_0 137 16 137 20.
- Definition loc_108 : location_info := LocationInfo file_0 137 16 137 20.
- Definition loc_109 : location_info := LocationInfo file_0 137 22 137 27.
- Definition loc_110 : location_info := LocationInfo file_0 137 22 137 27.
- Definition loc_111 : location_info := LocationInfo file_0 136 4 136 8.
- Definition loc_112 : location_info := LocationInfo file_0 136 11 136 28.
- Definition loc_113 : location_info := LocationInfo file_0 136 11 136 15.
- Definition loc_114 : location_info := LocationInfo file_0 136 11 136 15.
- Definition loc_115 : location_info := LocationInfo file_0 136 16 136 20.
- Definition loc_116 : location_info := LocationInfo file_0 136 16 136 20.
- Definition loc_117 : location_info := LocationInfo file_0 136 22 136 27.
- Definition loc_118 : location_info := LocationInfo file_0 136 22 136 27.
- Definition loc_119 : location_info := LocationInfo file_0 135 4 135 8.
- Definition loc_120 : location_info := LocationInfo file_0 135 11 135 28.
- Definition loc_121 : location_info := LocationInfo file_0 135 11 135 15.
- Definition loc_122 : location_info := LocationInfo file_0 135 11 135 15.
- Definition loc_123 : location_info := LocationInfo file_0 135 16 135 20.
- Definition loc_124 : location_info := LocationInfo file_0 135 16 135 20.
- Definition loc_125 : location_info := LocationInfo file_0 135 22 135 27.
- Definition loc_126 : location_info := LocationInfo file_0 135 22 135 27.
- Definition loc_127 : location_info := LocationInfo file_0 133 4 133 10.
- Definition loc_128 : location_info := LocationInfo file_0 133 5 133 10.
- Definition loc_129 : location_info := LocationInfo file_0 133 5 133 10.
- Definition loc_130 : location_info := LocationInfo file_0 133 13 133 14.
- Definition loc_131 : location_info := LocationInfo file_0 132 4 132 10.
- Definition loc_132 : location_info := LocationInfo file_0 132 5 132 10.
- Definition loc_133 : location_info := LocationInfo file_0 132 5 132 10.
- Definition loc_134 : location_info := LocationInfo file_0 132 13 132 14.
- Definition loc_135 : location_info := LocationInfo file_0 131 4 131 10.
- Definition loc_136 : location_info := LocationInfo file_0 131 5 131 10.
- Definition loc_137 : location_info := LocationInfo file_0 131 5 131 10.
- Definition loc_138 : location_info := LocationInfo file_0 131 13 131 14.
- Definition loc_139 : location_info := LocationInfo file_0 129 11 129 26.
- Definition loc_140 : location_info := LocationInfo file_0 129 11 129 19.
- Definition loc_141 : location_info := LocationInfo file_0 129 11 129 19.
- Definition loc_142 : location_info := LocationInfo file_0 129 20 129 25.
- Definition loc_143 : location_info := LocationInfo file_0 129 21 129 25.
- Definition loc_144 : location_info := LocationInfo file_0 127 20 127 41.
- Definition loc_145 : location_info := LocationInfo file_0 127 20 127 25.
- Definition loc_146 : location_info := LocationInfo file_0 127 20 127 25.
- Definition loc_147 : location_info := LocationInfo file_0 127 26 127 40.
- Definition loc_150 : location_info := LocationInfo file_0 126 20 126 41.
- Definition loc_151 : location_info := LocationInfo file_0 126 20 126 25.
- Definition loc_152 : location_info := LocationInfo file_0 126 20 126 25.
- Definition loc_153 : location_info := LocationInfo file_0 126 26 126 40.
- Definition loc_156 : location_info := LocationInfo file_0 125 20 125 41.
- Definition loc_157 : location_info := LocationInfo file_0 125 20 125 25.
- Definition loc_158 : location_info := LocationInfo file_0 125 20 125 25.
- Definition loc_159 : location_info := LocationInfo file_0 125 26 125 40.
- Definition loc_162 : location_info := LocationInfo file_0 124 18 124 24.
- Definition loc_163 : location_info := LocationInfo file_0 124 18 124 22.
- Definition loc_164 : location_info := LocationInfo file_0 124 18 124 22.
+ Definition loc_2 : location_info := LocationInfo file_0 141 4 141 25.
+ Definition loc_3 : location_info := LocationInfo file_0 142 4 142 42.
+ Definition loc_4 : location_info := LocationInfo file_0 143 4 143 42.
+ Definition loc_5 : location_info := LocationInfo file_0 144 4 144 42.
+ Definition loc_6 : location_info := LocationInfo file_0 146 4 146 28.
+ Definition loc_7 : location_info := LocationInfo file_0 148 4 148 15.
+ Definition loc_8 : location_info := LocationInfo file_0 149 4 149 15.
+ Definition loc_9 : location_info := LocationInfo file_0 150 4 150 15.
+ Definition loc_10 : location_info := LocationInfo file_0 152 4 152 29.
+ Definition loc_11 : location_info := LocationInfo file_0 153 4 153 29.
+ Definition loc_12 : location_info := LocationInfo file_0 154 4 154 29.
+ Definition loc_13 : location_info := LocationInfo file_0 156 4 156 29.
+ Definition loc_14 : location_info := LocationInfo file_0 158 4 158 25.
+ Definition loc_15 : location_info := LocationInfo file_0 160 4 160 29.
+ Definition loc_16 : location_info := LocationInfo file_0 162 4 162 23.
+ Definition loc_17 : location_info := LocationInfo file_0 163 4 163 23.
+ Definition loc_18 : location_info := LocationInfo file_0 164 4 164 23.
+ Definition loc_19 : location_info := LocationInfo file_0 166 4 166 28.
+ Definition loc_20 : location_info := LocationInfo file_0 168 4 168 32.
+ Definition loc_21 : location_info := LocationInfo file_0 169 4 169 32.
+ Definition loc_22 : location_info := LocationInfo file_0 170 4 170 32.
+ Definition loc_23 : location_info := LocationInfo file_0 172 4 172 32.
+ Definition loc_24 : location_info := LocationInfo file_0 173 4 173 32.
+ Definition loc_25 : location_info := LocationInfo file_0 174 4 174 32.
+ Definition loc_26 : location_info := LocationInfo file_0 174 4 174 8.
+ Definition loc_27 : location_info := LocationInfo file_0 174 4 174 8.
+ Definition loc_28 : location_info := LocationInfo file_0 174 9 174 23.
+ Definition loc_29 : location_info := LocationInfo file_0 174 25 174 30.
+ Definition loc_30 : location_info := LocationInfo file_0 174 25 174 30.
+ Definition loc_31 : location_info := LocationInfo file_0 173 4 173 8.
+ Definition loc_32 : location_info := LocationInfo file_0 173 4 173 8.
+ Definition loc_33 : location_info := LocationInfo file_0 173 9 173 23.
+ Definition loc_34 : location_info := LocationInfo file_0 173 25 173 30.
+ Definition loc_35 : location_info := LocationInfo file_0 173 25 173 30.
+ Definition loc_36 : location_info := LocationInfo file_0 172 4 172 8.
+ Definition loc_37 : location_info := LocationInfo file_0 172 4 172 8.
+ Definition loc_38 : location_info := LocationInfo file_0 172 9 172 23.
+ Definition loc_39 : location_info := LocationInfo file_0 172 25 172 30.
+ Definition loc_40 : location_info := LocationInfo file_0 172 25 172 30.
+ Definition loc_41 : location_info := LocationInfo file_0 170 11 170 30.
+ Definition loc_42 : location_info := LocationInfo file_0 170 11 170 17.
+ Definition loc_43 : location_info := LocationInfo file_0 170 11 170 17.
+ Definition loc_44 : location_info := LocationInfo file_0 170 12 170 17.
+ Definition loc_45 : location_info := LocationInfo file_0 170 12 170 17.
+ Definition loc_46 : location_info := LocationInfo file_0 170 21 170 30.
+ Definition loc_47 : location_info := LocationInfo file_0 170 29 170 30.
+ Definition loc_48 : location_info := LocationInfo file_0 169 11 169 30.
+ Definition loc_49 : location_info := LocationInfo file_0 169 11 169 17.
+ Definition loc_50 : location_info := LocationInfo file_0 169 11 169 17.
+ Definition loc_51 : location_info := LocationInfo file_0 169 12 169 17.
+ Definition loc_52 : location_info := LocationInfo file_0 169 12 169 17.
+ Definition loc_53 : location_info := LocationInfo file_0 169 21 169 30.
+ Definition loc_54 : location_info := LocationInfo file_0 169 29 169 30.
+ Definition loc_55 : location_info := LocationInfo file_0 168 11 168 30.
+ Definition loc_56 : location_info := LocationInfo file_0 168 11 168 17.
+ Definition loc_57 : location_info := LocationInfo file_0 168 11 168 17.
+ Definition loc_58 : location_info := LocationInfo file_0 168 12 168 17.
+ Definition loc_59 : location_info := LocationInfo file_0 168 12 168 17.
+ Definition loc_60 : location_info := LocationInfo file_0 168 21 168 30.
+ Definition loc_61 : location_info := LocationInfo file_0 168 29 168 30.
+ Definition loc_62 : location_info := LocationInfo file_0 166 11 166 26.
+ Definition loc_63 : location_info := LocationInfo file_0 166 11 166 19.
+ Definition loc_64 : location_info := LocationInfo file_0 166 11 166 19.
+ Definition loc_65 : location_info := LocationInfo file_0 166 20 166 25.
+ Definition loc_66 : location_info := LocationInfo file_0 166 21 166 25.
+ Definition loc_67 : location_info := LocationInfo file_0 164 4 164 9.
+ Definition loc_68 : location_info := LocationInfo file_0 164 12 164 22.
+ Definition loc_69 : location_info := LocationInfo file_0 164 12 164 15.
+ Definition loc_70 : location_info := LocationInfo file_0 164 12 164 15.
+ Definition loc_71 : location_info := LocationInfo file_0 164 16 164 21.
+ Definition loc_72 : location_info := LocationInfo file_0 164 17 164 21.
+ Definition loc_73 : location_info := LocationInfo file_0 163 4 163 9.
+ Definition loc_74 : location_info := LocationInfo file_0 163 12 163 22.
+ Definition loc_75 : location_info := LocationInfo file_0 163 12 163 15.
+ Definition loc_76 : location_info := LocationInfo file_0 163 12 163 15.
+ Definition loc_77 : location_info := LocationInfo file_0 163 16 163 21.
+ Definition loc_78 : location_info := LocationInfo file_0 163 17 163 21.
+ Definition loc_79 : location_info := LocationInfo file_0 162 4 162 9.
+ Definition loc_80 : location_info := LocationInfo file_0 162 12 162 22.
+ Definition loc_81 : location_info := LocationInfo file_0 162 12 162 15.
+ Definition loc_82 : location_info := LocationInfo file_0 162 12 162 15.
+ Definition loc_83 : location_info := LocationInfo file_0 162 16 162 21.
+ Definition loc_84 : location_info := LocationInfo file_0 162 17 162 21.
+ Definition loc_85 : location_info := LocationInfo file_0 160 11 160 27.
+ Definition loc_86 : location_info := LocationInfo file_0 160 11 160 17.
+ Definition loc_87 : location_info := LocationInfo file_0 160 11 160 17.
+ Definition loc_88 : location_info := LocationInfo file_0 160 18 160 23.
+ Definition loc_89 : location_info := LocationInfo file_0 160 19 160 23.
+ Definition loc_90 : location_info := LocationInfo file_0 160 25 160 26.
+ Definition loc_91 : location_info := LocationInfo file_0 158 4 158 8.
+ Definition loc_92 : location_info := LocationInfo file_0 158 11 158 24.
+ Definition loc_93 : location_info := LocationInfo file_0 158 11 158 18.
+ Definition loc_94 : location_info := LocationInfo file_0 158 11 158 18.
+ Definition loc_95 : location_info := LocationInfo file_0 158 19 158 23.
+ Definition loc_96 : location_info := LocationInfo file_0 158 19 158 23.
+ Definition loc_97 : location_info := LocationInfo file_0 156 11 156 27.
+ Definition loc_98 : location_info := LocationInfo file_0 156 11 156 17.
+ Definition loc_99 : location_info := LocationInfo file_0 156 11 156 17.
+ Definition loc_100 : location_info := LocationInfo file_0 156 18 156 23.
+ Definition loc_101 : location_info := LocationInfo file_0 156 19 156 23.
+ Definition loc_102 : location_info := LocationInfo file_0 156 25 156 26.
+ Definition loc_103 : location_info := LocationInfo file_0 154 4 154 8.
+ Definition loc_104 : location_info := LocationInfo file_0 154 11 154 28.
+ Definition loc_105 : location_info := LocationInfo file_0 154 11 154 15.
+ Definition loc_106 : location_info := LocationInfo file_0 154 11 154 15.
+ Definition loc_107 : location_info := LocationInfo file_0 154 16 154 20.
+ Definition loc_108 : location_info := LocationInfo file_0 154 16 154 20.
+ Definition loc_109 : location_info := LocationInfo file_0 154 22 154 27.
+ Definition loc_110 : location_info := LocationInfo file_0 154 22 154 27.
+ Definition loc_111 : location_info := LocationInfo file_0 153 4 153 8.
+ Definition loc_112 : location_info := LocationInfo file_0 153 11 153 28.
+ Definition loc_113 : location_info := LocationInfo file_0 153 11 153 15.
+ Definition loc_114 : location_info := LocationInfo file_0 153 11 153 15.
+ Definition loc_115 : location_info := LocationInfo file_0 153 16 153 20.
+ Definition loc_116 : location_info := LocationInfo file_0 153 16 153 20.
+ Definition loc_117 : location_info := LocationInfo file_0 153 22 153 27.
+ Definition loc_118 : location_info := LocationInfo file_0 153 22 153 27.
+ Definition loc_119 : location_info := LocationInfo file_0 152 4 152 8.
+ Definition loc_120 : location_info := LocationInfo file_0 152 11 152 28.
+ Definition loc_121 : location_info := LocationInfo file_0 152 11 152 15.
+ Definition loc_122 : location_info := LocationInfo file_0 152 11 152 15.
+ Definition loc_123 : location_info := LocationInfo file_0 152 16 152 20.
+ Definition loc_124 : location_info := LocationInfo file_0 152 16 152 20.
+ Definition loc_125 : location_info := LocationInfo file_0 152 22 152 27.
+ Definition loc_126 : location_info := LocationInfo file_0 152 22 152 27.
+ Definition loc_127 : location_info := LocationInfo file_0 150 4 150 10.
+ Definition loc_128 : location_info := LocationInfo file_0 150 5 150 10.
+ Definition loc_129 : location_info := LocationInfo file_0 150 5 150 10.
+ Definition loc_130 : location_info := LocationInfo file_0 150 13 150 14.
+ Definition loc_131 : location_info := LocationInfo file_0 149 4 149 10.
+ Definition loc_132 : location_info := LocationInfo file_0 149 5 149 10.
+ Definition loc_133 : location_info := LocationInfo file_0 149 5 149 10.
+ Definition loc_134 : location_info := LocationInfo file_0 149 13 149 14.
+ Definition loc_135 : location_info := LocationInfo file_0 148 4 148 10.
+ Definition loc_136 : location_info := LocationInfo file_0 148 5 148 10.
+ Definition loc_137 : location_info := LocationInfo file_0 148 5 148 10.
+ Definition loc_138 : location_info := LocationInfo file_0 148 13 148 14.
+ Definition loc_139 : location_info := LocationInfo file_0 146 11 146 26.
+ Definition loc_140 : location_info := LocationInfo file_0 146 11 146 19.
+ Definition loc_141 : location_info := LocationInfo file_0 146 11 146 19.
+ Definition loc_142 : location_info := LocationInfo file_0 146 20 146 25.
+ Definition loc_143 : location_info := LocationInfo file_0 146 21 146 25.
+ Definition loc_144 : location_info := LocationInfo file_0 144 20 144 41.
+ Definition loc_145 : location_info := LocationInfo file_0 144 20 144 25.
+ Definition loc_146 : location_info := LocationInfo file_0 144 20 144 25.
+ Definition loc_147 : location_info := LocationInfo file_0 144 26 144 40.
+ Definition loc_150 : location_info := LocationInfo file_0 143 20 143 41.
+ Definition loc_151 : location_info := LocationInfo file_0 143 20 143 25.
+ Definition loc_152 : location_info := LocationInfo file_0 143 20 143 25.
+ Definition loc_153 : location_info := LocationInfo file_0 143 26 143 40.
+ Definition loc_156 : location_info := LocationInfo file_0 142 20 142 41.
+ Definition loc_157 : location_info := LocationInfo file_0 142 20 142 25.
+ Definition loc_158 : location_info := LocationInfo file_0 142 20 142 25.
+ Definition loc_159 : location_info := LocationInfo file_0 142 26 142 40.
+ Definition loc_162 : location_info := LocationInfo file_0 141 18 141 24.
+ Definition loc_163 : location_info := LocationInfo file_0 141 18 141 22.
+ Definition loc_164 : location_info := LocationInfo file_0 141 18 141 22.
Definition loc_169 : location_info := LocationInfo file_0 27 4 27 26.
Definition loc_170 : location_info := LocationInfo file_0 27 11 27 25.
Definition loc_173 : location_info := LocationInfo file_0 35 4 35 32.
@@ -264,113 +264,143 @@ Section code.
Definition loc_282 : location_info := LocationInfo file_0 74 16 74 30.
Definition loc_283 : location_info := LocationInfo file_0 70 4 70 5.
Definition loc_284 : location_info := LocationInfo file_0 70 8 70 22.
- Definition loc_287 : location_info := LocationInfo file_0 87 2 87 19.
- Definition loc_288 : location_info := LocationInfo file_0 91 2 93 3.
- Definition loc_289 : location_info := LocationInfo file_0 94 2 94 12.
- Definition loc_290 : location_info := LocationInfo file_0 94 2 94 6.
- Definition loc_291 : location_info := LocationInfo file_0 94 3 94 6.
- Definition loc_292 : location_info := LocationInfo file_0 94 3 94 6.
- Definition loc_293 : location_info := LocationInfo file_0 94 9 94 11.
- Definition loc_294 : location_info := LocationInfo file_0 94 9 94 11.
- Definition loc_295 : location_info := LocationInfo file_0 91 2 93 3.
- Definition loc_296 : location_info := LocationInfo file_0 91 31 93 3.
- Definition loc_297 : location_info := LocationInfo file_0 92 4 92 26.
- Definition loc_298 : location_info := LocationInfo file_0 91 2 93 3.
- Definition loc_299 : location_info := LocationInfo file_0 91 2 93 3.
- Definition loc_300 : location_info := LocationInfo file_0 92 4 92 7.
- Definition loc_301 : location_info := LocationInfo file_0 92 10 92 25.
- Definition loc_302 : location_info := LocationInfo file_0 92 11 92 25.
- Definition loc_303 : location_info := LocationInfo file_0 92 12 92 18.
- Definition loc_304 : location_info := LocationInfo file_0 92 12 92 18.
- Definition loc_305 : location_info := LocationInfo file_0 92 14 92 17.
- Definition loc_306 : location_info := LocationInfo file_0 92 14 92 17.
- Definition loc_307 : location_info := LocationInfo file_0 91 8 91 30.
- Definition loc_308 : location_info := LocationInfo file_0 91 8 91 12.
- Definition loc_309 : location_info := LocationInfo file_0 91 8 91 12.
- Definition loc_310 : location_info := LocationInfo file_0 91 9 91 12.
- Definition loc_311 : location_info := LocationInfo file_0 91 9 91 12.
- Definition loc_312 : location_info := LocationInfo file_0 91 16 91 30.
- Definition loc_313 : location_info := LocationInfo file_0 87 16 87 18.
- Definition loc_314 : location_info := LocationInfo file_0 87 16 87 18.
- Definition loc_319 : location_info := LocationInfo file_0 104 4 104 21.
- Definition loc_320 : location_info := LocationInfo file_0 109 4 118 5.
- Definition loc_321 : location_info := LocationInfo file_0 119 4 119 13.
- Definition loc_322 : location_info := LocationInfo file_0 119 11 119 12.
- Definition loc_323 : location_info := LocationInfo file_0 109 4 118 5.
- Definition loc_324 : location_info := LocationInfo file_0 109 35 118 5.
- Definition loc_325 : location_info := LocationInfo file_0 110 8 110 27.
- Definition loc_326 : location_info := LocationInfo file_0 112 8 112 33.
- Definition loc_327 : location_info := LocationInfo file_0 113 8 115 9.
- Definition loc_328 : location_info := LocationInfo file_0 117 8 117 26.
- Definition loc_329 : location_info := LocationInfo file_0 109 4 118 5.
- Definition loc_330 : location_info := LocationInfo file_0 109 4 118 5.
- Definition loc_331 : location_info := LocationInfo file_0 117 8 117 12.
- Definition loc_332 : location_info := LocationInfo file_0 117 15 117 25.
- Definition loc_333 : location_info := LocationInfo file_0 117 16 117 25.
- Definition loc_334 : location_info := LocationInfo file_0 117 16 117 19.
- Definition loc_335 : location_info := LocationInfo file_0 117 16 117 19.
- Definition loc_336 : location_info := LocationInfo file_0 113 23 115 9.
- Definition loc_337 : location_info := LocationInfo file_0 114 12 114 21.
- Definition loc_338 : location_info := LocationInfo file_0 114 19 114 20.
- Definition loc_340 : location_info := LocationInfo file_0 113 11 113 21.
- Definition loc_341 : location_info := LocationInfo file_0 113 11 113 16.
- Definition loc_342 : location_info := LocationInfo file_0 113 11 113 16.
- Definition loc_343 : location_info := LocationInfo file_0 113 12 113 16.
- Definition loc_344 : location_info := LocationInfo file_0 113 12 113 16.
- Definition loc_345 : location_info := LocationInfo file_0 113 20 113 21.
- Definition loc_346 : location_info := LocationInfo file_0 113 20 113 21.
- Definition loc_347 : location_info := LocationInfo file_0 112 23 112 32.
- Definition loc_348 : location_info := LocationInfo file_0 112 23 112 32.
- Definition loc_349 : location_info := LocationInfo file_0 112 23 112 26.
- Definition loc_350 : location_info := LocationInfo file_0 112 23 112 26.
- Definition loc_353 : location_info := LocationInfo file_0 110 21 110 26.
- Definition loc_354 : location_info := LocationInfo file_0 110 21 110 26.
- Definition loc_355 : location_info := LocationInfo file_0 110 22 110 26.
- Definition loc_356 : location_info := LocationInfo file_0 110 22 110 26.
- Definition loc_359 : location_info := LocationInfo file_0 109 10 109 33.
- Definition loc_360 : location_info := LocationInfo file_0 109 10 109 15.
- Definition loc_361 : location_info := LocationInfo file_0 109 10 109 15.
- Definition loc_362 : location_info := LocationInfo file_0 109 11 109 15.
- Definition loc_363 : location_info := LocationInfo file_0 109 11 109 15.
- Definition loc_364 : location_info := LocationInfo file_0 109 19 109 33.
- Definition loc_365 : location_info := LocationInfo file_0 104 19 104 20.
- Definition loc_366 : location_info := LocationInfo file_0 104 19 104 20.
- Definition loc_371 : location_info := LocationInfo file_0 164 2 164 18.
- Definition loc_372 : location_info := LocationInfo file_0 174 2 179 3.
- Definition loc_373 : location_info := LocationInfo file_0 174 2 179 3.
- Definition loc_374 : location_info := LocationInfo file_0 174 31 179 3.
- Definition loc_375 : location_info := LocationInfo file_0 175 4 175 25.
- Definition loc_376 : location_info := LocationInfo file_0 176 4 176 20.
- Definition loc_377 : location_info := LocationInfo file_0 177 4 177 14.
- Definition loc_378 : location_info := LocationInfo file_0 178 4 178 19.
- Definition loc_379 : location_info := LocationInfo file_0 174 2 179 3.
- Definition loc_380 : location_info := LocationInfo file_0 174 2 179 3.
- Definition loc_381 : location_info := LocationInfo file_0 178 4 178 7.
- Definition loc_382 : location_info := LocationInfo file_0 178 10 178 18.
- Definition loc_383 : location_info := LocationInfo file_0 178 10 178 18.
- Definition loc_384 : location_info := LocationInfo file_0 177 4 177 7.
- Definition loc_385 : location_info := LocationInfo file_0 177 5 177 7.
- Definition loc_386 : location_info := LocationInfo file_0 177 5 177 7.
- Definition loc_387 : location_info := LocationInfo file_0 177 10 177 13.
- Definition loc_388 : location_info := LocationInfo file_0 177 10 177 13.
- Definition loc_389 : location_info := LocationInfo file_0 176 4 176 13.
- Definition loc_390 : location_info := LocationInfo file_0 176 4 176 7.
- Definition loc_391 : location_info := LocationInfo file_0 176 4 176 7.
- Definition loc_392 : location_info := LocationInfo file_0 176 16 176 19.
- Definition loc_393 : location_info := LocationInfo file_0 176 16 176 19.
- Definition loc_394 : location_info := LocationInfo file_0 176 17 176 19.
- Definition loc_395 : location_info := LocationInfo file_0 176 17 176 19.
- Definition loc_396 : location_info := LocationInfo file_0 175 4 175 12.
- Definition loc_397 : location_info := LocationInfo file_0 175 15 175 24.
- Definition loc_398 : location_info := LocationInfo file_0 175 15 175 24.
- Definition loc_399 : location_info := LocationInfo file_0 175 15 175 18.
- Definition loc_400 : location_info := LocationInfo file_0 175 15 175 18.
- Definition loc_401 : location_info := LocationInfo file_0 174 8 174 29.
- Definition loc_402 : location_info := LocationInfo file_0 174 8 174 11.
- Definition loc_403 : location_info := LocationInfo file_0 174 8 174 11.
- Definition loc_404 : location_info := LocationInfo file_0 174 15 174 29.
- Definition loc_405 : location_info := LocationInfo file_0 164 15 164 17.
- Definition loc_406 : location_info := LocationInfo file_0 164 15 164 17.
+ Definition loc_287 : location_info := LocationInfo file_0 89 2 89 17.
+ Definition loc_288 : location_info := LocationInfo file_0 93 2 96 3.
+ Definition loc_289 : location_info := LocationInfo file_0 97 2 97 13.
+ Definition loc_290 : location_info := LocationInfo file_0 97 9 97 12.
+ Definition loc_291 : location_info := LocationInfo file_0 97 9 97 12.
+ Definition loc_292 : location_info := LocationInfo file_0 93 2 96 3.
+ Definition loc_293 : location_info := LocationInfo file_0 93 31 96 3.
+ Definition loc_294 : location_info := LocationInfo file_0 94 4 94 20.
+ Definition loc_295 : location_info := LocationInfo file_0 95 4 95 13.
+ Definition loc_296 : location_info := LocationInfo file_0 93 2 96 3.
+ Definition loc_297 : location_info := LocationInfo file_0 93 2 96 3.
+ Definition loc_298 : location_info := LocationInfo file_0 95 4 95 7.
+ Definition loc_299 : location_info := LocationInfo file_0 95 4 95 12.
+ Definition loc_300 : location_info := LocationInfo file_0 95 4 95 7.
+ Definition loc_301 : location_info := LocationInfo file_0 95 4 95 7.
+ Definition loc_302 : location_info := LocationInfo file_0 95 11 95 12.
+ Definition loc_303 : location_info := LocationInfo file_0 94 4 94 5.
+ Definition loc_304 : location_info := LocationInfo file_0 94 8 94 19.
+ Definition loc_305 : location_info := LocationInfo file_0 94 9 94 19.
+ Definition loc_306 : location_info := LocationInfo file_0 94 9 94 13.
+ Definition loc_307 : location_info := LocationInfo file_0 94 9 94 13.
+ Definition loc_308 : location_info := LocationInfo file_0 94 11 94 12.
+ Definition loc_309 : location_info := LocationInfo file_0 94 11 94 12.
+ Definition loc_310 : location_info := LocationInfo file_0 93 9 93 29.
+ Definition loc_311 : location_info := LocationInfo file_0 93 9 93 11.
+ Definition loc_312 : location_info := LocationInfo file_0 93 9 93 11.
+ Definition loc_313 : location_info := LocationInfo file_0 93 10 93 11.
+ Definition loc_314 : location_info := LocationInfo file_0 93 10 93 11.
+ Definition loc_315 : location_info := LocationInfo file_0 93 15 93 29.
+ Definition loc_316 : location_info := LocationInfo file_0 89 15 89 16.
+ Definition loc_321 : location_info := LocationInfo file_0 104 2 104 19.
+ Definition loc_322 : location_info := LocationInfo file_0 108 2 110 3.
+ Definition loc_323 : location_info := LocationInfo file_0 111 2 111 12.
+ Definition loc_324 : location_info := LocationInfo file_0 111 2 111 6.
+ Definition loc_325 : location_info := LocationInfo file_0 111 3 111 6.
+ Definition loc_326 : location_info := LocationInfo file_0 111 3 111 6.
+ Definition loc_327 : location_info := LocationInfo file_0 111 9 111 11.
+ Definition loc_328 : location_info := LocationInfo file_0 111 9 111 11.
+ Definition loc_329 : location_info := LocationInfo file_0 108 2 110 3.
+ Definition loc_330 : location_info := LocationInfo file_0 108 31 110 3.
+ Definition loc_331 : location_info := LocationInfo file_0 109 4 109 26.
+ Definition loc_332 : location_info := LocationInfo file_0 108 2 110 3.
+ Definition loc_333 : location_info := LocationInfo file_0 108 2 110 3.
+ Definition loc_334 : location_info := LocationInfo file_0 109 4 109 7.
+ Definition loc_335 : location_info := LocationInfo file_0 109 10 109 25.
+ Definition loc_336 : location_info := LocationInfo file_0 109 11 109 25.
+ Definition loc_337 : location_info := LocationInfo file_0 109 12 109 18.
+ Definition loc_338 : location_info := LocationInfo file_0 109 12 109 18.
+ Definition loc_339 : location_info := LocationInfo file_0 109 14 109 17.
+ Definition loc_340 : location_info := LocationInfo file_0 109 14 109 17.
+ Definition loc_341 : location_info := LocationInfo file_0 108 8 108 30.
+ Definition loc_342 : location_info := LocationInfo file_0 108 8 108 12.
+ Definition loc_343 : location_info := LocationInfo file_0 108 8 108 12.
+ Definition loc_344 : location_info := LocationInfo file_0 108 9 108 12.
+ Definition loc_345 : location_info := LocationInfo file_0 108 9 108 12.
+ Definition loc_346 : location_info := LocationInfo file_0 108 16 108 30.
+ Definition loc_347 : location_info := LocationInfo file_0 104 16 104 18.
+ Definition loc_348 : location_info := LocationInfo file_0 104 16 104 18.
+ Definition loc_353 : location_info := LocationInfo file_0 121 4 121 21.
+ Definition loc_354 : location_info := LocationInfo file_0 126 4 135 5.
+ Definition loc_355 : location_info := LocationInfo file_0 136 4 136 13.
+ Definition loc_356 : location_info := LocationInfo file_0 136 11 136 12.
+ Definition loc_357 : location_info := LocationInfo file_0 126 4 135 5.
+ Definition loc_358 : location_info := LocationInfo file_0 126 35 135 5.
+ Definition loc_359 : location_info := LocationInfo file_0 127 8 127 27.
+ Definition loc_360 : location_info := LocationInfo file_0 129 8 129 33.
+ Definition loc_361 : location_info := LocationInfo file_0 130 8 132 9.
+ Definition loc_362 : location_info := LocationInfo file_0 134 8 134 26.
+ Definition loc_363 : location_info := LocationInfo file_0 126 4 135 5.
+ Definition loc_364 : location_info := LocationInfo file_0 126 4 135 5.
+ Definition loc_365 : location_info := LocationInfo file_0 134 8 134 12.
+ Definition loc_366 : location_info := LocationInfo file_0 134 15 134 25.
+ Definition loc_367 : location_info := LocationInfo file_0 134 16 134 25.
+ Definition loc_368 : location_info := LocationInfo file_0 134 16 134 19.
+ Definition loc_369 : location_info := LocationInfo file_0 134 16 134 19.
+ Definition loc_370 : location_info := LocationInfo file_0 130 23 132 9.
+ Definition loc_371 : location_info := LocationInfo file_0 131 12 131 21.
+ Definition loc_372 : location_info := LocationInfo file_0 131 19 131 20.
+ Definition loc_374 : location_info := LocationInfo file_0 130 11 130 21.
+ Definition loc_375 : location_info := LocationInfo file_0 130 11 130 16.
+ Definition loc_376 : location_info := LocationInfo file_0 130 11 130 16.
+ Definition loc_377 : location_info := LocationInfo file_0 130 12 130 16.
+ Definition loc_378 : location_info := LocationInfo file_0 130 12 130 16.
+ Definition loc_379 : location_info := LocationInfo file_0 130 20 130 21.
+ Definition loc_380 : location_info := LocationInfo file_0 130 20 130 21.
+ Definition loc_381 : location_info := LocationInfo file_0 129 23 129 32.
+ Definition loc_382 : location_info := LocationInfo file_0 129 23 129 32.
+ Definition loc_383 : location_info := LocationInfo file_0 129 23 129 26.
+ Definition loc_384 : location_info := LocationInfo file_0 129 23 129 26.
+ Definition loc_387 : location_info := LocationInfo file_0 127 21 127 26.
+ Definition loc_388 : location_info := LocationInfo file_0 127 21 127 26.
+ Definition loc_389 : location_info := LocationInfo file_0 127 22 127 26.
+ Definition loc_390 : location_info := LocationInfo file_0 127 22 127 26.
+ Definition loc_393 : location_info := LocationInfo file_0 126 10 126 33.
+ Definition loc_394 : location_info := LocationInfo file_0 126 10 126 15.
+ Definition loc_395 : location_info := LocationInfo file_0 126 10 126 15.
+ Definition loc_396 : location_info := LocationInfo file_0 126 11 126 15.
+ Definition loc_397 : location_info := LocationInfo file_0 126 11 126 15.
+ Definition loc_398 : location_info := LocationInfo file_0 126 19 126 33.
+ Definition loc_399 : location_info := LocationInfo file_0 121 19 121 20.
+ Definition loc_400 : location_info := LocationInfo file_0 121 19 121 20.
+ Definition loc_405 : location_info := LocationInfo file_0 181 2 181 18.
+ Definition loc_406 : location_info := LocationInfo file_0 191 2 196 3.
+ Definition loc_407 : location_info := LocationInfo file_0 191 2 196 3.
+ Definition loc_408 : location_info := LocationInfo file_0 191 31 196 3.
+ Definition loc_409 : location_info := LocationInfo file_0 192 4 192 25.
+ Definition loc_410 : location_info := LocationInfo file_0 193 4 193 20.
+ Definition loc_411 : location_info := LocationInfo file_0 194 4 194 14.
+ Definition loc_412 : location_info := LocationInfo file_0 195 4 195 19.
+ Definition loc_413 : location_info := LocationInfo file_0 191 2 196 3.
+ Definition loc_414 : location_info := LocationInfo file_0 191 2 196 3.
+ Definition loc_415 : location_info := LocationInfo file_0 195 4 195 7.
+ Definition loc_416 : location_info := LocationInfo file_0 195 10 195 18.
+ Definition loc_417 : location_info := LocationInfo file_0 195 10 195 18.
+ Definition loc_418 : location_info := LocationInfo file_0 194 4 194 7.
+ Definition loc_419 : location_info := LocationInfo file_0 194 5 194 7.
+ Definition loc_420 : location_info := LocationInfo file_0 194 5 194 7.
+ Definition loc_421 : location_info := LocationInfo file_0 194 10 194 13.
+ Definition loc_422 : location_info := LocationInfo file_0 194 10 194 13.
+ Definition loc_423 : location_info := LocationInfo file_0 193 4 193 13.
+ Definition loc_424 : location_info := LocationInfo file_0 193 4 193 7.
+ Definition loc_425 : location_info := LocationInfo file_0 193 4 193 7.
+ Definition loc_426 : location_info := LocationInfo file_0 193 16 193 19.
+ Definition loc_427 : location_info := LocationInfo file_0 193 16 193 19.
+ Definition loc_428 : location_info := LocationInfo file_0 193 17 193 19.
+ Definition loc_429 : location_info := LocationInfo file_0 193 17 193 19.
+ Definition loc_430 : location_info := LocationInfo file_0 192 4 192 12.
+ Definition loc_431 : location_info := LocationInfo file_0 192 15 192 24.
+ Definition loc_432 : location_info := LocationInfo file_0 192 15 192 24.
+ Definition loc_433 : location_info := LocationInfo file_0 192 15 192 18.
+ Definition loc_434 : location_info := LocationInfo file_0 192 15 192 18.
+ Definition loc_435 : location_info := LocationInfo file_0 191 8 191 29.
+ Definition loc_436 : location_info := LocationInfo file_0 191 8 191 11.
+ Definition loc_437 : location_info := LocationInfo file_0 191 8 191 11.
+ Definition loc_438 : location_info := LocationInfo file_0 191 15 191 29.
+ Definition loc_439 : location_info := LocationInfo file_0 181 15 181 17.
+ Definition loc_440 : location_info := LocationInfo file_0 181 15 181 17.
(* Definition of struct [list]. *)
Program Definition struct_list := {|
@@ -663,6 +693,53 @@ Section code.
)%E
|}.
+ (* Definition of function [length]. *)
+ Definition impl_length : function := {|
+ f_args := [
+ ("p", LPtr)
+ ];
+ f_local_vars := [
+ ("len", it_layout size_t)
+ ];
+ f_init := "#0";
+ f_code := (
+ <[ "#0" :=
+ "len" <-{ it_layout size_t }
+ LocInfoE loc_316 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_316 (i2v 0 i32))) ;
+ locinfo: loc_288 ;
+ Goto "#1"
+ ]> $
+ <[ "#1" :=
+ locinfo: loc_310 ;
+ if: LocInfoE loc_310 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_310 ((LocInfoE loc_311 (use{LPtr} (LocInfoE loc_313 (!{LPtr} (LocInfoE loc_314 ("p")))))) !={PtrOp, PtrOp} (LocInfoE loc_315 (NULL)))))
+ then
+ locinfo: loc_294 ;
+ Goto "#2"
+ else
+ locinfo: loc_289 ;
+ Goto "#3"
+ ]> $
+ <[ "#2" :=
+ locinfo: loc_294 ;
+ LocInfoE loc_303 ("p") <-{ LPtr }
+ LocInfoE loc_304 (&(LocInfoE loc_305 ((LocInfoE loc_306 (!{LPtr} (LocInfoE loc_308 (!{LPtr} (LocInfoE loc_309 ("p")))))) at{struct_list} "tail"))) ;
+ locinfo: loc_295 ;
+ LocInfoE loc_298 ("len") <-{ it_layout size_t }
+ LocInfoE loc_299 ((LocInfoE loc_300 (use{it_layout size_t} (LocInfoE loc_301 ("len")))) +{IntOp size_t, IntOp size_t} (LocInfoE loc_302 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_302 (i2v 1 i32))))) ;
+ locinfo: loc_296 ;
+ Goto "continue15"
+ ]> $
+ <[ "#3" :=
+ locinfo: loc_289 ;
+ Return (LocInfoE loc_290 (use{it_layout size_t} (LocInfoE loc_291 ("len"))))
+ ]> $
+ <[ "continue15" :=
+ locinfo: loc_288 ;
+ Goto "#1"
+ ]> $∅
+ )%E
+ |}.
+
(* Definition of function [append]. *)
Definition impl_append : function := {|
f_args := [
@@ -676,35 +753,35 @@ Section code.
f_code := (
<[ "#0" :=
"end" <-{ LPtr }
- LocInfoE loc_313 (use{LPtr} (LocInfoE loc_314 ("l1"))) ;
- locinfo: loc_288 ;
+ LocInfoE loc_347 (use{LPtr} (LocInfoE loc_348 ("l1"))) ;
+ locinfo: loc_322 ;
Goto "#1"
]> $
<[ "#1" :=
- locinfo: loc_307 ;
- if: LocInfoE loc_307 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_307 ((LocInfoE loc_308 (use{LPtr} (LocInfoE loc_310 (!{LPtr} (LocInfoE loc_311 ("end")))))) !={PtrOp, PtrOp} (LocInfoE loc_312 (NULL)))))
+ locinfo: loc_341 ;
+ if: LocInfoE loc_341 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_341 ((LocInfoE loc_342 (use{LPtr} (LocInfoE loc_344 (!{LPtr} (LocInfoE loc_345 ("end")))))) !={PtrOp, PtrOp} (LocInfoE loc_346 (NULL)))))
then
- locinfo: loc_297 ;
+ locinfo: loc_331 ;
Goto "#2"
else
- locinfo: loc_289 ;
+ locinfo: loc_323 ;
Goto "#3"
]> $
<[ "#2" :=
- locinfo: loc_297 ;
- LocInfoE loc_300 ("end") <-{ LPtr }
- LocInfoE loc_301 (&(LocInfoE loc_302 ((LocInfoE loc_303 (!{LPtr} (LocInfoE loc_305 (!{LPtr} (LocInfoE loc_306 ("end")))))) at{struct_list} "tail"))) ;
- locinfo: loc_298 ;
- Goto "continue15"
+ locinfo: loc_331 ;
+ LocInfoE loc_334 ("end") <-{ LPtr }
+ LocInfoE loc_335 (&(LocInfoE loc_336 ((LocInfoE loc_337 (!{LPtr} (LocInfoE loc_339 (!{LPtr} (LocInfoE loc_340 ("end")))))) at{struct_list} "tail"))) ;
+ locinfo: loc_332 ;
+ Goto "continue19"
]> $
<[ "#3" :=
- locinfo: loc_289 ;
- LocInfoE loc_291 (!{LPtr} (LocInfoE loc_292 ("end"))) <-{ LPtr }
- LocInfoE loc_293 (use{LPtr} (LocInfoE loc_294 ("l2"))) ;
+ locinfo: loc_323 ;
+ LocInfoE loc_325 (!{LPtr} (LocInfoE loc_326 ("end"))) <-{ LPtr }
+ LocInfoE loc_327 (use{LPtr} (LocInfoE loc_328 ("l2"))) ;
Return (VOID)
]> $
- <[ "continue15" :=
- locinfo: loc_288 ;
+ <[ "continue19" :=
+ locinfo: loc_322 ;
Goto "#1"
]> $∅
)%E
@@ -725,54 +802,54 @@ Section code.
f_code := (
<[ "#0" :=
"prev" <-{ LPtr }
- LocInfoE loc_365 (use{LPtr} (LocInfoE loc_366 ("p"))) ;
- locinfo: loc_320 ;
+ LocInfoE loc_399 (use{LPtr} (LocInfoE loc_400 ("p"))) ;
+ locinfo: loc_354 ;
Goto "#1"
]> $
<[ "#1" :=
- locinfo: loc_359 ;
- if: LocInfoE loc_359 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_359 ((LocInfoE loc_360 (use{LPtr} (LocInfoE loc_362 (!{LPtr} (LocInfoE loc_363 ("prev")))))) !={PtrOp, PtrOp} (LocInfoE loc_364 (NULL)))))
+ locinfo: loc_393 ;
+ if: LocInfoE loc_393 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_393 ((LocInfoE loc_394 (use{LPtr} (LocInfoE loc_396 (!{LPtr} (LocInfoE loc_397 ("prev")))))) !={PtrOp, PtrOp} (LocInfoE loc_398 (NULL)))))
then
Goto "#2"
else
- locinfo: loc_321 ;
+ locinfo: loc_355 ;
Goto "#3"
]> $
<[ "#2" :=
"cur" <-{ LPtr }
- LocInfoE loc_353 (use{LPtr} (LocInfoE loc_355 (!{LPtr} (LocInfoE loc_356 ("prev"))))) ;
+ LocInfoE loc_387 (use{LPtr} (LocInfoE loc_389 (!{LPtr} (LocInfoE loc_390 ("prev"))))) ;
"head" <-{ LPtr }
- LocInfoE loc_347 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_347 (use{LPtr} (LocInfoE loc_348 ((LocInfoE loc_349 (!{LPtr} (LocInfoE loc_350 ("cur")))) at{struct_list} "head"))))) ;
- locinfo: loc_340 ;
- if: LocInfoE loc_340 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_340 ((LocInfoE loc_341 (use{it_layout size_t} (LocInfoE loc_343 (!{LPtr} (LocInfoE loc_344 ("head")))))) ={IntOp size_t, IntOp size_t} (LocInfoE loc_345 (use{it_layout size_t} (LocInfoE loc_346 ("k")))))))
+ LocInfoE loc_381 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_381 (use{LPtr} (LocInfoE loc_382 ((LocInfoE loc_383 (!{LPtr} (LocInfoE loc_384 ("cur")))) at{struct_list} "head"))))) ;
+ locinfo: loc_374 ;
+ if: LocInfoE loc_374 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_374 ((LocInfoE loc_375 (use{it_layout size_t} (LocInfoE loc_377 (!{LPtr} (LocInfoE loc_378 ("head")))))) ={IntOp size_t, IntOp size_t} (LocInfoE loc_379 (use{it_layout size_t} (LocInfoE loc_380 ("k")))))))
then
- locinfo: loc_337 ;
+ locinfo: loc_371 ;
Goto "#5"
else
- locinfo: loc_328 ;
+ locinfo: loc_362 ;
Goto "#6"
]> $
<[ "#3" :=
- locinfo: loc_321 ;
- Return (LocInfoE loc_322 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_322 (i2v 0 i32))))
+ locinfo: loc_355 ;
+ Return (LocInfoE loc_356 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_356 (i2v 0 i32))))
]> $
<[ "#4" :=
- locinfo: loc_328 ;
- LocInfoE loc_331 ("prev") <-{ LPtr }
- LocInfoE loc_332 (&(LocInfoE loc_333 ((LocInfoE loc_334 (!{LPtr} (LocInfoE loc_335 ("cur")))) at{struct_list} "tail"))) ;
- locinfo: loc_329 ;
- Goto "continue19"
+ locinfo: loc_362 ;
+ LocInfoE loc_365 ("prev") <-{ LPtr }
+ LocInfoE loc_366 (&(LocInfoE loc_367 ((LocInfoE loc_368 (!{LPtr} (LocInfoE loc_369 ("cur")))) at{struct_list} "tail"))) ;
+ locinfo: loc_363 ;
+ Goto "continue23"
]> $
<[ "#5" :=
- locinfo: loc_337 ;
- Return (LocInfoE loc_338 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_338 (i2v 1 i32))))
+ locinfo: loc_371 ;
+ Return (LocInfoE loc_372 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_372 (i2v 1 i32))))
]> $
<[ "#6" :=
- locinfo: loc_328 ;
+ locinfo: loc_362 ;
Goto "#4"
]> $
- <[ "continue19" :=
- locinfo: loc_320 ;
+ <[ "continue23" :=
+ locinfo: loc_354 ;
Goto "#1"
]> $∅
)%E
@@ -792,40 +869,40 @@ Section code.
f_code := (
<[ "#0" :=
"cur" <-{ LPtr }
- LocInfoE loc_405 (use{LPtr} (LocInfoE loc_406 ("l1"))) ;
- locinfo: loc_372 ;
+ LocInfoE loc_439 (use{LPtr} (LocInfoE loc_440 ("l1"))) ;
+ locinfo: loc_406 ;
Goto "#1"
]> $
<[ "#1" :=
- locinfo: loc_401 ;
- if: LocInfoE loc_401 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_401 ((LocInfoE loc_402 (use{LPtr} (LocInfoE loc_403 ("cur")))) !={PtrOp, PtrOp} (LocInfoE loc_404 (NULL)))))
+ locinfo: loc_435 ;
+ if: LocInfoE loc_435 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_435 ((LocInfoE loc_436 (use{LPtr} (LocInfoE loc_437 ("cur")))) !={PtrOp, PtrOp} (LocInfoE loc_438 (NULL)))))
then
- locinfo: loc_375 ;
+ locinfo: loc_409 ;
Goto "#2"
else
Goto "#3"
]> $
<[ "#2" :=
- locinfo: loc_375 ;
- LocInfoE loc_396 ("cur_tail") <-{ LPtr }
- LocInfoE loc_397 (use{LPtr} (LocInfoE loc_398 ((LocInfoE loc_399 (!{LPtr} (LocInfoE loc_400 ("cur")))) at{struct_list} "tail"))) ;
- locinfo: loc_376 ;
- LocInfoE loc_389 ((LocInfoE loc_390 (!{LPtr} (LocInfoE loc_391 ("cur")))) at{struct_list} "tail") <-{ LPtr }
- LocInfoE loc_392 (use{LPtr} (LocInfoE loc_394 (!{LPtr} (LocInfoE loc_395 ("l2"))))) ;
- locinfo: loc_377 ;
- LocInfoE loc_385 (!{LPtr} (LocInfoE loc_386 ("l2"))) <-{ LPtr }
- LocInfoE loc_387 (use{LPtr} (LocInfoE loc_388 ("cur"))) ;
- locinfo: loc_378 ;
- LocInfoE loc_381 ("cur") <-{ LPtr }
- LocInfoE loc_382 (use{LPtr} (LocInfoE loc_383 ("cur_tail"))) ;
- locinfo: loc_379 ;
- Goto "continue26"
+ locinfo: loc_409 ;
+ LocInfoE loc_430 ("cur_tail") <-{ LPtr }
+ LocInfoE loc_431 (use{LPtr} (LocInfoE loc_432 ((LocInfoE loc_433 (!{LPtr} (LocInfoE loc_434 ("cur")))) at{struct_list} "tail"))) ;
+ locinfo: loc_410 ;
+ LocInfoE loc_423 ((LocInfoE loc_424 (!{LPtr} (LocInfoE loc_425 ("cur")))) at{struct_list} "tail") <-{ LPtr }
+ LocInfoE loc_426 (use{LPtr} (LocInfoE loc_428 (!{LPtr} (LocInfoE loc_429 ("l2"))))) ;
+ locinfo: loc_411 ;
+ LocInfoE loc_419 (!{LPtr} (LocInfoE loc_420 ("l2"))) <-{ LPtr }
+ LocInfoE loc_421 (use{LPtr} (LocInfoE loc_422 ("cur"))) ;
+ locinfo: loc_412 ;
+ LocInfoE loc_415 ("cur") <-{ LPtr }
+ LocInfoE loc_416 (use{LPtr} (LocInfoE loc_417 ("cur_tail"))) ;
+ locinfo: loc_413 ;
+ Goto "continue30"
]> $
<[ "#3" :=
Return (VOID)
]> $
- <[ "continue26" :=
- locinfo: loc_372 ;
+ <[ "continue30" :=
+ locinfo: loc_406 ;
Goto "#1"
]> $∅
)%E
diff --git a/tutorial/proofs/t03_list/generated_proof_length.v b/tutorial/proofs/t03_list/generated_proof_length.v
new file mode 100644
index 0000000000000000000000000000000000000000..3cf1c083966010220ff57b66b6a23104a975c872
--- /dev/null
+++ b/tutorial/proofs/t03_list/generated_proof_length.v
@@ -0,0 +1,34 @@
+From refinedc.typing Require Import typing.
+From refinedc.tutorial.t03_list Require Import generated_code.
+From refinedc.tutorial.t03_list Require Import generated_spec.
+Set Default Proof Using "Type".
+
+(* Generated from [tutorial/t03_list.c]. *)
+Section proof_length.
+ Context `{!typeG Σ} `{!globalG Σ}.
+
+ (* Typing proof for [length]. *)
+ Lemma type_length :
+ ⊢ typed_function impl_length type_of_length.
+ Proof.
+ start_function "length" ([p l]) => arg_p local_len.
+ split_blocks ((
+ <[ "#1" :=
+ ∃ q : loc,
+ ∃ l1 : list type,
+ arg_p â—â‚— (q @ (&own (l1 @ (list_t)))) ∗
+ local_len â—â‚— ((length l - length l1) @ (int (size_t))) ∗
+ (p â—â‚— (wand (q â—â‚— l1 @ list_t) (l @ (list_t))))
+ ]> $
+ ∅
+ )%I : gmap label (iProp Σ)) ((
+ ∅
+ )%I : gmap label (iProp Σ)).
+ - repeat liRStep; liShow.
+ all: print_typesystem_goal "length" "#0".
+ - repeat liRStep; liShow.
+ all: print_typesystem_goal "length" "#1".
+ Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
+ all: print_sidecondition_goal "length".
+ Qed.
+End proof_length.
diff --git a/tutorial/proofs/t03_list/generated_spec.v b/tutorial/proofs/t03_list/generated_spec.v
index 8403dce3f1f44c603514848ab27ee83e77c82d4d..e403b481eb494cb2ee0f889c12fb35e66a984d9c 100644
--- a/tutorial/proofs/t03_list/generated_spec.v
+++ b/tutorial/proofs/t03_list/generated_spec.v
@@ -122,6 +122,11 @@ Section spec.
fn(∀ l : (list type); (l @ (list_t)); True)
→ ∃ () : (), ((rev l) @ (list_t)); True.
+ (* Specifications for function [length]. *)
+ Definition type_of_length :=
+ fn(∀ (p, l) : loc * (list type); (p @ (&own (l @ (list_t)))); ⌜length l <= max_int size_tâŒ)
+ → ∃ () : (), ((length l) @ (int (size_t))); (p â—â‚— (l @ (list_t))).
+
(* Specifications for function [append]. *)
Definition type_of_append :=
fn(∀ (p, l1, l2) : loc * (list type) * (list type); (p @ (&own (l1 @ (list_t)))), (l2 @ (list_t)); True)
diff --git a/tutorial/proofs/t03_list/proof_files b/tutorial/proofs/t03_list/proof_files
index 709c2e2d7d9958f17e0b4abe4bcd8a6fddc03d70..4f3248c6ee0babb6fcb631386b020f666599766d 100644
--- a/tutorial/proofs/t03_list/proof_files
+++ b/tutorial/proofs/t03_list/proof_files
@@ -5,6 +5,7 @@ generated_proof_free.v
generated_proof_free_array.v
generated_proof_init.v
generated_proof_is_empty.v
+generated_proof_length.v
generated_proof_member.v
generated_proof_pop.v
generated_proof_push.v
diff --git a/tutorial/t03_list.c b/tutorial/t03_list.c
index 72ccbd2562962cdd19e1d05692ea0de7b70bdaac..ddf745a31a388d020fd2fdea16325826ce3b0636 100644
--- a/tutorial/t03_list.c
+++ b/tutorial/t03_list.c
@@ -80,6 +80,23 @@ list_t reverse (list_t p) {
return w;
}
+[[rc::parameters("p : loc", "l : {list type}")]]
+[[rc::args("p @ &own<l @ list_t>")]]
+[[rc::requires("{length l <= max_int size_t}")]]
+[[rc::returns("{length l} @ int<size_t>")]]
+[[rc::ensures("p @ &own<l @ list_t>")]]
+size_t length (list_t *p) {
+ size_t len = 0;
+ [[rc::exists("q : loc", "l1 : {list type}")]]
+ [[rc::inv_vars("p : q @ &own<l1 @ list_t>", "len : {length l - length l1} @ int<size_t>")]]
+ [[rc::constraints("p @ &own<wand<{q â—â‚— l1 @ list_t}, l @ list_t>>")]]
+ while (*p != NULL) {
+ p = &(*p)->tail;
+ len += 1;
+ }
+ return len;
+}
+
[[rc::parameters("p : loc", "l1 : {list type}", "l2 : {list type}")]]
[[rc::args("p @ &own<l1 @ list_t>", "l2 @ list_t")]]
[[rc::ensures("p @ &own<{l1 ++ l2} @ list_t>")]]