Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Grammar clarifications, particularly \in and \subset #58

Merged
merged 3 commits into from Jul 22, 2019

Conversation

@davidcok
Copy link
Contributor

commented Jun 24, 2019

Various grammar clarifications: precedence of \in and \subset; description of some potentially confusing points; some renaming for consistency.

@davidcok davidcok requested a review from pbaudin Jun 24, 2019

term.tex Outdated Show resolved Hide resolved
@vprevosto
Copy link
Member

left a comment

My only point is about the introduction of update to a range of cells.

@davidcok

This comment has been minimized.

Copy link
Contributor Author

commented Jul 11, 2019

@vprevosto

This comment has been minimized.

Copy link
Member

commented Jul 11, 2019

I agree that writing such terms is probably easier than a universal quantification. I was more concerned about what tools could do with that afterwards (especially the \lambda variant), but the ACSL manual is not supposed to worry too much about that. Still, I'd rather not have that in the basic terms but at a later stage.

@davidcok

This comment has been minimized.

Copy link
Contributor Author

commented Jul 11, 2019

@davidcok

This comment has been minimized.

Copy link
Contributor Author

commented Jul 11, 2019

@vprevosto

This comment has been minimized.

Copy link
Member

commented Jul 11, 2019

Sounds good. I'll commit something in this direction.

@vprevosto vprevosto force-pushed the cok-edits branch from 5f1a2c6 to 3b9ad39 Jul 11, 2019

@vprevosto

This comment has been minimized.

Copy link
Member

commented Jul 11, 2019

OK, ranges are now in the tsets section and array slice updates in the higher-order one. While writing an example for the latter, I did notice that array initialization wasn't extremely well described in the document (section 2.2.7 merely indicates that we use C designated initializers syntax). I've added a sentence to indicate that it is possible to have ranges (and \lambdas as well) there too, but at some point having proper grammar entries for both the standard designated initialization and the range-based one would be desirable (maybe not in this PR, though).

@pbaudin

This comment has been minimized.

Copy link
Contributor

commented Jul 18, 2019

That is ok for me and have only one question about the "functional update" & "offset extension" implemented into Frama-C. Do we add them into ACSL ?

@davidcok

This comment has been minimized.

Copy link
Contributor Author

commented Jul 18, 2019

@pbaudin

This comment has been minimized.

Copy link
Contributor

commented Jul 19, 2019

David,
The implemented syntax for the offset in updates is the one you use in initializers. The Frama C implementation tranforms an update with a compound offset in several updates with elementary offsets (those described into the actual ACSL document). That eases the work of Frama-C plugins, but that transformation allows ranges only for the last offset. There is below an example accepted by Frama-C since a long time:

struct st_c { int t[10] ; int c ;} ;
//@ logic struct st_c update1_idx_in_field (struct st_c a, integer idx, int x) = { a \with .t[idx] = x };

struct st_b { struct st_c c ; };
//@ logic struct st_b update2_idx_in_field (struct st_b a, integer idx, int x) = { a \with .c.t[idx] = x };
//@ logic struct st_b update2_range_in_field (struct st_b a, integer idx, int x) = { a \with .c.t[0..idx] = x };

//@ type ST10 = struct st_c [10];
//@ logic ST10 update3_field_at_idx (ST10 a, integer idx, int x) = { a \with [idx].c = x };

Unfortunately, as said before, the next update is not implemented into Frama-C.

//@ logic ST10 update3_field_in_range (ST10 a, integer idx, int x) = { a \with [0..idx].c = x };
// [kernel:annot-error] exemple.i: Warning:  range is only allowed for last offset. Ignoring global annotation

It could be nice to add this extension into the ACSL document. It is up to you.

@vprevosto

This comment has been minimized.

Copy link
Member

commented Jul 19, 2019

@pbaudin while I agree that allowing explicitly in the document a designator list instead of a single designator would be nice to have, I tend to think that this is relatively independent from this merge request (especially as the newly introduced range designators can only be put at the end of such a list). I'm thus inclined towards merging the current state and leaving designator lists for a later PR.

@vprevosto vprevosto self-assigned this Jul 22, 2019

@vprevosto vprevosto merged commit e0dbca4 into master Jul 22, 2019

@vprevosto vprevosto deleted the cok-edits branch Jul 22, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
3 participants
You can’t perform that action at this time.