fix generated code

f81a49ee · Michael Sammler · 7ef2bb97 · f81a49ee
Commit f81a49ee authored Mar 09, 2021 by Michael Sammler
--- a/examples/proofs/queue/generated_code.v
+++ b/examples/proofs/queue/generated_code.v
@@ -27,122 +27,122 @@ Section code.
  Definition loc_20 : location_info := LocationInfo file_0 27 18 27 23.
  Definition loc_21 : location_info := LocationInfo file_0 27 18 27 23.
  Definition loc_22 : location_info := LocationInfo file_0 27 24 27 44.
-  Definition loc_27 : location_info := LocationInfo file_0 39 2 39 38.
+  Definition loc_27 : location_info := LocationInfo file_0 38 2 38 38.
-  Definition loc_28 : location_info := LocationInfo file_0 39 9 39 37.
+  Definition loc_28 : location_info := LocationInfo file_0 38 9 38 37.
-  Definition loc_29 : location_info := LocationInfo file_0 39 9 39 19.
+  Definition loc_29 : location_info := LocationInfo file_0 38 9 38 19.
-  Definition loc_30 : location_info := LocationInfo file_0 39 9 39 19.
+  Definition loc_30 : location_info := LocationInfo file_0 38 9 38 19.
-  Definition loc_31 : location_info := LocationInfo file_0 39 9 39 13.
+  Definition loc_31 : location_info := LocationInfo file_0 38 9 38 13.
-  Definition loc_32 : location_info := LocationInfo file_0 39 9 39 13.
+  Definition loc_32 : location_info := LocationInfo file_0 38 9 38 13.
-  Definition loc_33 : location_info := LocationInfo file_0 39 11 39 12.
+  Definition loc_33 : location_info := LocationInfo file_0 38 11 38 12.
-  Definition loc_34 : location_info := LocationInfo file_0 39 11 39 12.
+  Definition loc_34 : location_info := LocationInfo file_0 38 11 38 12.
-  Definition loc_35 : location_info := LocationInfo file_0 39 23 39 37.
+  Definition loc_35 : location_info := LocationInfo file_0 38 23 38 37.
-  Definition loc_38 : location_info := LocationInfo file_0 47 2 47 55.
+  Definition loc_38 : location_info := LocationInfo file_0 46 2 46 55.
-  Definition loc_39 : location_info := LocationInfo file_0 48 2 48 17.
+  Definition loc_39 : location_info := LocationInfo file_0 47 2 47 17.
-  Definition loc_40 : location_info := LocationInfo file_0 49 2 49 30.
+  Definition loc_40 : location_info := LocationInfo file_0 48 2 48 30.
-  Definition loc_41 : location_info := LocationInfo file_0 50 2 50 21.
+  Definition loc_41 : location_info := LocationInfo file_0 49 2 49 21.
-  Definition loc_42 : location_info := LocationInfo file_0 51 2 51 27.
+  Definition loc_42 : location_info := LocationInfo file_0 50 2 50 27.
-  Definition loc_43 : location_info := LocationInfo file_0 51 2 51 12.
+  Definition loc_43 : location_info := LocationInfo file_0 50 2 50 12.
-  Definition loc_44 : location_info := LocationInfo file_0 51 2 51 6.
+  Definition loc_44 : location_info := LocationInfo file_0 50 2 50 6.
-  Definition loc_45 : location_info := LocationInfo file_0 51 2 51 6.
+  Definition loc_45 : location_info := LocationInfo file_0 50 2 50 6.
-  Definition loc_46 : location_info := LocationInfo file_0 51 4 51 5.
+  Definition loc_46 : location_info := LocationInfo file_0 50 4 50 5.
-  Definition loc_47 : location_info := LocationInfo file_0 51 4 51 5.
+  Definition loc_47 : location_info := LocationInfo file_0 50 4 50 5.
-  Definition loc_48 : location_info := LocationInfo file_0 51 15 51 26.
+  Definition loc_48 : location_info := LocationInfo file_0 50 15 50 26.
-  Definition loc_49 : location_info := LocationInfo file_0 51 16 51 26.
+  Definition loc_49 : location_info := LocationInfo file_0 50 16 50 26.
-  Definition loc_50 : location_info := LocationInfo file_0 51 16 51 20.
+  Definition loc_50 : location_info := LocationInfo file_0 50 16 50 20.
-  Definition loc_51 : location_info := LocationInfo file_0 51 16 51 20.
+  Definition loc_51 : location_info := LocationInfo file_0 50 16 50 20.
-  Definition loc_52 : location_info := LocationInfo file_0 50 2 50 13.
+  Definition loc_52 : location_info := LocationInfo file_0 49 2 49 13.
-  Definition loc_53 : location_info := LocationInfo file_0 50 3 50 13.
+  Definition loc_53 : location_info := LocationInfo file_0 49 3 49 13.
-  Definition loc_54 : location_info := LocationInfo file_0 50 3 50 13.
+  Definition loc_54 : location_info := LocationInfo file_0 49 3 49 13.
-  Definition loc_55 : location_info := LocationInfo file_0 50 3 50 7.
+  Definition loc_55 : location_info := LocationInfo file_0 49 3 49 7.
-  Definition loc_56 : location_info := LocationInfo file_0 50 3 50 7.
+  Definition loc_56 : location_info := LocationInfo file_0 49 3 49 7.
-  Definition loc_57 : location_info := LocationInfo file_0 50 5 50 6.
+  Definition loc_57 : location_info := LocationInfo file_0 49 5 49 6.
-  Definition loc_58 : location_info := LocationInfo file_0 50 5 50 6.
+  Definition loc_58 : location_info := LocationInfo file_0 49 5 49 6.
-  Definition loc_59 : location_info := LocationInfo file_0 50 16 50 20.
+  Definition loc_59 : location_info := LocationInfo file_0 49 16 49 20.
-  Definition loc_60 : location_info := LocationInfo file_0 50 16 50 20.
+  Definition loc_60 : location_info := LocationInfo file_0 49 16 49 20.
-  Definition loc_61 : location_info := LocationInfo file_0 49 2 49 12.
+  Definition loc_61 : location_info := LocationInfo file_0 48 2 48 12.
-  Definition loc_62 : location_info := LocationInfo file_0 49 2 49 6.
+  Definition loc_62 : location_info := LocationInfo file_0 48 2 48 6.
-  Definition loc_63 : location_info := LocationInfo file_0 49 2 49 6.
+  Definition loc_63 : location_info := LocationInfo file_0 48 2 48 6.
-  Definition loc_64 : location_info := LocationInfo file_0 49 15 49 29.
+  Definition loc_64 : location_info := LocationInfo file_0 48 15 48 29.
-  Definition loc_65 : location_info := LocationInfo file_0 48 2 48 12.
+  Definition loc_65 : location_info := LocationInfo file_0 47 2 47 12.
-  Definition loc_66 : location_info := LocationInfo file_0 48 2 48 6.
+  Definition loc_66 : location_info := LocationInfo file_0 47 2 47 6.
-  Definition loc_67 : location_info := LocationInfo file_0 48 2 48 6.
+  Definition loc_67 : location_info := LocationInfo file_0 47 2 47 6.
-  Definition loc_68 : location_info := LocationInfo file_0 48 15 48 16.
+  Definition loc_68 : location_info := LocationInfo file_0 47 15 47 16.
-  Definition loc_69 : location_info := LocationInfo file_0 48 15 48 16.
+  Definition loc_69 : location_info := LocationInfo file_0 47 15 47 16.
-  Definition loc_70 : location_info := LocationInfo file_0 47 22 47 54.
+  Definition loc_70 : location_info := LocationInfo file_0 46 22 46 54.
-  Definition loc_71 : location_info := LocationInfo file_0 47 22 47 27.
+  Definition loc_71 : location_info := LocationInfo file_0 46 22 46 27.
-  Definition loc_72 : location_info := LocationInfo file_0 47 22 47 27.
+  Definition loc_72 : location_info := LocationInfo file_0 46 22 46 27.
-  Definition loc_73 : location_info := LocationInfo file_0 47 28 47 53.
+  Definition loc_73 : location_info := LocationInfo file_0 46 28 46 53.
-  Definition loc_78 : location_info := LocationInfo file_0 61 2 63 3.
+  Definition loc_78 : location_info := LocationInfo file_0 59 2 61 3.
-  Definition loc_79 : location_info := LocationInfo file_0 64 2 64 33.
+  Definition loc_79 : location_info := LocationInfo file_0 62 2 62 33.
-  Definition loc_80 : location_info := LocationInfo file_0 65 2 65 25.
+  Definition loc_80 : location_info := LocationInfo file_0 63 2 63 25.
-  Definition loc_81 : location_info := LocationInfo file_0 66 2 71 3.
+  Definition loc_81 : location_info := LocationInfo file_0 64 2 69 3.
-  Definition loc_82 : location_info := LocationInfo file_0 72 2 72 40.
+  Definition loc_82 : location_info := LocationInfo file_0 70 2 70 40.
-  Definition loc_83 : location_info := LocationInfo file_0 73 2 73 13.
+  Definition loc_83 : location_info := LocationInfo file_0 71 2 71 13.
-  Definition loc_84 : location_info := LocationInfo file_0 73 9 73 12.
+  Definition loc_84 : location_info := LocationInfo file_0 71 9 71 12.
-  Definition loc_85 : location_info := LocationInfo file_0 73 9 73 12.
+  Definition loc_85 : location_info := LocationInfo file_0 71 9 71 12.
-  Definition loc_86 : location_info := LocationInfo file_0 72 2 72 6.
+  Definition loc_86 : location_info := LocationInfo file_0 70 2 70 6.
-  Definition loc_87 : location_info := LocationInfo file_0 72 2 72 6.
+  Definition loc_87 : location_info := LocationInfo file_0 70 2 70 6.
-  Definition loc_88 : location_info := LocationInfo file_0 72 7 72 32.
+  Definition loc_88 : location_info := LocationInfo file_0 70 7 70 32.
-  Definition loc_89 : location_info := LocationInfo file_0 72 34 72 38.
+  Definition loc_89 : location_info := LocationInfo file_0 70 34 70 38.
-  Definition loc_90 : location_info := LocationInfo file_0 72 34 72 38.
+  Definition loc_90 : location_info := LocationInfo file_0 70 34 70 38.
-  Definition loc_91 : location_info := LocationInfo file_0 66 35 69 3.
+  Definition loc_91 : location_info := LocationInfo file_0 64 35 67 3.
-  Definition loc_92 : location_info := LocationInfo file_0 67 4 67 32.
+  Definition loc_92 : location_info := LocationInfo file_0 65 4 65 32.
-  Definition loc_93 : location_info := LocationInfo file_0 68 4 68 29.
+  Definition loc_93 : location_info := LocationInfo file_0 66 4 66 29.
-  Definition loc_94 : location_info := LocationInfo file_0 68 4 68 14.
+  Definition loc_94 : location_info := LocationInfo file_0 66 4 66 14.
-  Definition loc_95 : location_info := LocationInfo file_0 68 4 68 8.
+  Definition loc_95 : location_info := LocationInfo file_0 66 4 66 8.
-  Definition loc_96 : location_info := LocationInfo file_0 68 4 68 8.
+  Definition loc_96 : location_info := LocationInfo file_0 66 4 66 8.
-  Definition loc_97 : location_info := LocationInfo file_0 68 6 68 7.
+  Definition loc_97 : location_info := LocationInfo file_0 66 6 66 7.
-  Definition loc_98 : location_info := LocationInfo file_0 68 6 68 7.
+  Definition loc_98 : location_info := LocationInfo file_0 66 6 66 7.
-  Definition loc_99 : location_info := LocationInfo file_0 68 17 68 28.
+  Definition loc_99 : location_info := LocationInfo file_0 66 17 66 28.
-  Definition loc_100 : location_info := LocationInfo file_0 68 18 68 28.
+  Definition loc_100 : location_info := LocationInfo file_0 66 18 66 28.
-  Definition loc_101 : location_info := LocationInfo file_0 68 18 68 22.
+  Definition loc_101 : location_info := LocationInfo file_0 66 18 66 22.
-  Definition loc_102 : location_info := LocationInfo file_0 68 18 68 22.
+  Definition loc_102 : location_info := LocationInfo file_0 66 18 66 22.
-  Definition loc_103 : location_info := LocationInfo file_0 68 20 68 21.
+  Definition loc_103 : location_info := LocationInfo file_0 66 20 66 21.
-  Definition loc_104 : location_info := LocationInfo file_0 68 20 68 21.
+  Definition loc_104 : location_info := LocationInfo file_0 66 20 66 21.
-  Definition loc_105 : location_info := LocationInfo file_0 67 4 67 14.
+  Definition loc_105 : location_info := LocationInfo file_0 65 4 65 14.
-  Definition loc_106 : location_info := LocationInfo file_0 67 4 67 8.
+  Definition loc_106 : location_info := LocationInfo file_0 65 4 65 8.
-  Definition loc_107 : location_info := LocationInfo file_0 67 4 67 8.
+  Definition loc_107 : location_info := LocationInfo file_0 65 4 65 8.
-  Definition loc_108 : location_info := LocationInfo file_0 67 6 67 7.
+  Definition loc_108 : location_info := LocationInfo file_0 65 6 65 7.
-  Definition loc_109 : location_info := LocationInfo file_0 67 6 67 7.
+  Definition loc_109 : location_info := LocationInfo file_0 65 6 65 7.
-  Definition loc_110 : location_info := LocationInfo file_0 67 17 67 31.
+  Definition loc_110 : location_info := LocationInfo file_0 65 17 65 31.
-  Definition loc_111 : location_info := LocationInfo file_0 69 9 71 3.
+  Definition loc_111 : location_info := LocationInfo file_0 67 9 69 3.
-  Definition loc_112 : location_info := LocationInfo file_0 70 4 70 28.
+  Definition loc_112 : location_info := LocationInfo file_0 68 4 68 28.
-  Definition loc_113 : location_info := LocationInfo file_0 70 4 70 14.
+  Definition loc_113 : location_info := LocationInfo file_0 68 4 68 14.
-  Definition loc_114 : location_info := LocationInfo file_0 70 4 70 8.
+  Definition loc_114 : location_info := LocationInfo file_0 68 4 68 8.
-  Definition loc_115 : location_info := LocationInfo file_0 70 4 70 8.
+  Definition loc_115 : location_info := LocationInfo file_0 68 4 68 8.
-  Definition loc_116 : location_info := LocationInfo file_0 70 6 70 7.
+  Definition loc_116 : location_info := LocationInfo file_0 68 6 68 7.
-  Definition loc_117 : location_info := LocationInfo file_0 70 6 70 7.
+  Definition loc_117 : location_info := LocationInfo file_0 68 6 68 7.
-  Definition loc_118 : location_info := LocationInfo file_0 70 17 70 27.
+  Definition loc_118 : location_info := LocationInfo file_0 68 17 68 27.
-  Definition loc_119 : location_info := LocationInfo file_0 70 17 70 27.
+  Definition loc_119 : location_info := LocationInfo file_0 68 17 68 27.
-  Definition loc_120 : location_info := LocationInfo file_0 70 17 70 21.
+  Definition loc_120 : location_info := LocationInfo file_0 68 17 68 21.
-  Definition loc_121 : location_info := LocationInfo file_0 70 17 70 21.
+  Definition loc_121 : location_info := LocationInfo file_0 68 17 68 21.
-  Definition loc_122 : location_info := LocationInfo file_0 66 5 66 33.
+  Definition loc_122 : location_info := LocationInfo file_0 64 5 64 33.
-  Definition loc_123 : location_info := LocationInfo file_0 66 5 66 15.
+  Definition loc_123 : location_info := LocationInfo file_0 64 5 64 15.
-  Definition loc_124 : location_info := LocationInfo file_0 66 5 66 15.
+  Definition loc_124 : location_info := LocationInfo file_0 64 5 64 15.
-  Definition loc_125 : location_info := LocationInfo file_0 66 5 66 9.
+  Definition loc_125 : location_info := LocationInfo file_0 64 5 64 9.
-  Definition loc_126 : location_info := LocationInfo file_0 66 5 66 9.
+  Definition loc_126 : location_info := LocationInfo file_0 64 5 64 9.
-  Definition loc_127 : location_info := LocationInfo file_0 66 19 66 33.
+  Definition loc_127 : location_info := LocationInfo file_0 64 19 64 33.
-  Definition loc_128 : location_info := LocationInfo file_0 65 14 65 24.
+  Definition loc_128 : location_info := LocationInfo file_0 63 14 63 24.
-  Definition loc_129 : location_info := LocationInfo file_0 65 14 65 24.
+  Definition loc_129 : location_info := LocationInfo file_0 63 14 63 24.
-  Definition loc_130 : location_info := LocationInfo file_0 65 14 65 18.
+  Definition loc_130 : location_info := LocationInfo file_0 63 14 63 18.
-  Definition loc_131 : location_info := LocationInfo file_0 65 14 65 18.
+  Definition loc_131 : location_info := LocationInfo file_0 63 14 63 18.
-  Definition loc_134 : location_info := LocationInfo file_0 64 22 64 32.
+  Definition loc_134 : location_info := LocationInfo file_0 62 22 62 32.
-  Definition loc_135 : location_info := LocationInfo file_0 64 22 64 32.
+  Definition loc_135 : location_info := LocationInfo file_0 62 22 62 32.
-  Definition loc_136 : location_info := LocationInfo file_0 64 22 64 26.
+  Definition loc_136 : location_info := LocationInfo file_0 62 22 62 26.
-  Definition loc_137 : location_info := LocationInfo file_0 64 22 64 26.
+  Definition loc_137 : location_info := LocationInfo file_0 62 22 62 26.
-  Definition loc_138 : location_info := LocationInfo file_0 64 24 64 25.
+  Definition loc_138 : location_info := LocationInfo file_0 62 24 62 25.
-  Definition loc_139 : location_info := LocationInfo file_0 64 24 64 25.
+  Definition loc_139 : location_info := LocationInfo file_0 62 24 62 25.
-  Definition loc_142 : location_info := LocationInfo file_0 61 36 63 3.
+  Definition loc_142 : location_info := LocationInfo file_0 59 36 61 3.
-  Definition loc_143 : location_info := LocationInfo file_0 62 4 62 26.
+  Definition loc_143 : location_info := LocationInfo file_0 60 4 60 26.
-  Definition loc_144 : location_info := LocationInfo file_0 62 11 62 25.
+  Definition loc_144 : location_info := LocationInfo file_0 60 11 60 25.
-  Definition loc_146 : location_info := LocationInfo file_0 61 6 61 34.
+  Definition loc_146 : location_info := LocationInfo file_0 59 6 59 34.
-  Definition loc_147 : location_info := LocationInfo file_0 61 6 61 16.
+  Definition loc_147 : location_info := LocationInfo file_0 59 6 59 16.
-  Definition loc_148 : location_info := LocationInfo file_0 61 6 61 16.
+  Definition loc_148 : location_info := LocationInfo file_0 59 6 59 16.
-  Definition loc_149 : location_info := LocationInfo file_0 61 6 61 10.
+  Definition loc_149 : location_info := LocationInfo file_0 59 6 59 10.
-  Definition loc_150 : location_info := LocationInfo file_0 61 6 61 10.
+  Definition loc_150 : location_info := LocationInfo file_0 59 6 59 10.
-  Definition loc_151 : location_info := LocationInfo file_0 61 8 61 9.
+  Definition loc_151 : location_info := LocationInfo file_0 59 8 59 9.
-  Definition loc_152 : location_info := LocationInfo file_0 61 8 61 9.
+  Definition loc_152 : location_info := LocationInfo file_0 59 8 59 9.
-  Definition loc_153 : location_info := LocationInfo file_0 61 20 61 34.
+  Definition loc_153 : location_info := LocationInfo file_0 59 20 59 34.
  (* Definition of struct [queue_elem]. *)
  Program Definition struct_queue_elem := {|