[c-parser] remove continue statement

[isubasinghe]

I needed to make this change to make the C-parser accept the code. Not entirely sure why the C-parser blew up when it saw the continue statement, I am unsure if this is a bug in the C-parser or just not supported by it.

[Ivan-Velickovic]

I'd like to understand why continue is not supported/working first.

[isubasinghe]

I'd like to understand why continue is not supported/working first.

Yeah sounds good, I think @lsf37 might know the answer to this, I'll leave this as it is until Gerwin returns from leave and addresses this.

[Xaphiosis]

It would be helpful to see how it "blew up". The C parser itself does support continue, at least as much as is seen in https://github.com/seL4/l4v/blob/master/tools/c-parser/testfiles/breakcontinue.c There might be an interplay here between the continue, switch and break in some manner, but I'm just guessing via a quick glance at the diff

[isubasinghe]

It would be helpful to see how it "blew up". The C parser itself does support continue, at least as much as is seen in https://github.com/seL4/l4v/blob/master/tools/c-parser/testfiles/breakcontinue.c There might be an interplay here between the continue, switch and break in some manner, but I'm just guessing via a quick glance at the diff

Ah thanks for the comment, not entirely sure what caused it to error out, I just bisected through the code until I found out that rewriting the continue statement makes the C parser accept the C code.

I will try and get more helpful output next week and update here, got a bunch of deadlines to worry about this week.

[Ivan-Velickovic]

Did we find out what the problem was?

[lsf37]

continue is definitely supported, so it would be good to figure out what is going on. This change seems to be doing a whole lot of other stuff too, though. Could it be somewhere in there?

[isubasinghe]

Sorry this is on my (fairly large) todo list. All the information I have for now is this:

When all the debug related functions and statements were stripped out, the C parser did end up working. I cannot give an estimate as to when I will get back to this issue, this is somewhat low priority for me until the March deadline is over with.

[lsf37]

Sorry this is on my (fairly large) todo list. All the information I have for now is this:

When all the debug related functions and statements were stripped out, the C parser did end up working.

That makes more sense -- I don't know how putc is defined/handled, but we are avoiding string literals and printing in the kernel, so at least those kinds of things would be much less tested. Would still be good to figure it out at some point.

I cannot give an estimate as to when I will get back to this issue, this is somewhat low priority for me until the March deadline is over with.

Ok, no hurry.

[isubasinghe]

When all the debug related functions and statements were stripped out, the C parser did end up working.

This statement was incorrect, apologies, it was a while since I looked at this, the issue isn't actually with the C parser but the translation to GraphLang.

I've added the program here: https://gist.github.com/isubasinghe/b8fb5abb5db9b6c769ad97c3e2b63866

Here is the export script: https://gist.github.com/isubasinghe/0a568ff2060443b8b43bf23474c37c55

[Ivan-Velickovic]

Closing because @isubasinghe won't be pursuing this anymore and we are likely looking at a change to verification tooling that would not need this patch.

If we do need it we can always re-open.