Improvements in the READMEs to reflect the new verification tools

[db7]

No description provided.

[radumcostache]

Checking it right now

[JonasOberhauser]

I haven't tried to run the shell snippets, but otherwise it looks good to me.
Is this expected to work with a large array of cmake and ctest versions? Otherwise maybe add a (tested with blah blah version blah...) text?

[radumcostache]

I haven't tried to run the shell snippets, but otherwise it looks good to me.

Is this expected to work with a large array of cmake and ctest versions? Otherwise maybe add a (tested with blah blah version blah...) text?

I believe that the features of cmake/ctest that we are using are basic enough so that the version probably wouldn't matter. However, the versions of the following are crucial:

• Boogie: only the latest release as of today (3.5.5) can handle irreducible control flow (our contribution)
• Z3: there were huge differences with older versions, not sure how newer ones behave (when compared to the one pinned in the Dockerfile)
• The cross compilers: initially we were using an older version of Ubuntu, and whatever version apt was installing for that, @lilith218 and I did not manage to inline the asm code for the builtins with that.

[db7]

• Boogie: only the latest release as of today (3.5.5) can handle irreducible control flow (our contribution)

can you point me to the PR/issue ? I will create a link from the documentation to it

[radumcostache]

• Boogie: only the latest release as of today (3.5.5) can handle irreducible control flow (our contribution)

can you point me to the PR/issue ? I will create a link from the documentation to it

This is the PR: boogie-org/boogie#1032
And this is the Release: https://github.com/boogie-org/boogie/releases/tag/v3.5.5 (don't ask me what is going on with that description :) )

[petemud]

don't ask me what is going on with that description :)

So... What's going on with that description? :D
Why doesn't it mention (arguably) the most important change?

[db7]

don't ask me what is going on with that description :)

So... What's going on with that description? :D Why doesn't it mention (arguably) the most important change?

@petemud @radumcostache -- can you explain me what is going on here ? :-)

[petemud]

I can't explain you, @db7. I can explain to you.

Changelog of release 3.5.5 of Boogie has a bunch about

BigFloat rounding overflow handling in FromRational

and nothing about irreducible control flow.

[db7]

I can't explain you, @db7. I can explain to you.

Got me.

Changelog of release 3.5.5 of Boogie has a bunch about

BigFloat rounding overflow handling in FromRational

and nothing about irreducible control flow.

I see. That is unfortunate. Anyway, we won't forget :D. I added these links to the VERIFICATION.md. If you have any feedback let me know.