Relax restriction on file name suffixes

[xldenis]

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]

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]

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]

Gillian/GillianCore/gil_parser/gil_parsing.ml

Lines 108 to 115 in f599599

	(* Check that the file is of a valid type *)
	let extension = Filename.extension path in
	let prev_normalised = String.equal extension ".ngil" in
	let () = Config.previously_normalised := prev_normalised in
	let () =
	if not (prev_normalised || String.equal extension ".gil") then
	failwith (Printf.sprintf "Error: %s is not a .gil or .ngil file" path)
	in