search

PrincetonUniversity / VST

Verified Software Toolchain
https://vst.cs.princeton.edu
Other
425 stars 91 forks source link

fix most of floyd/forward.v #694

Closed rinshankaihou closed 12 months ago

rinshankaihou commented 12 months ago

floyd/forward.v is mostly fixed, still need to fix some of its libraries.

andrew-appel commented 12 months ago

I suggest, in addition to the standard CI run at github, you also do "make all" locally in 32-bit mode, which runs several other test cases. Before doing that, you may need to initialize some submodules (FCF, etc.) on which those test cases rely.

andrew-appel commented 12 months ago

(of course, this can wait until you have made more progress on the basic test cases)

rinshankaihou commented 12 months ago

I suggest, in addition to the standard CI run at github, you also do "make all" locally in 32-bit mode, which runs several other test cases. Before doing that, you may need to initialize some submodules (FCF, etc.) on which those test cases rely.

I will keep that in mind, but as of now there is still some work to be done before the proof of any example (even floyd_test.c) works. By fixed I really mean that the file compiles but the tactics are most probably not functioning properly :)