search

rse-verification / interface-specification-propagator

GNU General Public License v2.0
0 stars 0 forks source link

Eva api update #1

Closed Ostbuggen closed 6 months ago

Ostbuggen commented 7 months ago

ISP has been updated for Frama-c 28.1

The deprecated API calls to the prior version of Eva has been updated. ISP now operates with the Eva.Results.request type instead of Db.Value.state when handling results of the Eva analysis. Additionally, a folder of general test cases has been added to the repo with oracles corresponding to the old version of ISP, with some differences.

Differences from old version

In the old version of Eva, when arrays had different requirements for different elements, Eva would propagate the most stringent of these requirements to all of the elements of the array. This bug has been fixed and as a result ISP produces different results in these situations from its earlier version. Otherwise there have been no differences in test results

One old API call could not be fully replicated due to changes in the API. There has been no effect on any of the tests as a result of this but it should be noted in case it causes trouble down the road.

Ostbuggen commented 7 months ago

Good work. Does this only work on V.28> now? I'm not sure that we should deprecate V.27 and less right now. Do you agree @woosh?

I think this will work for V.26 and forward. I'll test that before we merge.

Ostbuggen commented 7 months ago

Good work. Does this only work on V.28> now? I'm not sure that we should deprecate V.27 and less right now. Do you agree @woosh?

I think this will work for V.26 and forward. I'll test that before we merge.

It works for v.26 and forward. There are some slight differences in the test oracles (v28 Eva prints 3 fewer lines on execution than v27) but in terms of functionality it all looks good. Additionally the oracles for the tests that produce errors produce a different backtrace than what is in this repo when run from a container, as I worked in my WSL instead of in the auto-deduct container.

woosh commented 6 months ago

Approved! Merge it :)