Commit ef7547ec authored by Michael Sammler's avatar Michael Sammler
Browse files

Add mem cast

parent cdac291e
Pipeline #50055 passed with stage
in 20 minutes
......@@ -8,7 +8,8 @@ struct test {
[[rc::returns("{4} @ int<i32>")]]
int container_of_test() {
struct test t = {.a = 1, .b = 2};
struct test t;
t.a = 1; t.b = 2;
int *b = &t.b;
*b = 3;
struct test *pt = container_of(b, struct test, b);
......
......@@ -244,5 +244,8 @@ void fsm_realloc_if_necessary(struct fixed_size_map *m) {
rc_unfold(m2.length);
}
free_array(sizeof(struct item), m->length, m->items);
*m = m2;
// TODO: replace the following by *m = m2; when we support it
m->items = m2.items;
m->count = m2.count;
m->length = m2.length;
}
......@@ -259,7 +259,7 @@ Section code.
f_code := (
<[ "#0" :=
locinfo: loc_2 ;
Return (LocInfoE loc_3 (CopyAllocId (IntOp uintptr_t) (LocInfoE loc_5 (use{it_layout uintptr_t} (LocInfoE loc_6 ("to")))) (LocInfoE loc_7 (use{void*} (LocInfoE loc_8 ("from"))))))
Return (LocInfoE loc_3 (CopyAllocId (IntOp uintptr_t) (LocInfoE loc_5 (use{IntOp uintptr_t} (LocInfoE loc_6 ("to")))) (LocInfoE loc_7 (use{PtrOp} (LocInfoE loc_8 ("from"))))))
]> $
)%E
|}.
......@@ -280,15 +280,15 @@ Section code.
f_init := "#0";
f_code := (
<[ "#0" :=
"l" <-{ it_layout i32 } LocInfoE loc_68 (i2v 0 i32) ;
"r" <-{ it_layout i32 }
LocInfoE loc_64 (use{it_layout i32} (LocInfoE loc_65 ("n"))) ;
"l" <-{ IntOp i32 } LocInfoE loc_68 (i2v 0 i32) ;
"r" <-{ IntOp i32 }
LocInfoE loc_64 (use{IntOp i32} (LocInfoE loc_65 ("n"))) ;
locinfo: loc_12 ;
Goto "#1"
]> $
<[ "#1" :=
locinfo: loc_59 ;
if: LocInfoE loc_59 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_59 ((LocInfoE loc_60 (use{it_layout i32} (LocInfoE loc_61 ("l")))) <{IntOp i32, IntOp i32} (LocInfoE loc_62 (use{it_layout i32} (LocInfoE loc_63 ("r")))))))
if: LocInfoE loc_59 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_59 ((LocInfoE loc_60 (use{IntOp i32} (LocInfoE loc_61 ("l")))) <{IntOp i32, IntOp i32} (LocInfoE loc_62 (use{IntOp i32} (LocInfoE loc_63 ("r")))))))
then
Goto "#2"
else
......@@ -296,11 +296,11 @@ Section code.
Goto "#3"
]> $
<[ "#2" :=
"k" <-{ it_layout i32 }
LocInfoE loc_47 ((LocInfoE loc_48 (use{it_layout i32} (LocInfoE loc_49 ("l")))) +{IntOp i32, IntOp i32} (LocInfoE loc_50 ((LocInfoE loc_51 ((LocInfoE loc_52 (use{it_layout i32} (LocInfoE loc_53 ("r")))) -{IntOp i32, IntOp i32} (LocInfoE loc_54 (use{it_layout i32} (LocInfoE loc_55 ("l")))))) /{IntOp i32, IntOp i32} (LocInfoE loc_56 (i2v 2 i32))))) ;
"k" <-{ IntOp i32 }
LocInfoE loc_47 ((LocInfoE loc_48 (use{IntOp i32} (LocInfoE loc_49 ("l")))) +{IntOp i32, IntOp i32} (LocInfoE loc_50 ((LocInfoE loc_51 ((LocInfoE loc_52 (use{IntOp i32} (LocInfoE loc_53 ("r")))) -{IntOp i32, IntOp i32} (LocInfoE loc_54 (use{IntOp i32} (LocInfoE loc_55 ("l")))))) /{IntOp i32, IntOp i32} (LocInfoE loc_56 (i2v 2 i32))))) ;
locinfo: loc_34 ;
if: LocInfoE loc_34 (Call (LocInfoE loc_36 (use{void*} (LocInfoE loc_37 ("comp")))) [@{expr} LocInfoE loc_38 (use{void*} (LocInfoE loc_40 ((LocInfoE loc_41 (!{void*} (LocInfoE loc_42 ("xs")))) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_43 (use{it_layout i32} (LocInfoE loc_44 ("k"))))))) ;
LocInfoE loc_45 (use{void*} (LocInfoE loc_46 ("x"))) ])
if: LocInfoE loc_34 (Call (LocInfoE loc_36 (use{PtrOp} (LocInfoE loc_37 ("comp")))) [@{expr} LocInfoE loc_38 (use{PtrOp} (LocInfoE loc_40 ((LocInfoE loc_41 (!{PtrOp} (LocInfoE loc_42 ("xs")))) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_43 (use{IntOp i32} (LocInfoE loc_44 ("k"))))))) ;
LocInfoE loc_45 (use{PtrOp} (LocInfoE loc_46 ("x"))) ])
then
locinfo: loc_23 ;
Goto "#5"
......@@ -310,7 +310,7 @@ Section code.
]> $
<[ "#3" :=
locinfo: loc_13 ;
Return (LocInfoE loc_14 (use{it_layout i32} (LocInfoE loc_15 ("l"))))
Return (LocInfoE loc_14 (use{IntOp i32} (LocInfoE loc_15 ("l"))))
]> $
<[ "#4" :=
locinfo: loc_20 ;
......@@ -318,15 +318,15 @@ Section code.
]> $
<[ "#5" :=
locinfo: loc_23 ;
LocInfoE loc_24 ("l") <-{ it_layout i32 }
LocInfoE loc_25 ((LocInfoE loc_26 (use{it_layout i32} (LocInfoE loc_27 ("k")))) +{IntOp i32, IntOp i32} (LocInfoE loc_28 (i2v 1 i32))) ;
LocInfoE loc_24 ("l") <-{ IntOp i32 }
LocInfoE loc_25 ((LocInfoE loc_26 (use{IntOp i32} (LocInfoE loc_27 ("k")))) +{IntOp i32, IntOp i32} (LocInfoE loc_28 (i2v 1 i32))) ;
locinfo: loc_20 ;
Goto "#4"
]> $
<[ "#6" :=
locinfo: loc_30 ;
LocInfoE loc_31 ("r") <-{ it_layout i32 }
LocInfoE loc_32 (use{it_layout i32} (LocInfoE loc_33 ("k"))) ;
LocInfoE loc_31 ("r") <-{ IntOp i32 }
LocInfoE loc_32 (use{IntOp i32} (LocInfoE loc_33 ("k"))) ;
locinfo: loc_20 ;
Goto "#4"
]> $
......@@ -350,12 +350,12 @@ Section code.
f_init := "#0";
f_code := (
<[ "#0" :=
"xi" <-{ void* }
LocInfoE loc_88 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_88 (use{void*} (LocInfoE loc_89 ("x"))))) ;
"yi" <-{ void* }
LocInfoE loc_84 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_84 (use{void*} (LocInfoE loc_85 ("y"))))) ;
"xi" <-{ PtrOp }
LocInfoE loc_88 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_88 (use{PtrOp} (LocInfoE loc_89 ("x"))))) ;
"yi" <-{ PtrOp }
LocInfoE loc_84 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_84 (use{PtrOp} (LocInfoE loc_85 ("y"))))) ;
locinfo: loc_74 ;
Return (LocInfoE loc_75 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_75 ((LocInfoE loc_76 (use{it_layout size_t} (LocInfoE loc_78 (!{void*} (LocInfoE loc_79 ("xi")))))) {IntOp size_t, IntOp size_t} (LocInfoE loc_80 (use{it_layout size_t} (LocInfoE loc_82 (!{void*} (LocInfoE loc_83 ("yi"))))))))))
Return (LocInfoE loc_75 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_75 ((LocInfoE loc_76 (use{IntOp size_t} (LocInfoE loc_78 (!{PtrOp} (LocInfoE loc_79 ("xi")))))) {IntOp size_t, IntOp size_t} (LocInfoE loc_80 (use{IntOp size_t} (LocInfoE loc_82 (!{PtrOp} (LocInfoE loc_83 ("yi"))))))))))
]> $
)%E
|}.
......@@ -373,59 +373,59 @@ Section code.
f_code := (
<[ "#0" :=
locinfo: loc_94 ;
LocInfoE loc_253 ((LocInfoE loc_255 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_256 (i2v 0 i32))) <-{ void* }
LocInfoE loc_253 ((LocInfoE loc_255 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_256 (i2v 0 i32))) <-{ PtrOp }
LocInfoE loc_257 (Call (LocInfoE loc_259 (global_alloc)) [@{expr} LocInfoE loc_260 (i2v (it_layout size_t).(ly_size) size_t) ]) ;
locinfo: loc_95 ;
LocInfoE loc_244 ((LocInfoE loc_246 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_247 (i2v 1 i32))) <-{ void* }
LocInfoE loc_244 ((LocInfoE loc_246 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_247 (i2v 1 i32))) <-{ PtrOp }
LocInfoE loc_248 (Call (LocInfoE loc_250 (global_alloc)) [@{expr} LocInfoE loc_251 (i2v (it_layout size_t).(ly_size) size_t) ]) ;
locinfo: loc_96 ;
LocInfoE loc_235 ((LocInfoE loc_237 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_238 (i2v 2 i32))) <-{ void* }
LocInfoE loc_235 ((LocInfoE loc_237 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_238 (i2v 2 i32))) <-{ PtrOp }
LocInfoE loc_239 (Call (LocInfoE loc_241 (global_alloc)) [@{expr} LocInfoE loc_242 (i2v (it_layout size_t).(ly_size) size_t) ]) ;
locinfo: loc_97 ;
LocInfoE loc_226 ((LocInfoE loc_228 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_229 (i2v 3 i32))) <-{ void* }
LocInfoE loc_226 ((LocInfoE loc_228 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_229 (i2v 3 i32))) <-{ PtrOp }
LocInfoE loc_230 (Call (LocInfoE loc_232 (global_alloc)) [@{expr} LocInfoE loc_233 (i2v (it_layout size_t).(ly_size) size_t) ]) ;
locinfo: loc_98 ;
LocInfoE loc_217 ((LocInfoE loc_219 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_220 (i2v 4 i32))) <-{ void* }
LocInfoE loc_217 ((LocInfoE loc_219 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_220 (i2v 4 i32))) <-{ PtrOp }
LocInfoE loc_221 (Call (LocInfoE loc_223 (global_alloc)) [@{expr} LocInfoE loc_224 (i2v (it_layout size_t).(ly_size) size_t) ]) ;
locinfo: loc_99 ;
LocInfoE loc_209 (!{void*} (LocInfoE loc_211 ((LocInfoE loc_213 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_214 (i2v 0 i32))))) <-{ it_layout size_t }
LocInfoE loc_209 (!{PtrOp} (LocInfoE loc_211 ((LocInfoE loc_213 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_214 (i2v 0 i32))))) <-{ IntOp size_t }
LocInfoE loc_215 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_215 (i2v 0 i32))) ;
locinfo: loc_100 ;
LocInfoE loc_201 (!{void*} (LocInfoE loc_203 ((LocInfoE loc_205 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_206 (i2v 1 i32))))) <-{ it_layout size_t }
LocInfoE loc_201 (!{PtrOp} (LocInfoE loc_203 ((LocInfoE loc_205 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_206 (i2v 1 i32))))) <-{ IntOp size_t }
LocInfoE loc_207 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_207 (i2v 1 i32))) ;
locinfo: loc_101 ;
LocInfoE loc_193 (!{void*} (LocInfoE loc_195 ((LocInfoE loc_197 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_198 (i2v 2 i32))))) <-{ it_layout size_t }
LocInfoE loc_193 (!{PtrOp} (LocInfoE loc_195 ((LocInfoE loc_197 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_198 (i2v 2 i32))))) <-{ IntOp size_t }
LocInfoE loc_199 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_199 (i2v 2 i32))) ;
locinfo: loc_102 ;
LocInfoE loc_185 (!{void*} (LocInfoE loc_187 ((LocInfoE loc_189 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_190 (i2v 3 i32))))) <-{ it_layout size_t }
LocInfoE loc_185 (!{PtrOp} (LocInfoE loc_187 ((LocInfoE loc_189 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_190 (i2v 3 i32))))) <-{ IntOp size_t }
LocInfoE loc_191 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_191 (i2v 3 i32))) ;
locinfo: loc_103 ;
LocInfoE loc_177 (!{void*} (LocInfoE loc_179 ((LocInfoE loc_181 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_182 (i2v 4 i32))))) <-{ it_layout size_t }
LocInfoE loc_177 (!{PtrOp} (LocInfoE loc_179 ((LocInfoE loc_181 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_182 (i2v 4 i32))))) <-{ IntOp size_t }
LocInfoE loc_183 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_183 (i2v 4 i32))) ;
"needle" <-{ it_layout size_t }
"needle" <-{ IntOp size_t }
LocInfoE loc_173 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_173 (i2v 2 i32))) ;
"res" <-{ it_layout i32 }
"res" <-{ IntOp i32 }
LocInfoE loc_161 (Call (LocInfoE loc_163 (global_binary_search)) [@{expr} LocInfoE loc_164 (global_compare_int) ;
LocInfoE loc_165 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_166 (&(LocInfoE loc_167 ("ptrs"))))) ;
LocInfoE loc_168 (i2v 5 i32) ;
LocInfoE loc_169 (&(LocInfoE loc_170 ("needle"))) ]) ;
locinfo: loc_106 ;
assert: (LocInfoE loc_157 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_157 ((LocInfoE loc_158 (use{it_layout i32} (LocInfoE loc_159 ("res")))) ={IntOp i32, IntOp i32} (LocInfoE loc_160 (i2v 3 i32)))))) ;
assert: (LocInfoE loc_157 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_157 ((LocInfoE loc_158 (use{IntOp i32} (LocInfoE loc_159 ("res")))) ={IntOp i32, IntOp i32} (LocInfoE loc_160 (i2v 3 i32)))))) ;
locinfo: loc_107 ;
expr: (LocInfoE loc_107 (Call (LocInfoE loc_149 (global_free)) [@{expr} LocInfoE loc_150 (i2v (it_layout size_t).(ly_size) size_t) ;
LocInfoE loc_151 (use{void*} (LocInfoE loc_153 ((LocInfoE loc_155 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_156 (i2v 0 i32))))) ])) ;
LocInfoE loc_151 (use{PtrOp} (LocInfoE loc_153 ((LocInfoE loc_155 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_156 (i2v 0 i32))))) ])) ;
locinfo: loc_108 ;
expr: (LocInfoE loc_108 (Call (LocInfoE loc_140 (global_free)) [@{expr} LocInfoE loc_141 (i2v (it_layout size_t).(ly_size) size_t) ;
LocInfoE loc_142 (use{void*} (LocInfoE loc_144 ((LocInfoE loc_146 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_147 (i2v 1 i32))))) ])) ;
LocInfoE loc_142 (use{PtrOp} (LocInfoE loc_144 ((LocInfoE loc_146 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_147 (i2v 1 i32))))) ])) ;
locinfo: loc_109 ;
expr: (LocInfoE loc_109 (Call (LocInfoE loc_131 (global_free)) [@{expr} LocInfoE loc_132 (i2v (it_layout size_t).(ly_size) size_t) ;
LocInfoE loc_133 (use{void*} (LocInfoE loc_135 ((LocInfoE loc_137 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_138 (i2v 2 i32))))) ])) ;
LocInfoE loc_133 (use{PtrOp} (LocInfoE loc_135 ((LocInfoE loc_137 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_138 (i2v 2 i32))))) ])) ;
locinfo: loc_110 ;
expr: (LocInfoE loc_110 (Call (LocInfoE loc_122 (global_free)) [@{expr} LocInfoE loc_123 (i2v (it_layout size_t).(ly_size) size_t) ;
LocInfoE loc_124 (use{void*} (LocInfoE loc_126 ((LocInfoE loc_128 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_129 (i2v 3 i32))))) ])) ;
LocInfoE loc_124 (use{PtrOp} (LocInfoE loc_126 ((LocInfoE loc_128 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_129 (i2v 3 i32))))) ])) ;
locinfo: loc_111 ;
expr: (LocInfoE loc_111 (Call (LocInfoE loc_113 (global_free)) [@{expr} LocInfoE loc_114 (i2v (it_layout size_t).(ly_size) size_t) ;
LocInfoE loc_115 (use{void*} (LocInfoE loc_117 ((LocInfoE loc_119 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_120 (i2v 4 i32))))) ])) ;
LocInfoE loc_115 (use{PtrOp} (LocInfoE loc_117 ((LocInfoE loc_119 ("ptrs")) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_120 (i2v 4 i32))))) ])) ;
Return (VOID)
]> $
)%E
......
This diff is collapsed.
......@@ -68,7 +68,7 @@ Section spec.
Global Program Instance btree_t_rmovable : RMovable btree_t :=
{| rmovable patt__ := movable_eq _ _ (btree_t_unfold patt__) |}.
Next Obligation. solve_ty_layout_eq. Qed.
Solve Obligations with solve_ty_layout_eq.
Global Instance btree_t_simplify_hyp_place_inst_generated l_ β_ patt__:
SimplifyHypPlace l_ β_ (patt__ @ btree_t)%I (Some 100%N) :=
......
......@@ -6,34 +6,39 @@ Set Default Proof Using "Type".
(* Generated from [examples/container_of.c]. *)
Section code.
Definition file_0 : string := "examples/container_of.c".
Definition loc_2 : location_info := LocationInfo file_0 11 2 11 35.
Definition loc_3 : location_info := LocationInfo file_0 12 2 12 16.
Definition loc_4 : location_info := LocationInfo file_0 13 2 13 9.
Definition loc_5 : location_info := LocationInfo file_0 14 2 14 86.
Definition loc_6 : location_info := LocationInfo file_0 15 2 15 12.
Definition loc_7 : location_info := LocationInfo file_0 16 2 16 13.
Definition loc_8 : location_info := LocationInfo file_0 16 9 16 12.
Definition loc_9 : location_info := LocationInfo file_0 16 9 16 12.
Definition loc_10 : location_info := LocationInfo file_0 16 9 16 10.
Definition loc_11 : location_info := LocationInfo file_0 15 2 15 7.
Definition loc_12 : location_info := LocationInfo file_0 15 2 15 4.
Definition loc_13 : location_info := LocationInfo file_0 15 2 15 4.
Definition loc_14 : location_info := LocationInfo file_0 15 10 15 11.
Definition loc_15 : location_info := LocationInfo file_0 14 20 14 85.
Definition loc_16 : location_info := LocationInfo file_0 14 35 14 85.
Definition loc_17 : location_info := LocationInfo file_0 14 37 14 57.
Definition loc_18 : location_info := LocationInfo file_0 14 54 14 57.
Definition loc_19 : location_info := LocationInfo file_0 14 54 14 57.
Definition loc_20 : location_info := LocationInfo file_0 14 60 14 83.
Definition loc_23 : location_info := LocationInfo file_0 13 2 13 4.
Definition loc_24 : location_info := LocationInfo file_0 13 3 13 4.
Definition loc_25 : location_info := LocationInfo file_0 13 3 13 4.
Definition loc_26 : location_info := LocationInfo file_0 13 7 13 8.
Definition loc_27 : location_info := LocationInfo file_0 12 11 12 15.
Definition loc_28 : location_info := LocationInfo file_0 12 12 12 15.
Definition loc_29 : location_info := LocationInfo file_0 12 12 12 13.
Definition loc_33 : location_info := LocationInfo file_0 11 24 11 25.
Definition loc_34 : location_info := LocationInfo file_0 11 32 11 33.
Definition loc_2 : location_info := LocationInfo file_0 12 2 12 10.
Definition loc_3 : location_info := LocationInfo file_0 12 11 12 19.
Definition loc_4 : location_info := LocationInfo file_0 13 2 13 16.
Definition loc_5 : location_info := LocationInfo file_0 14 2 14 9.
Definition loc_6 : location_info := LocationInfo file_0 15 2 15 86.
Definition loc_7 : location_info := LocationInfo file_0 16 2 16 12.
Definition loc_8 : location_info := LocationInfo file_0 17 2 17 13.
Definition loc_9 : location_info := LocationInfo file_0 17 9 17 12.
Definition loc_10 : location_info := LocationInfo file_0 17 9 17 12.
Definition loc_11 : location_info := LocationInfo file_0 17 9 17 10.
Definition loc_12 : location_info := LocationInfo file_0 16 2 16 7.
Definition loc_13 : location_info := LocationInfo file_0 16 2 16 4.
Definition loc_14 : location_info := LocationInfo file_0 16 2 16 4.
Definition loc_15 : location_info := LocationInfo file_0 16 10 16 11.
Definition loc_16 : location_info := LocationInfo file_0 15 20 15 85.
Definition loc_17 : location_info := LocationInfo file_0 15 35 15 85.
Definition loc_18 : location_info := LocationInfo file_0 15 37 15 57.
Definition loc_19 : location_info := LocationInfo file_0 15 54 15 57.
Definition loc_20 : location_info := LocationInfo file_0 15 54 15 57.
Definition loc_21 : location_info := LocationInfo file_0 15 60 15 83.
Definition loc_24 : location_info := LocationInfo file_0 14 2 14 4.
Definition loc_25 : location_info := LocationInfo file_0 14 3 14 4.
Definition loc_26 : location_info := LocationInfo file_0 14 3 14 4.
Definition loc_27 : location_info := LocationInfo file_0 14 7 14 8.
Definition loc_28 : location_info := LocationInfo file_0 13 11 13 15.
Definition loc_29 : location_info := LocationInfo file_0 13 12 13 15.
Definition loc_30 : location_info := LocationInfo file_0 13 12 13 13.
Definition loc_33 : location_info := LocationInfo file_0 12 11 12 14.
Definition loc_34 : location_info := LocationInfo file_0 12 11 12 12.
Definition loc_35 : location_info := LocationInfo file_0 12 17 12 18.
Definition loc_36 : location_info := LocationInfo file_0 12 2 12 5.
Definition loc_37 : location_info := LocationInfo file_0 12 2 12 3.
Definition loc_38 : location_info := LocationInfo file_0 12 8 12 9.
(* Definition of struct [test]. *)
Program Definition struct_test := {|
......@@ -56,23 +61,24 @@ Section code.
f_init := "#0";
f_code := (
<[ "#0" :=
"t" <-{ layout_of struct_test }
StructInit struct_test [
("a", LocInfoE loc_33 (i2v 1 i32) : expr) ;
("b", LocInfoE loc_34 (i2v 2 i32) : expr)
] ;
"b" <-{ void* }
LocInfoE loc_27 (&(LocInfoE loc_28 ((LocInfoE loc_29 ("t")) at{struct_test} "b"))) ;
locinfo: loc_4 ;
LocInfoE loc_24 (!{void*} (LocInfoE loc_25 ("b"))) <-{ it_layout i32 }
LocInfoE loc_26 (i2v 3 i32) ;
"pt" <-{ void* }
LocInfoE loc_15 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_16 ((LocInfoE loc_17 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_18 (use{void*} (LocInfoE loc_19 ("b")))))) at_neg_offset{it_layout u8, PtrOp, IntOp size_t} (LocInfoE loc_20 ((OffsetOf (struct_test) ("b"))))))) ;
locinfo: loc_6 ;
LocInfoE loc_11 ((LocInfoE loc_12 (!{void*} (LocInfoE loc_13 ("pt")))) at{struct_test} "a") <-{ it_layout i32 }
LocInfoE loc_14 (i2v 4 i32) ;
locinfo: loc_2 ;
LocInfoE loc_36 ((LocInfoE loc_37 ("t")) at{struct_test} "a") <-{ IntOp i32 }
LocInfoE loc_38 (i2v 1 i32) ;
locinfo: loc_3 ;
LocInfoE loc_33 ((LocInfoE loc_34 ("t")) at{struct_test} "b") <-{ IntOp i32 }
LocInfoE loc_35 (i2v 2 i32) ;
"b" <-{ PtrOp }
LocInfoE loc_28 (&(LocInfoE loc_29 ((LocInfoE loc_30 ("t")) at{struct_test} "b"))) ;
locinfo: loc_5 ;
LocInfoE loc_25 (!{PtrOp} (LocInfoE loc_26 ("b"))) <-{ IntOp i32 }
LocInfoE loc_27 (i2v 3 i32) ;
"pt" <-{ PtrOp }
LocInfoE loc_16 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_17 ((LocInfoE loc_18 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_19 (use{PtrOp} (LocInfoE loc_20 ("b")))))) at_neg_offset{it_layout u8, PtrOp, IntOp size_t} (LocInfoE loc_21 ((OffsetOf (struct_test) ("b"))))))) ;
locinfo: loc_7 ;
Return (LocInfoE loc_8 (use{it_layout i32} (LocInfoE loc_9 ((LocInfoE loc_10 ("t")) at{struct_test} "a"))))
LocInfoE loc_12 ((LocInfoE loc_13 (!{PtrOp} (LocInfoE loc_14 ("pt")))) at{struct_test} "a") <-{ IntOp i32 }
LocInfoE loc_15 (i2v 4 i32) ;
locinfo: loc_8 ;
Return (LocInfoE loc_9 (use{IntOp i32} (LocInfoE loc_10 ((LocInfoE loc_11 ("t")) at{struct_test} "a"))))
]> $
)%E
|}.
......
......@@ -63,10 +63,10 @@ Section code.
f_init := "#0";
f_code := (
<[ "#0" :=
"r" <-{ it_layout u32 }
"r" <-{ IntOp u32 }
LocInfoE loc_38 (UnOp (CastOp $ IntOp u32) (IntOp i32) (LocInfoE loc_38 (i2v 0 i32))) ;
locinfo: loc_31 ;
if: LocInfoE loc_31 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_31 ((LocInfoE loc_32 ((LocInfoE loc_33 (UnOp (CastOp $ IntOp i32) (IntOp u8) (LocInfoE loc_33 (use{it_layout u8} (LocInfoE loc_34 ((LocInfoE loc_35 ("f")) at{struct_flags} "flags")))))) >>{IntOp i32, IntOp i32} (LocInfoE loc_36 (i2v 0 i32)))) &{IntOp i32, IntOp i32} (LocInfoE loc_37 (i2v 1 i32)))))
if: LocInfoE loc_31 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_31 ((LocInfoE loc_32 ((LocInfoE loc_33 (UnOp (CastOp $ IntOp i32) (IntOp u8) (LocInfoE loc_33 (use{IntOp u8} (LocInfoE loc_34 ((LocInfoE loc_35 ("f")) at{struct_flags} "flags")))))) >>{IntOp i32, IntOp i32} (LocInfoE loc_36 (i2v 0 i32)))) &{IntOp i32, IntOp i32} (LocInfoE loc_37 (i2v 1 i32)))))
then
locinfo: loc_23 ;
Goto "#5"
......@@ -76,7 +76,7 @@ Section code.
]> $
<[ "#1" :=
locinfo: loc_16 ;
if: LocInfoE loc_16 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_16 ((LocInfoE loc_17 ((LocInfoE loc_18 (UnOp (CastOp $ IntOp i32) (IntOp u8) (LocInfoE loc_18 (use{it_layout u8} (LocInfoE loc_19 ((LocInfoE loc_20 ("f")) at{struct_flags} "flags")))))) >>{IntOp i32, IntOp i32} (LocInfoE loc_21 (i2v 1 i32)))) &{IntOp i32, IntOp i32} (LocInfoE loc_22 (i2v 1 i32)))))
if: LocInfoE loc_16 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_16 ((LocInfoE loc_17 ((LocInfoE loc_18 (UnOp (CastOp $ IntOp i32) (IntOp u8) (LocInfoE loc_18 (use{IntOp u8} (LocInfoE loc_19 ((LocInfoE loc_20 ("f")) at{struct_flags} "flags")))))) >>{IntOp i32, IntOp i32} (LocInfoE loc_21 (i2v 1 i32)))) &{IntOp i32, IntOp i32} (LocInfoE loc_22 (i2v 1 i32)))))
then
locinfo: loc_8 ;
Goto "#3"
......@@ -86,12 +86,12 @@ Section code.
]> $
<[ "#2" :=
locinfo: loc_5 ;
Return (LocInfoE loc_6 (use{it_layout u32} (LocInfoE loc_7 ("r"))))
Return (LocInfoE loc_6 (use{IntOp u32} (LocInfoE loc_7 ("r"))))
]> $
<[ "#3" :=
locinfo: loc_8 ;
LocInfoE loc_9 ("r") <-{ it_layout u32 }
LocInfoE loc_10 ((LocInfoE loc_11 (use{it_layout u32} (LocInfoE loc_12 ("r")))) +{IntOp u32, IntOp u32} (LocInfoE loc_13 (use{it_layout u32} (LocInfoE loc_14 ("arg2"))))) ;
LocInfoE loc_9 ("r") <-{ IntOp u32 }
LocInfoE loc_10 ((LocInfoE loc_11 (use{IntOp u32} (LocInfoE loc_12 ("r")))) +{IntOp u32, IntOp u32} (LocInfoE loc_13 (use{IntOp u32} (LocInfoE loc_14 ("arg2"))))) ;
locinfo: loc_5 ;
Goto "#2"
]> $
......@@ -101,8 +101,8 @@ Section code.
]> $
<[ "#5" :=
locinfo: loc_23 ;
LocInfoE loc_24 ("r") <-{ it_layout u32 }
LocInfoE loc_25 ((LocInfoE loc_26 (use{it_layout u32} (LocInfoE loc_27 ("r")))) +{IntOp u32, IntOp u32} (LocInfoE loc_28 (use{it_layout u32} (LocInfoE loc_29 ("arg1"))))) ;
LocInfoE loc_24 ("r") <-{ IntOp u32 }
LocInfoE loc_25 ((LocInfoE loc_26 (use{IntOp u32} (LocInfoE loc_27 ("r")))) +{IntOp u32, IntOp u32} (LocInfoE loc_28 (use{IntOp u32} (LocInfoE loc_29 ("arg1"))))) ;
locinfo: loc_16 ;
Goto "#1"
]> $
......
......@@ -51,7 +51,7 @@ Section spec.
Global Program Instance flags_rmovable : RMovable flags :=
{| rmovable patt__ := movable_eq _ _ (flags_unfold patt__) |}.
Next Obligation. solve_ty_layout_eq. Qed.
Solve Obligations with solve_ty_layout_eq.
Global Instance flags_simplify_hyp_place_inst_generated l_ β_ patt__:
SimplifyHypPlace l_ β_ (patt__ @ flags)%I (Some 100%N) :=
......
This diff is collapsed.
......@@ -59,7 +59,7 @@ Section code.
]> $
<[ "#1" :=
locinfo: loc_7 ;
if: LocInfoE loc_7 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_7 ((LocInfoE loc_8 (UnOp (CastOp $ IntOp i32) (IntOp bool_it) (LocInfoE loc_8 (use{it_layout bool_it, ScOrd} (LocInfoE loc_11 ((LocInfoE loc_12 (!{void*} (LocInfoE loc_13 ("latch")))) at{struct_latch} "released")))))) ={IntOp i32, IntOp i32} (LocInfoE loc_14 (UnOp (CastOp $ IntOp i32) (IntOp bool_it) (LocInfoE loc_14 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_15 (i2v 0 i32)))))))))
if: LocInfoE loc_7 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_7 ((LocInfoE loc_8 (UnOp (CastOp $ IntOp i32) (IntOp bool_it) (LocInfoE loc_8 (use{IntOp bool_it, ScOrd} (LocInfoE loc_11 ((LocInfoE loc_12 (!{PtrOp} (LocInfoE loc_13 ("latch")))) at{struct_latch} "released")))))) ={IntOp i32, IntOp i32} (LocInfoE loc_14 (UnOp (CastOp $ IntOp i32) (IntOp bool_it) (LocInfoE loc_14 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_15 (i2v 0 i32)))))))))
then
locinfo: loc_5 ;
Goto "#2"
......@@ -91,7 +91,7 @@ Section code.
f_code := (
<[ "#0" :=
locinfo: loc_18 ;
LocInfoE loc_21 ((LocInfoE loc_22 (!{void*} (LocInfoE loc_23 ("latch")))) at{struct_latch} "released") <-{ it_layout bool_it, ScOrd }
LocInfoE loc_21 ((LocInfoE loc_22 (!{PtrOp} (LocInfoE loc_23 ("latch")))) at{struct_latch} "released") <-{ IntOp bool_it, ScOrd }
LocInfoE loc_24 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_24 (i2v 1 i32))) ;
Return (VOID)
]> $
......
......@@ -33,7 +33,7 @@ Section spec.
Global Program Instance latch_rmovable : RMovable latch :=
{| rmovable patt__ := movable_eq _ _ (latch_unfold patt__) |}.
Next Obligation. solve_ty_layout_eq. Qed.
Solve Obligations with solve_ty_layout_eq.
Global Instance latch_simplify_hyp_place_inst_generated l_ β_ patt__:
SimplifyHypPlace l_ β_ (patt__ @ latch)%I (Some 100%N) :=
......
......@@ -221,7 +221,7 @@ Section code.
f_code := (
<[ "#0" :=
locinfo: loc_2 ;
Return (LocInfoE loc_3 (CopyAllocId (IntOp uintptr_t) (LocInfoE loc_5 (use{it_layout uintptr_t} (LocInfoE loc_6 ("to")))) (LocInfoE loc_7 (use{void*} (LocInfoE loc_8 ("from"))))))
Return (LocInfoE loc_3 (CopyAllocId (IntOp uintptr_t) (LocInfoE loc_5 (use{IntOp uintptr_t} (LocInfoE loc_6 ("to")))) (LocInfoE loc_7 (use{PtrOp} (LocInfoE loc_8 ("from"))))))
]> $
)%E
|}.
......@@ -237,19 +237,19 @@ Section code.
f_code := (
<[ "#0" :=
locinfo: loc_11 ;
LocInfoE loc_36 ((LocInfoE loc_37 (!{void*} (LocInfoE loc_38 ("t")))) at{struct_lock_test} "outside") <-{ it_layout size_t }
LocInfoE loc_36 ((LocInfoE loc_37 (!{PtrOp} (LocInfoE loc_38 ("t")))) at{struct_lock_test} "outside") <-{ IntOp size_t }
LocInfoE loc_39 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_39 (i2v 0 i32))) ;
locinfo: loc_12 ;
LocInfoE loc_32 ((LocInfoE loc_33 (!{void*} (LocInfoE loc_34 ("t")))) at{struct_lock_test} "locked_int") <-{ it_layout size_t }
LocInfoE loc_32 ((LocInfoE loc_33 (!{PtrOp} (LocInfoE loc_34 ("t")))) at{struct_lock_test} "locked_int") <-{ IntOp size_t }
LocInfoE loc_35 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_35 (i2v 0 i32))) ;
locinfo: loc_13 ;
LocInfoE loc_27 ((LocInfoE loc_28 ((LocInfoE loc_29 (!{void*} (LocInfoE loc_30 ("t")))) at{struct_lock_test} "locked_struct")) at{struct_lock_test_inner} "a") <-{ it_layout size_t }
LocInfoE loc_27 ((LocInfoE loc_28 ((LocInfoE loc_29 (!{PtrOp} (LocInfoE loc_30 ("t")))) at{struct_lock_test} "locked_struct")) at{struct_lock_test_inner} "a") <-{ IntOp size_t }
LocInfoE loc_31 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_31 (i2v 0 i32))) ;
locinfo: loc_14 ;
LocInfoE loc_22 ((LocInfoE loc_23 ((LocInfoE loc_24 (!{void*} (LocInfoE loc_25 ("t")))) at{struct_lock_test} "locked_struct")) at{struct_lock_test_inner} "b") <-{ it_layout size_t }
LocInfoE loc_22 ((LocInfoE loc_23 ((LocInfoE loc_24 (!{PtrOp} (LocInfoE loc_25 ("t")))) at{struct_lock_test} "locked_struct")) at{struct_lock_test_inner} "b") <-{ IntOp size_t }
LocInfoE loc_26 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_26 (i2v 10 i32))) ;
locinfo: loc_15 ;
expr: (LocInfoE loc_15 (Call (LocInfoE loc_17 (global_sl_init)) [@{expr} LocInfoE loc_18 (&(LocInfoE loc_19 ((LocInfoE loc_20 (!{void*} (LocInfoE loc_21 ("t")))) at{struct_lock_test} "lock"))) ])) ;
expr: (LocInfoE loc_15 (Call (LocInfoE loc_17 (global_sl_init)) [@{expr} LocInfoE loc_18 (&(LocInfoE loc_19 ((LocInfoE loc_20 (!{PtrOp} (LocInfoE loc_21 ("t")))) at{struct_lock_test} "lock"))) ])) ;
Return (VOID)
]> $
)%E
......@@ -267,8 +267,8 @@ Section code.
f_code := (
<[ "#0" :=
locinfo: loc_42 ;
LocInfoE loc_43 ((LocInfoE loc_44 (!{void*} (LocInfoE loc_45 ("t")))) at{struct_lock_test} "outside") <-{ it_layout size_t }
LocInfoE loc_46 (use{it_layout size_t} (LocInfoE loc_47 ("n"))) ;
LocInfoE loc_43 ((LocInfoE loc_44 (!{PtrOp} (LocInfoE loc_45 ("t")))) at{struct_lock_test} "outside") <-{ IntOp size_t }
LocInfoE loc_46 (use{IntOp size_t} (LocInfoE loc_47 ("n"))) ;
Return (VOID)
]> $
)%E
......@@ -285,7 +285,7 @@ Section code.
f_code := (
<[ "#0" :=
locinfo: loc_50 ;
Return (LocInfoE loc_51 (use{it_layout size_t} (LocInfoE loc_52 ((LocInfoE loc_53 (!{void*} (LocInfoE loc_54 ("t")))) at{struct_lock_test} "outside"))))
Return (LocInfoE loc_51 (use{IntOp size_t} (LocInfoE loc_52 ((LocInfoE loc_53 (!{PtrOp} (LocInfoE loc_54 ("t")))) at{struct_lock_test} "outside"))))
]> $
)%E
|}.
......@@ -302,15 +302,15 @@ Section code.
f_code := (
<[ "#0" :=
locinfo: loc_57 ;
expr: (LocInfoE loc_57 (Call (LocInfoE loc_78 (global_sl_lock)) [@{expr} LocInfoE loc_79 (&(LocInfoE loc_80 ((LocInfoE loc_81 (!{void*} (LocInfoE loc_82 ("t")))) at{struct_lock_test} "lock"))) ])) ;
expr: (LocInfoE loc_57 (Call (LocInfoE loc_78 (global_sl_lock)) [@{expr} LocInfoE loc_79 (&(LocInfoE loc_80 ((LocInfoE loc_81 (!{PtrOp} (LocInfoE loc_82 ("t")))) at{struct_lock_test} "lock"))) ])) ;
locinfo: loc_58 ;
annot: (UnlockA) ;
expr: (LocInfoE loc_73 (&(LocInfoE loc_74 ((LocInfoE loc_75 (!{void*} (LocInfoE loc_76 ("t")))) at{struct_lock_test} "locked_int")))) ;
expr: (LocInfoE loc_73 (&(LocInfoE loc_74 ((LocInfoE loc_75 (!{PtrOp} (LocInfoE loc_76 ("t")))) at{struct_lock_test} "locked_int")))) ;
locinfo: loc_60 ;
LocInfoE loc_68 ((LocInfoE loc_69 (!{void*} (LocInfoE loc_70 ("t")))) at{struct_lock_test} "locked_int") <-{ it_layout size_t }