Skip to content

Commit 7cd3743

Browse files
committed
Use naïve unassume for apron analysis when strengthening disabled
1 parent 3ecae8e commit 7cd3743

File tree

1 file changed

+6
-1
lines changed

1 file changed

+6
-1
lines changed

src/analyses/apron/relationAnalysis.apron.ml

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -740,7 +740,12 @@ struct
740740
in
741741
({ f } : Queries.ask) in
742742
let rel = RD.assert_inv dummyask rel e false (no_overflow ask e_orig) in (* assume *)
743-
let rel = RD.keep_vars rel (List.map RV.local vars) in (* restrict *)
743+
let rel =
744+
if GobConfig.get_bool "ana.apron.strengthening" then
745+
RD.keep_vars rel (List.map RV.local vars) (* restrict *)
746+
else
747+
rel (* naive unassume: will be homogeneous join below *)
748+
in
744749

745750
(* TODO: parallel write_global? *)
746751
let st =

0 commit comments

Comments
 (0)