Goto instrument loop unwinding

[danpoe]

Loop unwinding with:

• partial loops, assume, assert, rest loops
• unwindsets

[danpoe]

The Linux builds now also work with a new travis.yml file that provides a more recent version of libstdc++.

[kroening]

May I ask for some reasonable squashing of commits, please?

[danpoe]

Ok, done.

[tautschnig]

As in other places just strings are thrown (and then also caught) I would suggest to use
throw "split string did not generate exactly 2 parts";
(and drop #include <stdexcept>)

[tautschnig]

I was surprised to see the quotes, see below for a suggestion on how to get rid of them.

[tautschnig]

If the testfile were required to be the first (instead of the last) argument then the code could be simplified and all the quotes would become unnecessary. More below.

[danpoe]

Doesn't test.pl always pass the testfile as the last argument?

[tautschnig]

So maybe test.pl should be tweaked to simplify such scripts? Else there could be a brief options parser in this code to extract the last argument from $@.

[tautschnig]

Use [ -z $# ] if moving the file argument into the first position and add || [ ! -s $1 ] to ensure it's a valid file(name).

[tautschnig]

To address both the argument swapping and add support for path names containing "." use:

name=$(echo $1 | sed 's/\.[^\.]*$//')
shift

[tautschnig]

k is unsigned, this is trivially true.

[tautschnig]

k is unsigned

[tautschnig]

That's a fresh goto_programt, should be trivially true?!

[tautschnig]

If I read the code correctly, this is the else case of k!=0 - should be trivially true.

[tautschnig]

Nit: just one blank line

[tautschnig]

danpoe commented on this pull request. > @@ -1324,6 +1360,10 @@ void goto_instrument_parse_optionst::help() "Semantic transformations:\n" " --nondet-volatile makes reads from volatile variables non-deterministic\n" " --unwind <n> unwinds the loops <n> times\n" + " --unwindset L:B,... unwind loop L with a bound of B\n" + " --partial-loops permit paths with partial loops\n" + " --unwinding-assertions generate unwinding assertions\n" + " --rest-loops add loop for remaining iterations after unwound part\n" How about "--continuation-loops"? It's not perfect either but at least gives some idea about what it does.

I do like this suggestion if it weren't for "continuation" to have a well-defined meaning in programming languages already. Maybe "--continue-as-loops" ? Best, Michael

[danpoe]

Ok, I think I've addressed everything.

[tautschnig]

I've added some nice-to-have notes.

[tautschnig]

I would suggest to place this in the unit/ top-level folder.

[danpoe]

Ok, I've added this to the unit tests folder.

[tautschnig]

I'm a bit surprised this works without std::, but it has done before. Maybe use safe_string2int so that we can later put in std::stoi across the codebase?

[danpoe]

I've changed this to safe_string2int().

[tautschnig]

Did you intentionally add .travis.yml changes to this pull request? (I am in favour of those changes, just asking.)

[danpoe]

I'm using some new versions of methods of, e.g., std::set that were added in C++11. This didn't compile with the old travis file as the STL version it used for the Linux builds was too old.

[tautschnig]

Ok, thanks for clarifying!

[tautschnig]

Unless anyone else voices concerns, it should just be a rebase that's blocking a merge.

[kroening]

should that be ssize_t?

[kroening]

Or use some reverse iterator?

[danpoe]

I've used a reverse iterator for this now.

[kroening]

This unfortunately needs to include widen() on WIN32, or Unicode filenames won't work.

[danpoe]

This is now rebased and I've addressed the additional comments.