whycpulimit : -s/-h instead of yes/no

whycpulimit : Fix return the status of the prover
gappa       : Fix inversion (should use meta showing
              what musn't be instantiated)

drivers/alt_ergo.drv

@@ -10,7 +10,7 @@ invalid "Invalid"
 unknown "I don't know" "Unknown"
 fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
 time "Valid (%s)"
-time "cpulimit_time : %s s"
+time "why3cpulimit time : %s s"
 
 (* À discuter *)
 transformation "simplify_recursive_definition"

drivers/coq.drv

@@ -5,6 +5,7 @@ filename "%f_%t_%g.v"
 valid 0
 unknown "Error: \\(.*\\)$" "\\1"
 fail "Syntax error: \\(.*\\)$" "\\1"
+time "why3cpulimit time : %s s"
 
 prelude "(* This file is generated by Why3's Coq driver *)"
 prelude "(* Beware! Only edit allowed sections below    *)"

drivers/cvc3.drv

@@ -7,7 +7,7 @@ filename "%f-%t-%g.smt"
 
 valid "unsat"
 unknown "\\bunknown\\b\\|\\bsat\\b" "Unknown"
-time "cpulimit_time : %s s"
+time "why3cpulimit time : %s s"
 
 (* À discuter *)
 transformation "simplify_recursive_definition"

drivers/gappa.drv

@@ -8,7 +8,8 @@ filename "%f-%t-%g.gappa"
 
 valid 0
 unknown "no contradiction was found\\|some enclosures were not satisfied" "Unknown"
-time "cpulimit_time : %s s"
+time "why3cpulimit time : %s s"
+fail "Error: \\(.*\\)" "\\1"
 
 transformation "simplify_recursive_definition"
 transformation "inline_trivial"
@@ -95,7 +96,7 @@ theory real.Real
   meta "inline : no" logic (<=)
   meta "inline : no" logic (>=)
   meta "inline : no" logic (>)
-
+  
   remove prop CommutativeGroup.Comm.Comm
   remove prop CommutativeGroup.Assoc.Assoc
   remove prop CommutativeGroup.Unit_def

drivers/simplify.drv

@@ -7,7 +7,7 @@ filename "%f-%t-%g.sx"
 
 valid "\\bValid\\b"
 unknown "\\bInvalid\\b" "Unknown"
-time "cpulimit_time : %s s"
+time "why3cpulimit time : %s s"
 
 transformation "simplify_recursive_definition"
 transformation "inline_trivial"

drivers/tptp.drv

@@ -10,7 +10,7 @@ timeout "Resource limit exceeded"
 timeout "CPU time limit exceeded"
 unknown "No Proof Found"            "Unknown"
 fail    "Failure.*"                   "\"\\0\""
-time "cpulimit_time : %s s"
+time "why3cpulimit time : %s s"
 (* time    "%h:%m:%s on the problem" *)
 (* time    "Total time[ ]*: %s s" *)
 

drivers/verit.drv

@@ -7,7 +7,7 @@ filename "%f-%t-%g.smt"
 
 valid "^unsat"
 unknown "^\\(unknown\\|sat\\)" "Unknown"
-time "cpulimit_time : %s s"
+time "why3cpulimit time : %s s"
 
 (* À discuter *)
 transformation "simplify_recursive_definition"

drivers/yices.drv

@@ -7,7 +7,7 @@ filename "%f-%t-%g.smt"
 
 valid "\\bunsat\\b"
 unknown "\\bunknown\\b\\|\\bsat\\b\\|feature not supported: non linear problem" "Unknown"
-time "cpulimit_time : %s s"
+time "why3cpulimit time : %s s"
 
 (* À discuter *)
 transformation "simplify_recursive_definition"

drivers/z3.drv

@@ -7,7 +7,7 @@ filename "%f-%t-%g.smt"
 
 valid "^unsat"
 unknown "^\\(unknown\\|sat\\|Fail\\)" "Unknown"
-time "cpulimit_time : %s s"
+time "why3cpulimit time : %s s"
 
 
 (* À discuter *)

share/provers-detection-data.conf

@@ -11,7 +11,7 @@ version_ok = "0.92"
 version_ok = "0.91"
 version_old = "0.9"
 version_old = "0.8"
-command = "why3-cpulimit %t %m yes %e %f"
+command = "why3-cpulimit %t %m -s %e %f 2>&1"
 driver = "drivers/alt_ergo.drv"
 
 [ATP cvc3]
@@ -21,7 +21,7 @@ version_switch = "-version"
 version_regexp = "This is CVC3 version \\([^ \n]+\\)"
 version_ok = "2.2"
 version_old = "2.1"
-command = "why3-cpulimit 0 %m yes %e -timeout %t -lang smt %f 2>&1"
+command = "why3-cpulimit 0 %m -s %e -timeout %t -lang smt %f 2>&1"
 driver = "drivers/cvc3.drv"
 
 [ATP yices]
@@ -32,7 +32,7 @@ version_regexp = "[Yices ]*\\([^ \n]+\\)"
 version_ok = "1.0.27"
 version_old = "1.0.17"
 version_old = "1.0.24"
-command = "why3-cpulimit %t %m yes %e -smt 2>&1"
+command = "why3-cpulimit %t %m -s %e -smt 2>&1"
 driver = "drivers/yices.drv"
 
 [ATP eprover]
@@ -40,7 +40,7 @@ name = "Eprover"
 exec = "eprover"
 version_switch = "--version"
 version_regexp = "E \\([^\n]+\\)"
-command = "why3-cpulimit 0 %m yes %e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f 2>&1"
+command = "why3-cpulimit 0 %m -s %e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f 2>&1"
 driver = "drivers/tptp.drv"
 
 [ATP gappa]
@@ -54,7 +54,7 @@ version_old = "0.12.2"
 version_old = "0.12.1"
 version_old = "0.12.0"
 version_old = "0.11.2"
-command = "why3-cpulimit %t %m yes %e %f 2>&1"
+command = "why3-cpulimit %t %m -s %e %f 2>&1"
 driver = "drivers/gappa.drv"
 
 [ATP simplify]
@@ -67,7 +67,7 @@ version_switch = "-version"
 version_regexp = "Simplify version \\([^ \n,]+\\)"
 version_ok = "1.5.5"
 version_ok = "1.5.4"
-command = "why3-cpulimit %t %m yes %e %f 2>&1"
+command = "why3-cpulimit %t %m -s %e %f 2>&1"
 driver = "drivers/simplify.drv"
 
 [ATP spass]
@@ -75,7 +75,7 @@ name = "Spass"
 exec = "SPASS"
 version_switch = "-TPTP || true"
 version_regexp = "SPASS V \\([^ \n\t]+\\)"
-command = "why3-cpulimit 0 %m yes %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f 2>&1"
+command = "why3-cpulimit 0 %m -s %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f 2>&1"
 driver = "drivers/tptp.drv"
 
 [ATP verit]
@@ -84,7 +84,7 @@ exec = "veriT"
 exec = "verit"
 version_switch = "--help"
 version_regexp = "Version: \\([^ \n\r]+\\)"
-command = "why3-cpulimit %t %m yes %e %f 2>&1"
+command = "why3-cpulimit %t %m -s %e %f 2>&1"
 driver = "drivers/verit.drv"
 
 [ATP z3]
@@ -96,7 +96,7 @@ version_regexp = "Z3 version \\([^ \n\r]+\\)"
 version_ok = "2.2"
 version_old = "2.1"
 version_old = "1.3"
-command = "why3-cpulimit %t %m yes %e -smt %f 2>&1"
+command = "why3-cpulimit %t %m -s %e -smt %f 2>&1"
 driver = "drivers/z3.drv"
 
 [ITP coq]
@@ -110,7 +110,7 @@ version_ok = "8.2pl1"
 version_ok = "8.2"
 version_old = "8.1"
 version_old = "8.0"
-command = "%e %f"
+command = "why3-cpulimit 0 %m -s %e %f"
 driver = "drivers/coq.drv"
 editor = "coqide"
 

src/printer/gappa.ml

@@ -74,6 +74,7 @@ let get_info =
             let real_ge = find_real "infix >=" in
             let real_lt = find_real "infix <" in
             let real_gt = find_real "infix >" in
+            let real_inv = find_real "inv" in
             let find_real_abs = find_th env "real" "Abs" in
             let real_abs = find_real_abs "abs" in
 	    let find_rounding_theory = find_th env "floating_point" "Rounding" in
@@ -90,7 +91,7 @@ let get_info =
                  int_add; int_sub; int_mul;
                  int_le; int_ge; int_lt; int_gt;
 		 int_abs;
-		 real_add; real_sub; real_mul; real_div;
+		 real_add; real_sub; real_mul; real_div; real_inv;
                  real_le; real_ge; real_lt; real_gt;
                  real_abs;
 		 !round_single;

src/tools/cpulimit.c

@@ -43,19 +43,19 @@ int main(int argc, char *argv[]) {
 
   if (argc < 5) {
     fprintf(stderr, "usage: %s <time limit in seconds> \
-<virtual memory limit in MiB> <print time yes|no> <command>\n\
+<virtual memory limit in MiB> <-s|-h> <command>\n\
 a null value sets no limit (keeps the actual limit)\n", argv[0]);
     return EXIT_FAILURE;
   }
 
   /* Fork if requested */
-  if(strcmp("yes",argv[3]) == 0){
+  if(strcmp("-s",argv[3]) == 0){
       int pid = fork ();
       if (pid == -1){
           perror("fork");
           exit(EXIT_FAILURE);
       } else if (pid == 0){
-          /* The child continue to execute the program */
+          /* The child continues to execute the program */
       } else {
           /* The parent will not exit this condition */
           int status;
@@ -64,8 +64,12 @@ a null value sets no limit (keeps the actual limit)\n", argv[0]);
           times(&tms);
           double time = (double)((tms.tms_cutime + tms.tms_cstime + 0.0)
                                  / sysconf(_SC_CLK_TCK));
-          fprintf(stdout, "cpulimit_time : %f s\n",time);
-          return status;
+          fprintf(stdout, "why3cpulimit time : %f s\n",time);
+          if (WIFEXITED(status)){
+              return WEXITSTATUS(status);
+          }
+
+          kill(getpid(),SIGTERM);
       }
   }