Skip to content

Commit

Permalink
[hack] Simple model for .hack_enum_label
Browse files Browse the repository at this point in the history
Summary: To make sure that we don't treat $builtins.hack_enum_label() call as unknown

Reviewed By: davidpichardie

Differential Revision:
D69591417

Privacy Context Container: L1208441

fbshipit-source-id: 995a8fbfccef4058b40969417c5267ceb8d5f909
  • Loading branch information
geralt-encore authored and facebook-github-bot committed Feb 13, 2025
1 parent 0f36a26 commit 37b9417
Showing 1 changed file with 9 additions and 0 deletions.
9 changes: 9 additions & 0 deletions infer/src/pulse/PulseModelsHack.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1587,6 +1587,14 @@ let hhbc_concat arg1 arg2 : model =
assign_ret res


let hack_enum_label : model =
let open DSL.Syntax in
start_model
@@ fun () ->
let* any = fresh () in
assign_ret any


let matchers : matcher list =
let open ProcnameDispatcher.Call in
[ -"$builtins" &:: "nondet" <>$$--> lift_model @@ Basic.nondet ~desc:"nondet"
Expand Down Expand Up @@ -1660,5 +1668,6 @@ let matchers : matcher list =
; -"$builtins" &:: "hhbc_iter_get_value" <>$ capt_arg_payload $+ capt_arg_payload
$--> hhbc_iter_get_value
; -"$builtins" &:: "hhbc_iter_next" <>$ capt_arg_payload $+ capt_arg_payload $--> hhbc_iter_next
; -"$builtins" &:: "hack_enum_label" <>--> hack_enum_label
; -"Infer$static" &:: "newUnconstrainedInt" <>$ any_arg $--> hack_unconstrained_int ]
|> List.map ~f:(ProcnameDispatcher.Call.contramap_arg_payload ~f:ValueOrigin.addr_hist)

0 comments on commit 37b9417

Please sign in to comment.