gobra icon indicating copy to clipboard operation
gobra copied to clipboard

Published 20 hours ago • verified publisher icon viperproject

Making Gobra deterministic

Open viper-admin opened this issue 5 years ago • 3 comments

Created by @Felalolf on 2019-10-08 15:36 Last updated on 2020-07-07 09:09

As discussed in some Viper meeting, it seems to be a good idea to make Gobra deterministic.

For Gobra this means that when Gobra is run sequentially on the same input file with the same flags set Gobra should generate identical Viper files.

viper-admin avatar Oct 08 '19 15:10 viper-admin

@Felalolf commented on 2020-07-07 09:07

One of our students has worked on this. It will be merged eventually. So if determinism is required, then contact me and I will do the merge.

viper-admin avatar Jul 07 '20 09:07 viper-admin

@Felalolf on 2020-07-07 09:09:

  • changed the assignee from (none) to @Felalolf

viper-admin avatar Jul 07 '20 09:07 viper-admin

In theory this issue was fixed in Silas' work. We should add some tests and then the issue can be closed.

Felalolf avatar Sep 30 '20 14:09 Felalolf