Skip to content

GitLab

Commit 8b3257a9 authored by Michael Sammler's avatar Michael Sammler Committed by Rodolphe Lepigre
Browse files

Add mem_cast.

parent 349842ae
Pipeline #50447 passed with stage
in 17 minutes and 44 seconds
Expand all Hide whitespace changes
Inline Side-by-side
examples/proofs/binary_search/generated_code.v
View file @ 8b3257a9
......@@ -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
......
examples/proofs/btree/generated_code.v
View file @ 8b3257a9
This diff is collapsed.
examples/proofs/container_of/generated_code.v
View file @ 8b3257a9
......@@ -56,23 +56,23 @@ Section code.
f_init := "#0";
f_code := (
<[ "#0" :=
"t" <-{ layout_of struct_test }
"t" <-{ StructOp struct_test ([ IntOp i32 ; IntOp i32 ]) }
StructInit struct_test [
("a", LocInfoE loc_33 (i2v 1 i32) : expr) ;
("b", LocInfoE loc_34 (i2v 2 i32) : expr)
] ;
"b" <-{ void* }
"b" <-{ PtrOp }
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_24 (!{PtrOp} (LocInfoE loc_25 ("b"))) <-{ IntOp 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"))))))) ;
"pt" <-{ PtrOp }
LocInfoE loc_15 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_16 ((LocInfoE loc_17 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_18 (use{PtrOp} (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_11 ((LocInfoE loc_12 (!{PtrOp} (LocInfoE loc_13 ("pt")))) at{struct_test} "a") <-{ IntOp i32 }
LocInfoE loc_14 (i2v 4 i32) ;
locinfo: loc_7 ;
Return (LocInfoE loc_8 (use{it_layout i32} (LocInfoE loc_9 ((LocInfoE loc_10 ("t")) at{struct_test} "a"))))
Return (LocInfoE loc_8 (use{IntOp i32} (LocInfoE loc_9 ((LocInfoE loc_10 ("t")) at{struct_test} "a"))))
]> $∅
)%E
|}.
......
examples/proofs/flags/generated_code.v
View file @ 8b3257a9
......@@ -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"
]> $
......
examples/proofs/intptr/generated_code.v
View file @ 8b3257a9
This diff is collapsed.
examples/proofs/latch/generated_code.v
View file @ 8b3257a9
......@@ -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)
]> $∅
......
examples/proofs/latch/latch_def.v
View file @ 8b3257a9
......@@ -13,8 +13,8 @@ Section type.
l ↦ LATCH_INIT ={E}=∗ l ◁ₗ{Shr} P @ latch.
Proof.
iIntros (? ?) "Hl".
iApply ty_share => //. unshelve iApply (@ty_ref with "[] Hl") => //.
{ apply _. } { solve_goal. }
iApply ty_share => //. unshelve iApply (@ty_ref with "[] Hl").
{ apply _. } { apply: (UntypedOp struct_latch). } { apply: MCNone. } { solve_goal. } { done. }
rewrite /ty_own_val/=. repeat iSplit => //. rewrite /ty_own_val/=/ty_own_val/=. iSplit => //. by iExists false.
Qed.
End type.
examples/proofs/lock/generated_code.v
View file @ 8b3257a9
......@@ -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 }
LocInfoE loc_71 (use{it_layout size_t} (LocInfoE loc_72 ("n"))) ;
LocInfoE loc_68 ((LocInfoE loc_69 (!{PtrOp} (LocInfoE loc_70 ("t")))) at{struct_lock_test} "locked_int") <-{ IntOp size_t }
LocInfoE loc_71 (use{IntOp size_t} (LocInfoE loc_72 ("n"))) ;
locinfo: loc_61 ;
expr: (LocInfoE loc_61 (Call (LocInfoE loc_63 (global_sl_unlock)) [@{expr} LocInfoE loc_64 (AnnotExpr 1%nat LockA (LocInfoE loc_64 (&(LocInfoE loc_65 ((LocInfoE loc_66 (!{void*} (LocInfoE loc_67 ("t")))) at{struct_lock_test} "lock"))))) ])) ;
expr: (LocInfoE loc_61 (Call (LocInfoE loc_63 (global_sl_unlock)) [@{expr} LocInfoE loc_64 (AnnotExpr 1%nat LockA (LocInfoE loc_64 (&(LocInfoE loc_65 ((LocInfoE loc_66 (!{PtrOp} (LocInfoE loc_67 ("t")))) at{struct_lock_test} "lock"))))) ])) ;
Return (VOID)
]> $∅
)%E
......@@ -328,16 +328,16 @@ Section code.
f_code := (
<[ "#0" :=
locinfo: loc_85 ;
expr: (LocInfoE loc_85 (Call (LocInfoE loc_110 (global_sl_lock)) [@{expr} LocInfoE loc_111 (&(LocInfoE loc_112 ((LocInfoE loc_113 (!{void*} (LocInfoE loc_114 ("t")))) at{struct_lock_test} "lock"))) ])) ;
expr: (LocInfoE loc_85 (Call (LocInfoE loc_110 (global_sl_lock)) [@{expr} LocInfoE loc_111 (&(LocInfoE loc_112 ((LocInfoE loc_113 (!{PtrOp} (LocInfoE loc_114 ("t")))) at{struct_lock_test} "lock"))) ])) ;
locinfo: loc_86 ;
annot: (UnlockA) ;
expr: (LocInfoE loc_105 (&(LocInfoE loc_106 ((LocInfoE loc_107 (!{void*} (LocInfoE loc_108 ("t")))) at{struct_lock_test} "locked_int")))) ;
"ret" <-{ it_layout size_t }
LocInfoE loc_99 (use{it_layout size_t} (LocInfoE loc_100 ((LocInfoE loc_101 (!{void*} (LocInfoE loc_102 ("t")))) at{struct_lock_test} "locked_int"))) ;
expr: (LocInfoE loc_105 (&(LocInfoE loc_106 ((LocInfoE loc_107 (!{PtrOp} (LocInfoE loc_108 ("t")))) at{struct_lock_test} "locked_int")))) ;
"ret" <-{ IntOp size_t }
LocInfoE loc_99 (use{IntOp size_t} (LocInfoE loc_100 ((LocInfoE loc_101 (!{PtrOp} (LocInfoE loc_102 ("t")))) at{struct_lock_test} "locked_int"))) ;
locinfo: loc_89 ;
expr: (LocInfoE loc_89 (Call (LocInfoE loc_94 (global_sl_unlock)) [@{expr} LocInfoE loc_95 (AnnotExpr 1%nat LockA (LocInfoE loc_95 (&(LocInfoE loc_96 ((LocInfoE loc_97 (!{void*} (LocInfoE loc_98 ("t")))) at{struct_lock_test} "lock"))))) ])) ;
expr: (LocInfoE loc_89 (Call (LocInfoE loc_94 (global_sl_unlock)) [@{expr} LocInfoE loc_95 (AnnotExpr 1%nat LockA (LocInfoE loc_95 (&(LocInfoE loc_96 ((LocInfoE loc_97 (!{PtrOp} (LocInfoE loc_98 ("t")))) at{struct_lock_test} "lock"))))) ])) ;
locinfo: loc_90 ;
Return (LocInfoE loc_91 (use{it_layout size_t} (LocInfoE loc_92 ("ret"))))
Return (LocInfoE loc_91 (use{IntOp size_t} (LocInfoE loc_92 ("ret"))))
]> $∅
)%E
|}.
......@@ -354,12 +354,12 @@ Section code.
f_code := (
<[ "#0" :=
locinfo: loc_117 ;
expr: (LocInfoE loc_117 (Call (LocInfoE loc_178 (global_sl_lock)) [@{expr} LocInfoE loc_179 (&(LocInfoE loc_180 ((LocInfoE loc_181 (!{void*} (LocInfoE loc_182 ("t")))) at{struct_lock_test} "lock"))) ])) ;
expr: (LocInfoE loc_117 (Call (LocInfoE loc_178 (global_sl_lock)) [@{expr} LocInfoE loc_179 (&(LocInfoE loc_180 ((LocInfoE loc_181 (!{PtrOp} (LocInfoE loc_182 ("t")))) at{struct_lock_test} "lock"))) ])) ;
locinfo: loc_118 ;
annot: (UnlockA) ;
expr: (LocInfoE loc_173 (&(LocInfoE loc_174 ((LocInfoE loc_175 (!{void*} (LocInfoE loc_176 ("t")))) at{struct_lock_test} "locked_struct")))) ;
expr: (LocInfoE loc_173 (&(LocInfoE loc_174 ((LocInfoE loc_175 (!{PtrOp} (LocInfoE loc_176 ("t")))) at{struct_lock_test} "locked_struct")))) ;
locinfo: loc_165 ;
if: LocInfoE loc_165 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_165 ((LocInfoE loc_166 (use{it_layout size_t} (LocInfoE loc_167 ((LocInfoE loc_168 ((LocInfoE loc_169 (!{void*} (LocInfoE loc_170 ("t")))) at{struct_lock_test} "locked_struct")) at{struct_lock_test_inner} "b")))) >{IntOp size_t, IntOp size_t} (LocInfoE loc_171 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_172 (i2v 0 i32)))))))
if: LocInfoE loc_165 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_165 ((LocInfoE loc_166 (use{IntOp size_t} (LocInfoE loc_167 ((LocInfoE loc_168 ((LocInfoE loc_169 (!{PtrOp} (LocInfoE loc_170 ("t")))) at{struct_lock_test} "locked_struct")) at{struct_lock_test_inner} "b")))) >{IntOp size_t, IntOp size_t} (LocInfoE loc_171 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_172 (i2v 0 i32)))))))
then
locinfo: loc_140 ;
Goto "#2"
......@@ -367,20 +367,20 @@ Section code.
Goto "#3"
]> $
<[ "#1" :=
"ret" <-{ it_layout size_t }
LocInfoE loc_132 (use{it_layout size_t} (LocInfoE loc_133 ((LocInfoE loc_134 ((LocInfoE loc_135 (!{void*} (LocInfoE loc_136 ("t")))) at{struct_lock_test} "locked_struct")) at{struct_lock_test_inner} "a"))) ;
"ret" <-{ IntOp size_t }
LocInfoE loc_132 (use{IntOp size_t} (LocInfoE loc_133 ((LocInfoE loc_134 ((LocInfoE loc_135 (!{PtrOp} (LocInfoE loc_136 ("t")))) at{struct_lock_test} "locked_struct")) at{struct_lock_test_inner} "a"))) ;
locinfo: loc_122 ;
expr: (LocInfoE loc_122 (Call (LocInfoE loc_127 (global_sl_unlock)) [@{expr} LocInfoE loc_128 (AnnotExpr 1%nat LockA (LocInfoE loc_128 (&(LocInfoE loc_129 ((LocInfoE loc_130 (!{void*} (LocInfoE loc_131 ("t")))) at{struct_lock_test} "lock"))))) ])) ;
expr: (LocInfoE loc_122 (Call (LocInfoE loc_127 (global_sl_unlock)) [@{expr} LocInfoE loc_128 (AnnotExpr 1%nat LockA (LocInfoE loc_128 (&(LocInfoE loc_129 ((LocInfoE loc_130 (!{PtrOp} (LocInfoE loc_131 ("t")))) at{struct_lock_test} "lock"))))) ])) ;
locinfo: loc_123 ;
Return (LocInfoE loc_124 (use{it_layout size_t} (LocInfoE loc_125 ("ret"))))
Return (LocInfoE loc_124 (use{IntOp size_t} (LocInfoE loc_125 ("ret"))))
]> $
<[ "#2" :=
locinfo: loc_140 ;
LocInfoE loc_153 ((LocInfoE loc_154 ((LocInfoE loc_155 (!{void*} (LocInfoE loc_156 ("t")))) at{struct_lock_test} "locked_struct")) at{struct_lock_test_inner} "a") <-{ it_layout size_t }
LocInfoE loc_157 ((LocInfoE loc_158 (use{it_layout size_t} (LocInfoE loc_159 ((LocInfoE loc_160 ((LocInfoE loc_161 (!{void*} (LocInfoE loc_162 ("t")))) at{struct_lock_test} "locked_struct")) at{struct_lock_test_inner} "a")))) +{IntOp size_t, IntOp size_t} (LocInfoE loc_163 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_163 (i2v 1 i32))))) ;
LocInfoE loc_153 ((LocInfoE loc_154 ((LocInfoE loc_155 (!{PtrOp} (LocInfoE loc_156 ("t")))) at{struct_lock_test} "locked_struct")) at{struct_lock_test_inner} "a") <-{ IntOp size_t }
LocInfoE loc_157 ((LocInfoE loc_158 (use{IntOp size_t} (LocInfoE loc_159 ((LocInfoE loc_160 ((LocInfoE loc_161 (!{PtrOp} (LocInfoE loc_162 ("t")))) at{struct_lock_test} "locked_struct")) at{struct_lock_test_inner} "a")))) +{IntOp size_t, IntOp size_t} (LocInfoE loc_163 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_163 (i2v 1 i32))))) ;
locinfo: loc_141 ;
LocInfoE loc_142 ((LocInfoE loc_143 ((LocInfoE loc_144 (!{void*} (LocInfoE loc_145 ("t")))) at{struct_lock_test} "locked_struct")) at{struct_lock_test_inner} "b") <-{ it_layout size_t }
LocInfoE loc_146 ((LocInfoE loc_147 (use{it_layout size_t} (LocInfoE loc_148 ((LocInfoE loc_149 ((LocInfoE loc_150 (!{void*} (LocInfoE loc_151 ("t")))) at{struct_lock_test} "locked_struct")) at{struct_lock_test_inner} "b")))) -{IntOp size_t, IntOp size_t} (LocInfoE loc_152 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_152 (i2v 1 i32))))) ;
LocInfoE loc_142 ((LocInfoE loc_143 ((LocInfoE loc_144 (!{PtrOp} (LocInfoE loc_145 ("t")))) at{struct_lock_test} "locked_struct")) at{struct_lock_test_inner} "b") <-{ IntOp size_t }
LocInfoE loc_146 ((LocInfoE loc_147 (use{IntOp size_t} (LocInfoE loc_148 ((LocInfoE loc_149 ((LocInfoE loc_150 (!{PtrOp} (LocInfoE loc_151 ("t")))) at{struct_lock_test} "locked_struct")) at{struct_lock_test_inner} "b")))) -{IntOp size_t, IntOp size_t} (LocInfoE loc_152 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_152 (i2v 1 i32))))) ;
Goto "#1"
]> $
<[ "#3" :=
......
examples/proofs/malloc1/generated_code.v
View file @ 8b3257a9
......@@ -165,7 +165,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
|}.
......@@ -184,16 +184,16 @@ Section code.
f_code := (
<[ "#0" :=
locinfo: loc_11 ;
LocInfoE loc_29 ((LocInfoE loc_30 (!{void*} (LocInfoE loc_31 ("s")))) at{struct_slab} "chunk") <-{ void* }
LocInfoE loc_32 (use{void*} (LocInfoE loc_33 ("p"))) ;
LocInfoE loc_29 ((LocInfoE loc_30 (!{PtrOp} (LocInfoE loc_31 ("s")))) at{struct_slab} "chunk") <-{ PtrOp }
LocInfoE loc_32 (use{PtrOp} (LocInfoE loc_33 ("p"))) ;
locinfo: loc_12 ;
LocInfoE loc_24 ((LocInfoE loc_25 (!{void*} (LocInfoE loc_26 ("s")))) at{struct_slab} "chunksize") <-{ it_layout size_t }
LocInfoE loc_27 (use{it_layout size_t} (LocInfoE loc_28 ("chunksize"))) ;
LocInfoE loc_24 ((LocInfoE loc_25 (!{PtrOp} (LocInfoE loc_26 ("s")))) at{struct_slab} "chunksize") <-{ IntOp size_t }
LocInfoE loc_27 (use{IntOp <