Skip to content

Commit

Permalink
[hackc] add hhbc_iter_base model and update hackc version
Browse files Browse the repository at this point in the history
Summary:
a recent change in hackc broke our unit tests, by introducing a new builtin.
We fix the problem by adding a trivial model.

Reviewed By: jvillard

Differential Revision: D55745317

fbshipit-source-id: fb788ea000fe684c1b1f03ffe8a0217ba81d77d9
  • Loading branch information
davidpichardie authored and facebook-github-bot committed Apr 4, 2024
1 parent 30c2603 commit eded1af
Showing 1 changed file with 6 additions and 0 deletions.
6 changes: 6 additions & 0 deletions infer/src/pulse/PulseModelsHack.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1168,6 +1168,11 @@ let hhbc_add x y : model =
assign_ret sum (* unconstrained value *)


let hhbc_iter_base arg : model =
let open DSL.Syntax in
start_model @@ assign_ret arg


let hhbc_iter_init iteraddr keyaddr eltaddr arg : model =
let open DSL.Syntax in
start_model
Expand Down Expand Up @@ -1422,6 +1427,7 @@ let matchers : matcher list =
$--> Vec.vec_from_async
; -"$root" &:: "FlibSL::Dict::from_async" <>$ capt_arg_payload $+ capt_arg_payload
$--> Dict.dict_from_async
; -"$builtins" &:: "hhbc_iter_base" <>$ capt_arg_payload $--> hhbc_iter_base
; -"$builtins" &:: "hhbc_iter_init" <>$ capt_arg_payload $+ capt_arg_payload $+ capt_arg_payload
$+ capt_arg_payload $--> hhbc_iter_init
; -"$builtins" &:: "hhbc_iter_next" <>$ capt_arg_payload $+ capt_arg_payload $+ capt_arg_payload
Expand Down

0 comments on commit eded1af

Please sign in to comment.