Commit 1a1bcbab authored by MARCHE Claude's avatar MARCHE Claude

nightly bench: show in the subject of the mail if there are diffs or not

parent cf308ded
......@@ -107,6 +107,7 @@ diff -u $PREVIOUS $OUT &> $DIFF
if test "$?" == 0 ; then
echo "---------- No difference with last bench ---------- " >> $REPORT
else
SUBJECT="$SUBJECT (with new differences)"
if expr `cat $DIFF | wc -l` '>=' `cat $OUT | wc -l` ; then
echo "------- Diff with last bench is larger than the bench itself ------" >> $REPORT
else
......
......@@ -443,7 +443,7 @@ let warn_dubious_axiom uc k p syms =
p.id_string
with Exit -> ()
let add_decl uc d =
let add_decl ?(warn=true) uc d =
check_decl_opacity d; (* we don't care about tasks *)
let uc = add_tdecl uc (create_decl d) in
match d.d_node with
......@@ -453,7 +453,7 @@ let add_decl uc d =
| Dlogic dl -> List.fold_left add_logic uc dl
| Dind (_, dl) -> List.fold_left add_ind uc dl
| Dprop ((k,pr,_) as p) ->
warn_dubious_axiom uc k pr.pr_name d.d_syms;
if warn then warn_dubious_axiom uc k pr.pr_name d.d_syms;
add_prop uc p
(** Declaration constructors + add_decl *)
......@@ -463,7 +463,8 @@ let add_data_decl uc dl = add_decl uc (create_data_decl dl)
let add_param_decl uc ls = add_decl uc (create_param_decl ls)
let add_logic_decl uc dl = add_decl uc (create_logic_decl dl)
let add_ind_decl uc s dl = add_decl uc (create_ind_decl s dl)
let add_prop_decl uc k p f = add_decl uc (create_prop_decl k p f)
let add_prop_decl ?warn uc k p f =
add_decl ?warn uc (create_prop_decl k p f)
(** Use *)
......
......@@ -140,14 +140,15 @@ val restore_path : ident -> string list * string * string list
val create_decl : decl -> tdecl
val add_decl : theory_uc -> decl -> theory_uc
val add_decl : ?warn:bool -> theory_uc -> decl -> theory_uc
val add_ty_decl : theory_uc -> tysymbol -> theory_uc
val add_data_decl : theory_uc -> data_decl list -> theory_uc
val add_param_decl : theory_uc -> lsymbol -> theory_uc
val add_logic_decl : theory_uc -> logic_decl list -> theory_uc
val add_ind_decl : theory_uc -> ind_sign -> ind_decl list -> theory_uc
val add_prop_decl : theory_uc -> prop_kind -> prsymbol -> term -> theory_uc
val add_prop_decl :
?warn:bool -> theory_uc -> prop_kind -> prsymbol -> term -> theory_uc
(** {2 Use} *)
......
......@@ -2022,7 +2022,7 @@ let wp_rec ~wp env kn th fdl =
Eval_match.eval_match ~inline:Eval_match.inline_nonrec_linear lkn f in*)
let pr = create_prsymbol (id_clone name) in
let d = create_prop_decl Paxiom pr f in
Theory.add_decl th d
Theory.add_decl ~warn:false th d
else
th
in
......
theory Tests
use import int.Int
axiom a : 1 = 2
type myRecord = { value : int }
axiom value_axiom : forall i1 : myRecord. i1.value >= 1
end
theory T
type t
function f t : int
end
theory BadExtension
use import int.Int
axiom a : 1 = 2
use import T
axiom a : forall x:t. f x >= 0
end
\ No newline at end of file
module ProblemWithLemmaFunction
(* this case should not issue a warning *)
use import int.Int
let lemma plus_comm (x y : int) : unit
ensures { x + y = y + x }
= ()
end
\ No newline at end of file
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