From 6051f2a3d86760359a3863f348712002d9fd0d77 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 11 Mar 2024 14:00:27 +0200 Subject: [PATCH] Fix inconsistent strengthening behavior with polyhedra --- src/cdomains/apron/apronDomain.apron.ml | 11 +++++++++-- .../56-witness/25-apron-unassume-strengthening.c | 2 -- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml index 2b8f360bc5..bdec5db221 100644 --- a/src/cdomains/apron/apronDomain.apron.ml +++ b/src/cdomains/apron/apronDomain.apron.ml @@ -639,14 +639,21 @@ struct (* Whether [con1] contains a var in [env]. *) let env_exists_mem_con1 env con1 = try - Lincons1.iter (fun _ var -> - if Environment.mem_var env var then + Lincons1.iter (fun coeff var -> + (* Lincons1 from polyhedra may contain variable with zero coefficient. + These are silently not printed! *) + if not (Coeff.is_zero coeff) && Environment.mem_var env var then raise Not_found ) con1; false with Not_found -> true in + let env_exists_mem_con1 env con1 = + let r = env_exists_mem_con1 env con1 in + if M.tracing then M.trace "apron" "env_exists_mem_con1 %s %s -> %B\n" (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) env) (Lincons1.show con1) r; + r + in (* Heuristically reorder constraints to pass 36/12 with singlethreaded->multithreaded mode switching. *) (* Put those constraints which strictly are in one argument's env first, to (hopefully) ensure they remain. *) let (x_cons1_some_y, x_cons1_only_x) = Array.partition (env_exists_mem_con1 y_env) x_cons1 in diff --git a/tests/regression/56-witness/25-apron-unassume-strengthening.c b/tests/regression/56-witness/25-apron-unassume-strengthening.c index 94765fec4d..bd7d720326 100644 --- a/tests/regression/56-witness/25-apron-unassume-strengthening.c +++ b/tests/regression/56-witness/25-apron-unassume-strengthening.c @@ -18,7 +18,5 @@ int main() { __goblint_check(x >= 0); __goblint_check(x < y); // TODO? Used to work without type bounds: https://github.com/goblint/analyzer/issues/1373. } - - // TODO: Why swapped with polyhedra? return 0; }