diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index 5d66659b43..90fd6037fa 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -52,17 +52,23 @@ struct (* Functions for manipulating globals as temporary locals. *) let read_global ask getg st g x = - if ThreadFlag.has_ever_been_multi ask then - Priv.read_global ask getg st g x - else ( - let rel = st.rel in - (* If it has escaped and we have never been multi-threaded, we can still refer to the local *) - let g_var = if g.vglob then RV.global g else RV.local g in - let x_var = RV.local x in - let rel' = RD.add_vars rel [g_var] in - let rel' = RD.assign_var rel' x_var g_var in + let x_var = RV.local x in + let rel' = + if ThreadFlag.has_ever_been_multi ask then + Priv.read_global ask getg st g x + else ( + let rel = st.rel in + (* If it has escaped and we have never been multi-threaded, we can still refer to the local *) + let g_var = if g.vglob then RV.global g else RV.local g in + let rel' = RD.add_vars rel [g_var] in + let rel' = RD.assign_var rel' x_var g_var in + rel' + ) + in + if (GobConfig.get_bool "exp.volatiles_are_top" && BaseUtil.is_always_unknown g) || GobConfig.get_bool "exp.globs_are_top" then + RD.forget_vars rel' [x_var] + else rel' - ) module VH = BatHashtbl.Make (Basetype.Variables) diff --git a/tests/regression/36-apron/100-volatiles-are-top.c b/tests/regression/36-apron/100-volatiles-are-top.c new file mode 100644 index 0000000000..725de08430 --- /dev/null +++ b/tests/regression/36-apron/100-volatiles-are-top.c @@ -0,0 +1,19 @@ +// SKIP PARAM: --set ana.activated[+] apron --set ana.apron.domain interval --enable exp.volatiles_are_top +// Test that exp.volatiles_are_top is respected by the relational (apron) analysis. +// volatile and extern variables should be treated as top when read. +#include + +extern int ext; +volatile int vol; + +int main(void) { + ext = 5; + int x = ext; // x should be top: ext is extern, exp.volatiles_are_top is on + __goblint_check(x == 5); // UNKNOWN! + + vol = 3; + int y = vol; // y should be top: vol is volatile, exp.volatiles_are_top is on + __goblint_check(y == 3); // UNKNOWN! + + return 0; +}