search

GillianPlatform / Gillian

The Gillian Platform main repository
https://GillianPlatform.github.io
BSD 3-Clause "New" or "Revised" License
78 stars 12 forks source link

Relax restriction on file name suffixes #290

Open xldenis opened 5 months ago

xldenis commented 5 months ago

Currently, Gillian Core seems to error if a file doesn't end in either .gil or .ngil saying:

 Error: ../tests/noproph/list_std.stdout is not a .gil or .ngil file

Could we remove this check? Or at least add a -f FORMAT flag that can be used to force gillian to treat a file as acceptable? As the error message implies, I have plenty of .stdout files containing .gil programs and I would like to load them, changing my suffix is not an option as they are generated by a 3rd party tool.

giltho commented 5 months ago

This can be done at the instantiation level by changing the parse_and_compile function to detect the .stdout extension and not perform any compilation This can also be hidden behind a flag at the instantiation level by extending TargetLangOptions

xldenis commented 5 months ago

This can be done at the instantiation level by changing the parse_and_compile function to detect the .stdout extension and not perform any compilation

Hmm I don't think this is an issue with the instantiation level compilation:

              Called from Command_line__Verification_console.Make.parse_eprog in file "GillianCore/command_line/verification_console.ml", line 60, characters 10-59
              Called from Command_line__Verification_console.Make.process_files in file "GillianCore/command_line/verification_console.ml", line 75, characters 6-40
              Called from Command_line__Verification_console.Make.verify in file "GillianCore/command_line/verification_console.ml", line 122, characters 6-76

The issue here seems entirely localized within Gillian-Core?

xldenis commented 5 months ago

https://github.com/GillianPlatform/Gillian/blob/f5995995deb0334f8b292c07fb15f7bdebde6514/GillianCore/gil_parser/gil_parsing.ml#L108-L115