Ensure that compound literals with array type have checked type in checked scopes. #395
Comments
|
Completed by PR #396. |
dopelsunce
pushed a commit
to dopelsunce/checkedc-clang
that referenced
this issue
Sep 28, 2020
checkedc#395) This changes simplifies the description of bounds declaration checking to use read/write sets of pending variable sets. Currently we are using a notion of pending variables in the description of checking of bounds declarations. They are computed by another function that is called during checking. This doesn't extend well to lvalue expressions because lvalue expressions depend on variables, which may be modified within an expression. This change replaces pending variables with read/write summaries. This allows a bottom computation of a summary of the effects of an expression. We can then determine if the read/write summary for expression with an unspecified order of evaluation with respect to each other conflict. The read/write summaries for lvalue expressions can use variables defined in known frames of reference (states after an expression is evaluated). There are some examples that still need to be updated.
sulekhark
pushed a commit
that referenced
this issue
Feb 27, 2021
* Fixing issue: correctcomputation#390 * Adding -verify
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
A compound literal with array type has the form
(T[n]) { e1, e2, e3, ... }. We need to make sure that the array type ends up being checked in a checked scope.We can either require (1) that the array type be completely checked or (2) convert any unchecked array type to the corresponding checked array type and verify that the resulting type is completely checked. I am leaning toward the second option because it'll be less typing for programmers.
The text was updated successfully, but these errors were encountered: