Commit 854a4341 authored by Julien Signoles's avatar Julien Signoles
Browse files

[e-acsl:archi] fix bug with VLA

parent 0bc945bf
......@@ -118,10 +118,16 @@ let mk_named_store_stmt name ?str_size vi =
let store = mk_rtl_call ~loc name in
match ty, str_size with
| TArray(_, Some _,_,_), None ->
store [ Cil.evar ~loc vi ; Cil.sizeOf ~loc ty ]
| TPtr(TInt(IChar, _), _), Some size -> store [ Cil.evar ~loc vi ; size ]
| _, None -> store [ Cil.mkAddrOfVi vi ; Cil.sizeOf ~loc ty ]
| _, Some _ -> assert false
store [ Cil.evar ~loc vi; Cil.sizeOf ~loc ty ]
| TPtr(TInt(IChar, _), _), Some size ->
store [ Cil.evar ~loc vi ; size ]
| TPtr _, Some size ->
(* a VLA that has been converted to a pointer by the kernel *)
store [ Cil.evar ~loc vi; size ]
| _, None ->
store [ Cil.mkAddrOfVi vi ; Cil.sizeOf ~loc ty ]
| _, Some _ ->
assert false
let mk_store_stmt ?str_size vi =
mk_named_store_stmt "store_block" ?str_size vi
......@@ -160,6 +166,6 @@ let mk_runtime_check ?(reverse=false) kind kf e p =
(*
Local Variables:
compile-command: "make -C ../.."
compile-command: "make -C ../../../../.."
End:
*)
......@@ -64,6 +64,6 @@ val mk_runtime_check:
(*
Local Variables:
compile-command: "make -C ../.."
compile-command: "make -C ../../../../.."
End:
*)
......@@ -57,7 +57,7 @@ let rec inject_in_init env kf_opt vi off = function
CompoundInit(typ, List.rev l), env
let inject_in_local_init loc env kf vi = function
| ConsInit (fvi, _sz :: _, _) as init
| ConsInit (fvi, sz :: _, _) as init
when Functions.Libc.is_vla_alloc_name fvi.vname ->
(* handle variable-length array allocation via [__fc_vla_alloc]. Here each
instance of [__fc_vla_alloc] is rewritten to [alloca] (that is used to
......@@ -70,7 +70,7 @@ let inject_in_local_init loc env kf vi = function
fvi.vname <- Functions.Libc.actual_alloca;
(* Since we need to pass [vi] by value, cannot use [Misc.mk_store_stmt]
here. Do it manually. *)
let store = Constructor.mk_store_stmt vi in
let store = Constructor.mk_store_stmt ~str_size:sz vi in
let env = Env.add_stmt ~post:true env kf store in
init, env
......
......@@ -38,7 +38,7 @@ int main(int argc, char **argv)
;
__lengthof_arr = (unsigned long)LEN;
int *arr = __builtin_alloca(sizeof(int) * __lengthof_arr);
__e_acsl_store_block((void *)(& arr),(size_t)8);
__e_acsl_store_block((void *)arr,sizeof(int) * __lengthof_arr);
__e_acsl_store_block((void *)(& arr),(size_t)8);
__e_acsl_full_init((void *)(& arr));
i = 0;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment