Skip to content
Snippets Groups Projects
Commit f3d35fe3 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[Aorai] Fixes test script after changes in kernel API

parent 2128aefb
No related branches found
No related tags found
No related merge requests found
...@@ -4,17 +4,15 @@ ...@@ -4,17 +4,15 @@
open Kernel open Kernel
module StdString = String module P = Plugin.Register
(struct
include Plugin.Register
(struct
let name = "aorai testing module" let name = "aorai testing module"
let shortname = "aorai-test" let shortname = "aorai-test"
let help = "utility script for aorai regtests" let help = "utility script for aorai regtests"
end) end)
module TestNumber = module TestNumber =
Zero P.Zero
(struct (struct
let option_name = "-aorai-test-number" let option_name = "-aorai-test-number"
let help = "test number when multiple tests are run over the same file" let help = "test number when multiple tests are run over the same file"
...@@ -22,7 +20,7 @@ module TestNumber = ...@@ -22,7 +20,7 @@ module TestNumber =
end) end)
module InternalWpShare = module InternalWpShare =
Empty_string( P.Empty_string(
struct struct
let option_name = "-aorai-test-wp-share" let option_name = "-aorai-test-wp-share"
let help = "use custom wp share dir (when in internal plugin mode)" let help = "use custom wp share dir (when in internal plugin mode)"
...@@ -30,7 +28,7 @@ module InternalWpShare = ...@@ -30,7 +28,7 @@ module InternalWpShare =
end) end)
module ProveAuxSpec = module ProveAuxSpec =
False( P.False(
struct struct
let option_name = "-aorai-test-prove-aux-spec" let option_name = "-aorai-test-prove-aux-spec"
let help = "use WP + alt-ergo to prove that generated spec and body \ let help = "use WP + alt-ergo to prove that generated spec and body \
...@@ -40,11 +38,11 @@ module ProveAuxSpec = ...@@ -40,11 +38,11 @@ module ProveAuxSpec =
let ok = ref false let ok = ref false
let is_suffix suf str = let is_suffix suf str =
let lsuf = StdString.length suf in let lsuf = String.length suf in
let lstr = StdString.length str in let lstr = String.length str in
if lstr <= lsuf then false if lstr <= lsuf then false
else else
let estr = StdString.sub str (lstr - lsuf) lsuf in let estr = String.sub str (lstr - lsuf) lsuf in
estr = suf estr = suf
let extend () = let extend () =
...@@ -68,7 +66,7 @@ let extend () = ...@@ -68,7 +66,7 @@ let extend () =
let tmpfile = let tmpfile =
Filename.get_temp_dir_name () ^ "/aorai_" ^ Filename.get_temp_dir_name () ^ "/aorai_" ^
(Filename.chop_extension (Filename.chop_extension
(Filename.basename (List.hd (Kernel.Files.get())))) ^ "_" ^ (Filename.basename (List.hd (Kernel.Files.get()):>string))) ^ "_" ^
(string_of_int (TestNumber.get ())) ^ ".i" (string_of_int (TestNumber.get ())) ^ ".i"
in in
let () = let () =
...@@ -87,7 +85,7 @@ let extend () = ...@@ -87,7 +85,7 @@ let extend () =
in in
Project.copy ~selection my_project; Project.copy ~selection my_project;
Project.set_current my_project; Project.set_current my_project;
Files.append_after [ tmpfile ]; Files.append_after [ Filepath.Normalized.of_string tmpfile ];
Constfold.off (); Constfold.off ();
Ast.compute(); Ast.compute();
if ProveAuxSpec.get () then begin if ProveAuxSpec.get () then begin
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment