Commit cdf7be7f authored by Francois Bobot's avatar Francois Bobot

main.ml Remove the sanitizer for the filename

parent 5a420f68
......@@ -163,7 +163,7 @@ bin/top: $(CMO)
test: bin/why.byte
mkdir -p output_why3
ocamlrun -bt bin/why.byte -I theories/ --driver drivers/why3.drv \
--output-dir output_why3 src/test.why
--output-dir output_why3 --all-goals src/test.why
bin/why.byte --driver drivers/alt_ergo.drv -I theories/ \
--output-file - --goal Test.G src/test.why --timeout 3
bin/why.byte --driver drivers/alt_ergo.drv -I theories/ \
......
......@@ -175,8 +175,8 @@ let extract_goals ?filter =
(th,task,drv)) l in
List.rev_append l acc
let file_sanitizer =
Ident.sanitizer Ident.char_to_alnumus Ident.char_to_alnumus
let file_sanitizer = None (* We should remove which character? *)
(* Ident.sanitizer Ident.char_to_alnumus Ident.char_to_alnumus*)
let print_theory_namespace fmt th =
let module T = struct
......@@ -329,9 +329,9 @@ let () =
exit 0
end;
let src_filename_printer = Ident.create_ident_printer
~sanitizer:file_sanitizer [] in
?sanitizer:file_sanitizer [] in
let dest_filename_printer = Ident.create_ident_printer
~sanitizer:file_sanitizer [] in
?sanitizer:file_sanitizer [] in
Queue.iter (do_file env drv src_filename_printer dest_filename_printer)
files
with e when not !debug ->
......
(* test file *)
theory Bug
use import int.Int
type t
end
theory Test
use import int.Int
logic id(x: int) : int = x
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment