Skip to content
Snippets Groups Projects
Commit 47162946 authored by David Bühler's avatar David Bühler
Browse files

[Eva] Slightly simplifies reallocarry builtin.

parent 2cca8a49
No related branches found
No related tags found
No related merge requests found
......@@ -860,10 +860,7 @@ let reallocarray_builtin state args =
Eva_utils.warning_once_current
"reallocarray out of bounds: assert(nmemb * size <= SIZE_MAX)";
if size_ok = Alarmset.False (* size always overflows *)
then
let c_values = [Some Cvalue.V.singleton_zero, state] in
let c_clobbered = Base.SetLattice.bottom in
Builtins.Full { c_values; c_clobbered; c_from = None; }
then Builtins.Result [Cvalue.V.singleton_zero]
else
let valid_size =
Cvalue.V.narrow (Cvalue.V.inject_ival (zero_to_max_bytes ())) size
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment