Test verify-c-common docker on windows

[priyasiddharth]

siddharth  10:08
TL;DR: Does anyone have experience running verify-c-common/seahorn docker on windows
@Liam Metke is able to build aws-c-common and verify-c-common on windows + docker. When we try to run ninja test , we get failing tests  (some are passing).
@Alex Chen tried the docker on mac and it worked for him. I tried local seahorn + verify-c-common and it works so I am thinking it might be an issue on windows.
Wondering if windows+verify-c-common/seahorn has been tested before? (edited) 

siddharth  10:16
I've given @Liam Metke access to lilla-my.cs to unblock him

arie  23:52
no, @Liam Metke is our first Windows user. I am surprised that there are issues since docker is supposed to run on a VM so completely protected from host machine
23:52
worth while tracking this down since it might be some underlying issue that is only appearing on @Liam Metke setup
23:53
I want to try Windows setup myself, but, unfortunately, while I have a suitable machine, I don't have cycles for that at the moment
23:53
for debugging, I would take a test that fails, and try to identify what is the difference
23:53
you can generate VC in smt2, and then run the result on windows and linux -- we would expect same results
23:54
we would expect VCs to be syntactically the same -- although they don't have to due to non-determinism in some order of expressions when VCs are produced
23:54
I would then compare llvm bitcode files starting with the input to seahorn binary. I expect them to be identical between windows and linux -- these are deterministic
23:55
then we can take it from there
23:55
I would start with simplest possible example. So start with smallest failing test. Then try, by hand, to reduce the number of assertions, until there are as few as possible while still failing
23:56
I'd start by replacing fpf to bpf , i.e., removing auto-generated memory safety checks
23:56
then, remove hand inserted assertions one-by-one