Skip to content

Commit

Permalink
Refine the abstract domain of values (#490)
Browse files Browse the repository at this point in the history 
Introduce a `Num p` abstract value that stands for any number (but no
pointers), with provenance `p`.  In non-strict mode, this makes the
value analysis more precise than using `Ifptr p` for the same purpose,
like we did before.

Also: minor simplifications and cleanups in the management of provenance.
In strict mode, instead of setting all provenances to `Pbot`, just
propagate them but ignore them in `aptr_of_aval`.  Simplify
`vnormalize` and its proof consequently.

Also: more precise definition of vlub, without a catch-all Vtop case.
  • Loading branch information
@xavierleroy
xavierleroy committed May 25, 2023
1 parent 94d2111 commit 8d5a9df
Showing 1 changed file with 209 additions and 191 deletions.
Loading

1 comment on commit 8d5a9df

@monniaux
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I confirm that this fixes the issues we had where CompCert did not see that accesses to arrays outside of the current stackframe could not interfere with variables in the current stackframe. Thank you.

Please sign in to comment.