From 9a8305d6c02bcfcf94fba491cdbde63d612a2aa6 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Sat, 2 Dec 2017 11:22:50 +0000 Subject: [PATCH 01/22] OCaml 4.06.0 rebuild. --- why.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/why.spec b/why.spec index 270051a..1449532 100644 --- a/why.spec +++ b/why.spec @@ -10,7 +10,7 @@ Name: why Version: 2.39 -Release: 2%{?dist} +Release: 3%{?dist} Summary: Software verification platform License: LGPLv2 with exceptions @@ -244,6 +244,9 @@ gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || : %changelog +* Sat Dec 02 2017 Richard W.M. Jones - 2.39-3 +- OCaml 4.06.0 rebuild. + * Sat Oct 7 2017 Jerry James - 2.39-2 - Rebuild for why3 0.88.0 From bfd7fd56a1eb65c26f914095d957dfa86bbbe195 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sat, 9 Dec 2017 16:07:42 -0700 Subject: [PATCH 02/22] Bring back the -project patch, still needed (bz 1520483). Add the -safe-string patch for building with ocaml 4.06.0. Build the Jessie plugin with -runtime-variant _pic. --- why-ocaml-4.06.patch | 22 ++++++++ why-project.patch | 115 ++++++++++++++++++++++++++++++++++++++++++ why-safe-string.patch | 67 ++++++++++++++++++++++++ why.spec | 23 +++++++-- 4 files changed, 224 insertions(+), 3 deletions(-) create mode 100644 why-ocaml-4.06.patch create mode 100644 why-project.patch create mode 100644 why-safe-string.patch diff --git a/why-ocaml-4.06.patch b/why-ocaml-4.06.patch new file mode 100644 index 0000000..32f133c --- /dev/null +++ b/why-ocaml-4.06.patch @@ -0,0 +1,22 @@ +--- configure.orig 2017-08-23 02:08:38.000000000 -0600 ++++ configure 2017-12-09 13:10:09.950794648 -0700 +@@ -1823,7 +1823,7 @@ case $OCAMLVERSION in + OCAMLWARN=Aer-6-41-44-45 ;; + 4.02.*) + OCAMLWARN=Aer-3-6-41-44-45-48-50 ;; +- 4.03.*|4.04.*) ++ 4.03.*|4.04.*|4.05.*|4.06.*) + OCAMLWARN=Aer-3-6-41-44-45-48-50-52-57 ;; + *) + { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: Unknown Objective Caml version" >&5 +--- Makefile.in.orig 2017-12-04 21:00:24.549232019 -0700 ++++ Makefile.in 2017-12-09 13:10:39.550655718 -0700 +@@ -213,7 +213,7 @@ jc/jc.cmx jc/jc.o: $(JCCMX_EXPORT) + # ppc: jc/jc.cmi jc/jc.cmo jc/jc.cmx + + bin/jessie.opt: $(JCCMX) +- $(if $(QUIET),@echo 'Linking $@' &&) $(OCAMLOPT) $(OFLAGS) $(APRONLIB) $(APRONLIBS) $(ATPLIB) -o $@ \ ++ $(if $(QUIET),@echo 'Linking $@' &&) $(OCAMLOPT) -runtime-variant _pic $(OFLAGS) $(APRONLIB) $(APRONLIBS) $(ATPLIB) -o $@ \ + unix.cmxa str.cmxa nums.cmxa graph.cmxa $^ + $(STRIP) $@ + diff --git a/why-project.patch b/why-project.patch new file mode 100644 index 0000000..e50186a --- /dev/null +++ b/why-project.patch @@ -0,0 +1,115 @@ +--- Makefile.in.orig 2017-08-23 02:08:38.000000000 -0600 ++++ Makefile.in 2017-12-04 21:00:24.549232019 -0700 +@@ -154,7 +154,7 @@ CMO_EXPORT = src/lib.cmo src/rc.cmo src + src/effect.cmo src/pp.cmo src/option_misc.cmo \ + src/report.cmo \ + src/explain.cmo \ +- src/xml.cmo src/project.cmo ++ src/xml.cmo src/whyproject.cmo + + # jessie + JCCML_EXPORT = src/why3_kw.ml jc/output.ml \ +--- src/options.mli.orig 2017-08-23 02:08:38.000000000 -0600 ++++ src/options.mli 2017-12-04 21:01:17.268996320 -0700 +@@ -184,7 +184,7 @@ val files : string list + (*s GUI? *) + + val gui : bool ref +-val gui_project : Project.t option ref ++val gui_project : Whyproject.t option ref + val lib_files_to_load : string list + + (* +--- src/pretty.ml.orig 2017-08-23 02:08:38.000000000 -0600 ++++ src/pretty.ml 2017-12-04 21:02:42.540615229 -0700 +@@ -416,12 +416,12 @@ let output_project f = + with Not_found -> + functions := SMap.add fn SMap.empty !functions) + Util.program_locs ; +- let p = Project.create (Filename.basename f) in +- Project.set_project_context_file p (f ^ "_ctx.why"); ++ let p = Whyproject.create (Filename.basename f) in ++ Whyproject.set_project_context_file p (f ^ "_ctx.why"); + List.iter + (fun (expl,fpo) -> + let n = expl.lemma_or_fun_name in +- let _ = Project.add_lemma p n expl fpo in ()) ++ let _ = Whyproject.add_lemma p n expl fpo in ()) + !lemmas; + SMap.iter + (fun fname behs -> +@@ -431,15 +431,15 @@ let output_project f = + floc + with Not_found -> Loc.dummy_floc + in +- let f = Project.add_function p fname floc in ++ let f = Whyproject.add_function p fname floc in + SMap.iter + (fun beh vcs -> +- let be = Project.add_behavior f beh floc in ++ let be = Whyproject.add_behavior f beh floc in + List.iter + (fun (expl,fpo) -> +- let _ = Project.add_goal be expl fpo in ()) ++ let _ = Whyproject.add_goal be expl fpo in ()) + vcs) + behs) + !functions; +- Project.save p f; ++ Whyproject.save p f; + p +--- src/pretty.mli.orig 2017-08-23 02:08:38.000000000 -0600 ++++ src/pretty.mli 2017-12-04 21:03:05.635512035 -0700 +@@ -50,4 +50,4 @@ val output_files : string -> unit + (* [output_project f] produces a whole project description, in a file + [f.wpr], together with other needed files [f_ctx.why], [f_lemmas.why], + and each goal in a separate file [f_po.why] for i=1,2,... *) +-val output_project : string -> Project.t ++val output_project : string -> Whyproject.t +--- src/whyweb.ml.orig 2017-08-23 02:08:38.000000000 -0600 ++++ src/whyweb.ml 2017-12-04 21:04:16.932193463 -0700 +@@ -29,7 +29,7 @@ + (**************************************************************************) + + open Format +-open Project ++open Whyproject + + (*prover*) + let provers = [Ergo ; Simplify ; Z3 ; Yices ; Cvc3] +@@ -168,7 +168,7 @@ let file = match !file with + | None -> () + | Some f -> Arg.usage spec usage; exit 1 + +-let proj = ref (Project.create "") ++let proj = ref (Whyproject.create "") + + let proj_file = ref "" + +@@ -260,7 +260,7 @@ let interp_com c = + let _ = Thread.create (launch_behavior Cvc3) b in () + | `LaunchCvc3Function f -> + let _ = Thread.create (launch_function Cvc3) f in () +- | `Save -> Project.save !proj !proj.project_name ++ | `Save -> Whyproject.save !proj !proj.project_name + end; + loc + with Not_found -> ("",0,0,0) +@@ -343,7 +343,7 @@ let main_page msg = + let load_prj file = + eprintf "Reading file %s@." file; + try +- proj := Project.load file; ++ proj := Whyproject.load file; + proj_file := file; + with + Sys_error _ -> +@@ -526,7 +526,7 @@ wprint "
Save Proj + " ns; + wprint ""; + List.iter (fun prover -> +- wprint "" (Project.provers_name prover)) ++ wprint "" (Whyproject.provers_name prover)) + provers; + wprint " + "; diff --git a/why-safe-string.patch b/why-safe-string.patch new file mode 100644 index 0000000..20c3406 --- /dev/null +++ b/why-safe-string.patch @@ -0,0 +1,67 @@ +--- jc/jc_annot_inference.ml.orig 2017-08-23 02:08:38.000000000 -0600 ++++ jc/jc_annot_inference.ml 2017-12-05 21:03:16.549749880 -0700 +@@ -212,14 +212,14 @@ let name_of_term t = + Format.fprintf str_formatter "%a" Jc_output.term t; + let s = Format.flush_str_formatter () in + let s = filter_alphanumeric s in +- "T" ^ unique_term_name t s ++ "T" ^ unique_term_name t (Bytes.to_string s) + + let name_of_assertion a = + ignore (Format.flush_str_formatter ()); + Format.fprintf str_formatter "%a" Jc_output.assertion a; + let s = Format.flush_str_formatter () in + let s = filter_alphanumeric s in +- "A" ^ unique_assertion_name a s ++ "A" ^ unique_assertion_name a (Bytes.to_string s) + + (* support of (Nicolas) *) + let rec destruct_alloc t = +--- jc/jc_region.ml.orig 2017-08-23 02:08:38.000000000 -0600 ++++ jc/jc_region.ml 2017-12-05 21:01:36.269076188 -0700 +@@ -244,8 +244,8 @@ struct + jc_reg_variable = false; + jc_reg_bitwise = false; + jc_reg_id = id; +- jc_reg_name = name; +- jc_reg_final_name = name ^ "_" ^ (string_of_int id); ++ jc_reg_name = (Bytes.to_string name); ++ jc_reg_final_name = (Bytes.to_string name) ^ "_" ^ (string_of_int id); + jc_reg_type = ty; + } + +@@ -258,8 +258,8 @@ struct + jc_reg_variable = true; + jc_reg_bitwise = false; + jc_reg_id = id; +- jc_reg_name = name; +- jc_reg_final_name = name ^ "_" ^ (string_of_int id); ++ jc_reg_name = (Bytes.to_string name); ++ jc_reg_final_name = (Bytes.to_string name) ^ "_" ^ (string_of_int id); + jc_reg_type = ty; + } + +--- src/lib.ml.orig 2017-08-23 02:08:38.000000000 -0600 ++++ src/lib.ml 2017-12-05 20:43:07.384255238 -0700 +@@ -54,7 +54,7 @@ let file_subdir ~dir ~file = + let file_copy src dest = + let cin = open_in src + and cout = open_out dest +- and buff = String.make 1024 ' ' ++ and buff = Bytes.make 1024 ' ' + and n = ref 0 + in + while n := input cin buff 0 1024; !n <> 0 do +@@ -68,10 +68,10 @@ let file_copy_if_different src dst = + + let channel_contents_buf cin = + let buf = Buffer.create 1024 +- and buff = String.make 1024 ' ' in ++ and buff = Bytes.make 1024 ' ' in + let n = ref 0 in + while n := input cin buff 0 1024; !n <> 0 do +- Buffer.add_substring buf buff 0 !n ++ Buffer.add_subbytes buf buff 0 !n + done; + buf + diff --git a/why.spec b/why.spec index 1449532..c2fc8ec 100644 --- a/why.spec +++ b/why.spec @@ -26,6 +26,13 @@ Source7: rem.pvs Source8: patch_jessie_pvs # Created with gimp from official upstream icon Source9: %{name}-icons.tar.xz +# Avoid a clash between Frama-C and why modules both named "Project". +# Sent upstream 26 Jun 2014. +Patch0: %{name}-project.patch +# Adapt to the safe string feature of ocaml 4.06 +Patch1: %{name}-safe-string.patch +# Adapt to ocaml 4.06 in general +Patch2: %{name}-ocaml-4.06.patch BuildRequires: auto-destdir BuildRequires: desktop-file-utils @@ -37,6 +44,7 @@ BuildRequires: ocaml-apron-devel BuildRequires: ocaml-camlp4-devel BuildRequires: ocaml-findlib BuildRequires: ocaml-mlgmpidl-devel +BuildRequires: ocaml-num-devel BuildRequires: ocaml-ocamldoc BuildRequires: ocaml-ocamlgraph-devel BuildRequires: ocaml-zarith-devel @@ -115,6 +123,13 @@ based on Why, including various automated and interactive provers. %prep %setup -q %setup -q -T -D -a 9 +%patch0 +%patch1 +%patch2 + +# The other part of avoiding the "Project" module name clash +mv src/project.ml src/whyproject.ml +mv src/project.mli src/whyproject.mli cp -p %SOURCE2 ./ @@ -147,9 +162,6 @@ sed -ri 's,ocaml(c|opt),& -g,' atp/Makefile # Command "pvs" is LVM2's /sbin/pvs, so rename "pvs" to pvs-sbcl: sed -i 's/pvs/pvs-sbcl/' configure -# Allow building with OCaml 4.05 -sed -i 's/4\.04\.\*/4.04.*|4.05.*/' configure - %build %if ! %{opt} %global opt_option OCAMLBEST=byte OCAMLDEP=ocamldep OCAMLYACC=ocamlyacc OCAMLLEX=ocamllex @@ -244,6 +256,11 @@ gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || : %changelog +* Sat Dec 9 2017 Jerry James - 2.39-3 +- Bring back the -project patch, still needed (bz 1520483) +- Add the -safe-string patch for building with ocaml 4.06.0 +- Build the Jessie plugin with -runtime-variant _pic + * Sat Dec 02 2017 Richard W.M. Jones - 2.39-3 - OCaml 4.06.0 rebuild. From d328121299f44fbb864b2b87a6161040c08b36ea Mon Sep 17 00:00:00 2001 From: Igor Gnatenko Date: Thu, 18 Jan 2018 22:48:54 +0100 Subject: [PATCH 03/22] Remove obsolete scriptlets Signed-off-by: Igor Gnatenko --- why.spec | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) diff --git a/why.spec b/why.spec index c2fc8ec..1e925f2 100644 --- a/why.spec +++ b/why.spec @@ -10,7 +10,7 @@ Name: why Version: 2.39 -Release: 3%{?dist} +Release: 4%{?dist} Summary: Software verification platform License: LGPLv2 with exceptions @@ -216,14 +216,6 @@ cp -p %{SOURCE1} %{SOURCE3} CHANGES README Version %{buildroot}%{why_doc_dir} %check make check -%post jessie -touch --no-create %{_datadir}/icons/hicolor &>/dev/null -gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || : - -%postun jessie -touch --no-create %{_datadir}/icons/hicolor &>/dev/null -gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || : - %files %doc README.why-coq.Fedora %license COPYING LICENSE @@ -256,6 +248,9 @@ gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || : %changelog +* Thu Jan 18 2018 Igor Gnatenko - 2.39-4 +- Remove obsolete scriptlets + * Sat Dec 9 2017 Jerry James - 2.39-3 - Bring back the -project patch, still needed (bz 1520483) - Add the -safe-string patch for building with ocaml 4.06.0 From 88eb8b7a51249bdd3aecea35174efeff8ec09af0 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Fri, 9 Feb 2018 20:55:21 +0000 Subject: [PATCH 04/22] - Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild Signed-off-by: Fedora Release Engineering --- why.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/why.spec b/why.spec index 1e925f2..9c84a8c 100644 --- a/why.spec +++ b/why.spec @@ -10,7 +10,7 @@ Name: why Version: 2.39 -Release: 4%{?dist} +Release: 5%{?dist} Summary: Software verification platform License: LGPLv2 with exceptions @@ -248,6 +248,9 @@ make check %changelog +* Fri Feb 09 2018 Fedora Release Engineering - 2.39-5 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild + * Thu Jan 18 2018 Igor Gnatenko - 2.39-4 - Remove obsolete scriptlets From 88002a4073e641acc683fe58e5369d776c683fb8 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 12 Feb 2018 20:20:06 -0700 Subject: [PATCH 05/22] New upstream release. Add -num patch to fix incomplete num to zarith conversion. --- .gitignore | 1 + sources | 2 +- why-num.patch | 596 ++++++++++++++++++++++++++++++++++++++++++ why-ocaml-4.06.patch | 19 +- why-project.patch | 22 +- why-safe-string.patch | 52 +--- why.spec | 29 +- 7 files changed, 629 insertions(+), 92 deletions(-) create mode 100644 why-num.patch diff --git a/.gitignore b/.gitignore index ba8b107..31ca9a5 100644 --- a/.gitignore +++ b/.gitignore @@ -3,3 +3,4 @@ /why-2.36.tar.gz /why-2.38.tar.gz /why-2.39.tar.gz +/why-2.40.tar.gz diff --git a/sources b/sources index 77125d9..2db9799 100644 --- a/sources +++ b/sources @@ -1,3 +1,3 @@ SHA512 (krakatoa.pdf) = 5d0f4e6b938ddc1eafa48264c02cf99e68f776a7e190b997e35fb2cd154627b5d27369886f570cbcfdfe5f3a1929a97a1fec9457a6f6662f83cbb2e51f65ca04 -SHA512 (why-2.39.tar.gz) = b36e9423ff82fa2f51fea40a33021ed0def3719d9421b2f7f1e2aa1d6113faacf932984ac293b6d0ac92f800fd48efbdd8cc3ec6a929003a57da20efab682bad +SHA512 (why-2.40.tar.gz) = e99f528ab2a3030c5ed8509ec45e75dc2f3dc2ed92fe1213c2b92a2dc700e2d9c32bc765751b2660cc1f3a6e110b4687a4262779fdae52faaaf144c411712972 SHA512 (why-icons.tar.xz) = d6ca78cf09540f5742564912470fb8c49f7d11ca16cd8bb60c8790af10c1591198f6020bd792cff8e3464f762b7ef0a690d3e4ba1a2cf670c286c8056d266bc3 diff --git a/why-num.patch b/why-num.patch new file mode 100644 index 0000000..10b0164 --- /dev/null +++ b/why-num.patch @@ -0,0 +1,596 @@ +--- atp/cooper.ml.orig 2018-01-23 03:07:35.000000000 -0700 ++++ atp/cooper.ml 2018-02-11 20:48:48.754907226 -0700 +@@ -38,10 +38,10 @@ + (* Lift operations up to numerals. *) + (* ------------------------------------------------------------------------- *) + +-let mk_numeral n = Fn(string_of_num n,[]);; ++let mk_numeral n = Fn(Z.to_string n,[]);; + + let dest_numeral = +- function (Fn(ns,[])) -> num_of_string ns ++ function (Fn(ns,[])) -> Z.of_string ns + | _ -> failwith "dest_numeral";; + + let is_numeral = can dest_numeral;; +@@ -59,12 +59,12 @@ let numeral2 fn m n = mk_numeral(fn (des + (* ------------------------------------------------------------------------- *) + + let rec linear_cmul n tm = +- if n =/ Int 0 then Fn("0",[]) else ++ if Z.equal n Z.zero then Fn("0",[]) else + match tm with + Fn("+",[Fn("*",[c1; x1]); rest]) -> +- Fn("+",[Fn("*",[numeral1 (( */ ) n) c1; x1]); ++ Fn("+",[Fn("*",[numeral1 (Z.mul n) c1; x1]); + linear_cmul n rest]) +- | k -> numeral1 (( */ ) n) k;; ++ | k -> numeral1 (Z.mul n) k;; + + let earlierv vars (Var x) (Var y) = earlier vars x y;; + +@@ -73,7 +73,7 @@ let rec linear_add vars tm1 tm2 = + (Fn("+",[Fn("*",[c1; x1]); rest1]), + Fn("+",[Fn("*",[c2; x2]); rest2])) -> + if x1 = x2 then +- let c = numeral2 (+/) c1 c2 in ++ let c = numeral2 Z.add c1 c2 in + if c = Fn("0",[]) then linear_add vars rest1 rest2 + else Fn("+",[Fn("*",[c; x1]); linear_add vars rest1 rest2]) + else if earlierv vars x1 x2 then +@@ -84,9 +84,9 @@ let rec linear_add vars tm1 tm2 = + Fn("+",[Fn("*",[c1; x1]); linear_add vars rest1 tm2]) + | (_,Fn("+",[Fn("*",[c2; x2]); rest2])) -> + Fn("+",[Fn("*",[c2; x2]); linear_add vars tm1 rest2]) +- | _ -> numeral2 (+/) tm1 tm2;; ++ | _ -> numeral2 Z.add tm1 tm2;; + +-let linear_neg tm = linear_cmul (Int(-1)) tm;; ++let linear_neg tm = linear_cmul Z.minus_one tm;; + + let linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2);; + +@@ -116,7 +116,7 @@ let mkatom vars p t = Atom(R(p,[Fn("0",[ + let linform vars fm = + match fm with + Atom(R("divides",[c;t])) -> +- let c' = mk_numeral(abs_num(dest_numeral c)) in ++ let c' = mk_numeral(Z.abs(dest_numeral c)) in + Atom(R("divides",[c';lint vars t])) + | Atom(R("=",[s;t])) -> mkatom vars "=" (Fn("-",[t;s])) + | Atom(R("<",[s;t])) -> mkatom vars "<" (Fn("-",[t;s])) +@@ -144,11 +144,11 @@ let rec posineq fm = + let rec formlcm x fm = + match fm with + Atom(R(p,[_;Fn("+",[Fn("*",[c;y]);z])])) when y = x -> +- abs_num(dest_numeral c) ++ Z.abs(dest_numeral c) + | Not(p) -> formlcm x p + | And(p,q) -> lcm_num (formlcm x p) (formlcm x q) + | Or(p,q) -> lcm_num (formlcm x p) (formlcm x q) +- | _ -> Int 1;; ++ | _ -> Z.one;; + + (* ------------------------------------------------------------------------- *) + (* Adjust all coefficients of x in formula; fold in reduction to +/- 1. *) +@@ -157,10 +157,10 @@ let rec formlcm x fm = + let rec adjustcoeff x l fm = + match fm with + Atom(R(p,[d; Fn("+",[Fn("*",[c;y]);z])])) when y = x -> +- let m = l // dest_numeral c in +- let n = if p = "<" then abs_num(m) else m in +- let xtm = Fn("*",[mk_numeral(m // n); x]) in +- Atom(R(p,[linear_cmul (abs_num m) d; ++ let m = Z.div l (dest_numeral c) in ++ let n = if p = "<" then Z.abs(m) else m in ++ let xtm = Fn("*",[mk_numeral(Z.div m n); x]) in ++ Atom(R(p,[linear_cmul (Z.abs m) d; + Fn("+",[xtm; linear_cmul n z])])) + | Not(p) -> Not(adjustcoeff x l p) + | And(p,q) -> And(adjustcoeff x l p,adjustcoeff x l q) +@@ -174,7 +174,7 @@ let rec adjustcoeff x l fm = + let unitycoeff x fm = + let l = formlcm x fm in + let fm' = adjustcoeff x l fm in +- if l =/ Int 1 then fm' else ++ if Z.equal l Z.one then fm' else + let xp = Fn("+",[Fn("*",[Fn("1",[]);x]); Fn("0",[])]) in + And(Atom(R("divides",[mk_numeral l; xp])),adjustcoeff x l fm);; + +@@ -204,7 +204,7 @@ let rec divlcm x fm = + | Not(p) -> divlcm x p + | And(p,q) -> lcm_num (divlcm x p) (divlcm x q) + | Or(p,q) -> lcm_num (divlcm x p) (divlcm x q) +- | _ -> Int 1;; ++ | _ -> Z.one;; + + (* ------------------------------------------------------------------------- *) + (* Construct the B-set. *) +@@ -242,8 +242,8 @@ let rec linrep vars x t fm = + (* ------------------------------------------------------------------------- *) + + let operations = +- ["=",(=/); "<",(",(>/); "<=",(<=/); ">=",(>=/); +- "divides",(fun x y -> mod_num y x =/ Int 0)];; ++ ["=",(Z.equal); "<",(Z.lt); ">",(Z.gt); "<=",(Z.leq); ">=",(Z.geq); ++ "divides",(fun x y -> Z.equal (Z.rem y x) Z.zero)];; + + let evalc_atom at = + match at with +@@ -265,7 +265,7 @@ let cooper vars fm = + let x = Var x0 in + let p = unitycoeff x p0 in + let p_inf = simplify(minusinf x p) and bs = bset x p +- and js = Int 1 --- divlcm x p in ++ and js = Z.one --- divlcm x p in + let p_element j b = + linrep vars x (linear_add vars b (mk_numeral j)) p in + let stage j = list_disj +--- atp/defcnf.ml.orig 2018-01-23 03:07:35.000000000 -0700 ++++ atp/defcnf.ml 2018-02-11 14:00:03.159892859 -0700 +@@ -55,7 +55,7 @@ let rec nenf fm = + (* Make a stylized variable and update the index. *) + (* ------------------------------------------------------------------------- *) + +-let mkprop n = Atom(P("p_"^(string_of_num n))),n +/ Int 1;; ++let mkprop n = Atom(P("p_"^(Z.to_string n))),Z.succ n;; + + (* ------------------------------------------------------------------------- *) + (* Make n large enough that "v_m" won't clash with s for any m >= n *) +@@ -67,7 +67,7 @@ let max_varindex pfx = + let l = String.length s in + if l <= m or String.sub s 0 m <> pfx then n else + let s' = String.sub s m (l - m) in +- if forall numeric (explode s') then max_num n (num_of_string s') ++ if forall numeric (explode s') then Z.max n (Z.of_string s') + else n;; + + (* ------------------------------------------------------------------------- *) +@@ -90,7 +90,7 @@ and defstep op (p,q) (fm,defs,n) = + + let defcnf fm = + let fm' = nenf(psimplify fm) in +- let n = Int 1 +/ overatoms (max_varindex "p_" ** pname) fm' (Int 0) in ++ let n = Z.succ (overatoms (max_varindex "p_" ** pname) fm' Z.zero) in + let (fm'',defs,_) = maincnf (fm',undefined,n) in + let deflist = map (snd ** snd) (funset defs) in + let subcnfs = itlist ((@) ** simpcnf) deflist (simpcnf fm'') in +@@ -130,7 +130,7 @@ let rec andcnf (fm,defs,n as trip) = + + let defcnfs fm = + let fm' = nenf(psimplify fm) in +- let n = Int 1 +/ overatoms (max_varindex "p_" ** pname) fm' (Int 0) in ++ let n = Z.succ (overatoms (max_varindex "p_" ** pname) fm' Z.zero) in + let (fm'',defs,_) = andcnf (fm',undefined,n) in + let deflist = map (snd ** snd) (funset defs) in + setify(itlist ((@) ** simpcnf) deflist (simpcnf fm''));; +@@ -181,7 +181,7 @@ let rec andcnf pos (fm,defs,n as trip) = + + let defcnfs imps fm = + let fm' = nenf(psimplify fm) in +- let n = Int 1 +/ overatoms (max_varindex "p_" ** pname) fm' (Int 0) in ++ let n = Z.succ (overatoms (max_varindex "p_" ** pname) fm' Z.zero) in + let (fm'',defs,_) = andcnf imps (fm',undefined,n) in + let deflist = map (snd ** snd) (funset defs) in + setify(itlist ((@) ** simpcnf) deflist (simpcnf fm''));; +@@ -209,7 +209,7 @@ let rec andcnf3 pos (fm,defs,n as trip) + + let defcnf3s imps fm = + let fm' = nenf(psimplify fm) in +- let n = Int 1 +/ overatoms (max_varindex "p_" ** pname) fm' (Int 0) in ++ let n = Z.succ (overatoms (max_varindex "p_" ** pname) fm' Z.zero) in + let (fm'',defs,_) = andcnf3 imps (fm',undefined,n) in + let deflist = map (snd ** snd) (funset defs) in + setify(itlist ((@) ** simpcnf) deflist (simpcnf fm''));; +--- atp/fourier_motzkin.ml.orig 2018-01-23 03:07:35.000000000 -0700 ++++ atp/fourier_motzkin.ml 2018-02-11 20:34:13.822886848 -0700 +@@ -71,10 +71,10 @@ let rec posineq fm = + let rec adjustcoeff x l fm = + match fm with + Atom(R(p,[d; Fn("+",[Fn("*",[c;y]);z])])) when y = x -> +- let m = l // dest_numeral c in +- let n = if p = "<=" then abs_num(m) else m in +- let xtm = Fn("*",[mk_numeral(m // n); x]) in +- Atom(R(p,[linear_cmul (abs_num m) d; ++ let m = Z.div l (dest_numeral c) in ++ let n = if p = "<=" then Z.abs(m) else m in ++ let xtm = Fn("*",[mk_numeral(Z.div m n); x]) in ++ Atom(R(p,[linear_cmul (Z.abs m) d; + Fn("+",[xtm; linear_cmul n z])])) + | Not(p) -> Not(adjustcoeff x l p) + | And(p,q) -> And(adjustcoeff x l p,adjustcoeff x l q) +@@ -88,7 +88,7 @@ let rec adjustcoeff x l fm = + let unitycoeff x fm = + let l = formlcm x fm in + let fm' = adjustcoeff x l fm in +- if l =/ Int 1 then fm' else ++ if Z.equal l Z.one then fm' else + adjustcoeff x l fm;; + + (* ------------------------------------------------------------------------- *) +@@ -98,10 +98,10 @@ let unitycoeff x fm = + let isolate x fm = + match fm with + Atom(R(p,[_;Fn("+",[Fn("*",[c;y]);z])])) when y = x -> +- let c = mk_numeral (Int 0 -/ dest_numeral c) in ++ let c = mk_numeral (Z.sub Z.zero (dest_numeral c)) in + Atom(R(p,[Fn("*",[c;y]);z])) + | Atom(R(p,[zero;Fn("*",[c;y])])) when y = x -> +- let c = mk_numeral (Int 0 -/ dest_numeral c) in ++ let c = mk_numeral (Z.sub Z.zero (dest_numeral c)) in + Atom(R(p,[Fn("*",[c;y]);zero])) + | _ -> + printer fm; +@@ -110,7 +110,7 @@ let isolate x fm = + let replace vars x t fm = + match fm with + Atom(R(p,[Fn("*",[c;y]);z])) when y = x -> +- let t = if dest_numeral c >/ Int 0 then t else linear_neg t in ++ let t = if Z.gt (dest_numeral c) Z.zero then t else linear_neg t in + linform vars (Atom(R(p,[t;z]))) + | _ -> assert false + +@@ -128,13 +128,13 @@ let fourier vars fm = + (function (Atom(R("=",_))) -> true | _ -> false) cjs in + let (Atom(R("=",[s;t]))) = eqn in + let (Fn("*",[c;_])) = s in +- let y = if dest_numeral c =/ Int 1 then t else linear_neg t in ++ let y = if Z.equal (dest_numeral c) Z.one then t else linear_neg t in + list_conj(map (replace vars x y) (subtract cjs [eqn])) + with Failure _ -> + let l,r = + partition + (fun (Atom(R("<=",[Fn("*",[c;_]);t]))) -> +- dest_numeral c =/ Int (-1)) cjs ++ Z.equal (dest_numeral c) Z.minus_one) cjs + in + let lefts = map (fun (Atom(R("<=",[_;l]))) -> linear_neg l) l + and rights = map (fun (Atom(R("<=",[_;r]))) -> r) r in +--- atp/lib.ml.orig 2018-01-23 03:07:35.000000000 -0700 ++++ atp/lib.ml 2018-02-11 13:26:57.020559495 -0700 +@@ -46,11 +46,9 @@ let ( ** ) = fun f g x -> f(g x);; + (* GCD and LCM on arbitrary-precision numbers. *) + (* ------------------------------------------------------------------------- *) + +-let gcd_num n1 n2 = +- abs_num(num_of_big_int +- (Big_int.gcd_big_int (big_int_of_num n1) (big_int_of_num n2)));; ++let gcd_num n1 n2 = Z.gcd n1 n2;; + +-let lcm_num n1 n2 = abs_num(n1 */ n2) // gcd_num n1 n2;; ++let lcm_num n1 n2 = Z.lcm n1 n2;; + + (* ------------------------------------------------------------------------- *) + (* A useful idiom for "non contradictory" etc. *) +@@ -73,7 +71,7 @@ let can f x = try f x; true with Failure + + let rec (--) = fun m n -> if m > n then [] else m::((m + 1) -- n);; + +-let rec (---) = fun m n -> if m >/ n then [] else m::((m +/ Int 1) --- n);; ++let rec (---) = fun m n -> if Z.gt m n then [] else m::((Z.succ m) --- n);; + + let rec map2 f l1 l2 = + match (l1,l2) with +@@ -596,4 +594,4 @@ let equated (Partition f) = dom f;; + (* First number starting at n for which p succeeds. *) + (* ------------------------------------------------------------------------- *) + +-let rec first n p = if p(n) then n else first (n +/ Int 1) p;; ++let rec first n p = if p(n) then n else first (Z.succ n) p;; +--- atp/Makefile.orig 2018-01-23 03:07:35.000000000 -0700 ++++ atp/Makefile 2018-02-11 13:14:15.311777144 -0700 +@@ -8,6 +8,8 @@ + # many.ml (Example relevant to many-sorted logic) + # hol.ml (Simple higher order logic setup) + ++ZARITHLIB=$(shell ocamlfind query zarith) ++ + #MLFILES = lib.ml intro.ml formulas.ml prop.ml propexamples.ml \ + defcnf.ml dp.ml stal.ml bdd.ml fol.ml skolem.ml \ + herbrand.ml unif.ml tableaux.ml resolution.ml prolog.ml \ +@@ -33,9 +35,9 @@ compiled: example.ml atp.cmx; ocamlopt - + + # Make the appropriate object for the main body of code + +-atp.cmx: atp.ml; ocamlopt -w ax -c atp.ml ++atp.cmx: atp.ml; ocamlopt -I $(ZARITHLIB) -w ax -c atp.ml + +-atp.cmo: atp.ml; ocamlc -w ax -c atp.ml ++atp.cmo: atp.ml; ocamlc -I $(ZARITHLIB) -w ax -c atp.ml + + # Make the camlp4 quotation expander + +--- atp/make.ml.orig 2018-01-23 03:07:35.000000000 -0700 ++++ atp/make.ml 2018-02-11 14:37:48.178019612 -0700 +@@ -44,10 +44,9 @@ + Gc.set { (Gc.get()) with Gc.stack_limit = 16777216 };; (* Up the stack size *) + Format.set_margin 72;; (* Reduce margins *) + open Format;; (* Open formatting *) +-open Num;; (* Open bignums *) + let imperative_assign = (:=);; (* Preserve this *) + +-let print_num n = print_string(string_of_num n);; (* Avoid range limit *) ++let print_num n = print_string(Z.to_string n);; (* Avoid range limit *) + #install_printer print_num;; (* when printing nums *) + + (* ------------------------------------------------------------------------- *) +--- atp/Mk_ml_file.orig 2018-01-23 03:07:35.000000000 -0700 ++++ atp/Mk_ml_file 2018-02-10 22:01:01.925304810 -0700 +@@ -1,4 +1,3 @@ +-echo "open Num;;" + echo "open Format;;" + + cat $@ | sed 's/START_INTERACTIVE;;/(\*/' | sed 's/END_INTERACTIVE;;/\*)/' +--- jc/jc_annot_inference.ml.orig 2018-02-10 16:03:04.338379961 -0700 ++++ jc/jc_annot_inference.ml 2018-02-11 13:13:48.313855743 -0700 +@@ -49,7 +49,6 @@ open Apron + open Coeff + open Interval + open Lincons1 +-open Num + + + (*****************************************************************************) +@@ -1120,7 +1119,7 @@ let linearize t = + try match t#node with + | JCTconst c -> + begin match c with +- | JCCinteger s -> (TermMap.empty, num_of_string s) ++ | JCCinteger s -> (TermMap.empty, Z.of_string s) + | JCCboolean _ | JCCvoid | JCCnull | JCCreal _ | JCCstring _ -> + err () + end +@@ -1133,7 +1132,7 @@ let linearize t = + (fun vt1 c1 acc -> + try + let c2 = TermMap.find vt1 coeffs2 in +- TermMap.add vt1 (c1 +/ c2) acc ++ TermMap.add vt1 (Z.add c1 c2) acc + with Not_found -> TermMap.add vt1 c1 acc + ) coeffs1 TermMap.empty + in +@@ -1143,55 +1142,55 @@ let linearize t = + else TermMap.add vt2 c2 acc + ) coeffs2 coeffs + in +- (coeffs, cst1 +/ cst2) ++ (coeffs, (Z.add cst1 cst2)) + | `Bsub -> + let coeffs = TermMap.fold + (fun vt1 c1 acc -> + try + let c2 = TermMap.find vt1 coeffs2 in +- TermMap.add vt1 (c1 -/ c2) acc ++ TermMap.add vt1 (Z.sub c1 c2) acc + with Not_found -> TermMap.add vt1 c1 acc + ) coeffs1 TermMap.empty + in + let coeffs = TermMap.fold + (fun vt2 c2 acc -> + if TermMap.mem vt2 coeffs then acc +- else TermMap.add vt2 (minus_num c2) acc ++ else TermMap.add vt2 (Z.neg c2) acc + ) coeffs2 coeffs + in +- (coeffs, cst1 -/ cst2) ++ (coeffs, (Z.sub cst1 cst2)) + | `Bmul when TermMap.is_empty coeffs1 || TermMap.is_empty coeffs2 -> + let coeffs = + if TermMap.is_empty coeffs1 then +- TermMap.map (fun c -> c */ cst1) coeffs2 ++ TermMap.map (fun c -> Z.mul c cst1) coeffs2 + else +- TermMap.map (fun c -> c */ cst2) coeffs1 ++ TermMap.map (fun c -> Z.mul c cst2) coeffs1 + in +- (coeffs, cst1 */ cst2) ++ (coeffs, (Z.mul cst1 cst2)) + | `Bmul + | `Bdiv + | `Bmod -> err () + end + | JCTbinary(t1,(#bitwise_op as bop,`Integer),t2) -> + let coeffs1, cst1 = aux t1 in +- if coeffs1 = TermMap.empty && cst1 =/ Int 0 then ++ if coeffs1 = TermMap.empty && Z.equal cst1 Z.zero then + match bop with + | `Bbw_and + | `Bshift_left + | `Blogical_shift_right +- | `Barith_shift_right -> TermMap.empty, Int 0 ++ | `Barith_shift_right -> TermMap.empty, Z.zero + | `Bbw_or + | `Bbw_xor -> aux t2 + | _ -> err () + else + (* Consider non-linear term as abstract variable. *) +- (TermMap.add t (Int 1) TermMap.empty, Int 0) ++ (TermMap.add t Z.one TermMap.empty, Z.zero) + | JCTunary((uop,`Integer),t1) -> + let coeffs1,cst1 = aux t1 in + begin match uop with + | `Uminus -> +- let coeffs = TermMap.map (fun c -> minus_num c) coeffs1 in +- (coeffs, minus_num cst1) ++ let coeffs = TermMap.map (fun c -> Z.neg c) coeffs1 in ++ (coeffs, Z.neg cst1) + | _ -> err () + end + | JCTvar _ | JCTderef _ | JCToffset _ | JCTapp _ | JCTbinary _ +@@ -1201,13 +1200,16 @@ let linearize t = + | JCTrange _ | JCTif _ | JCTlet _ -> + err () + with Failure "linearize" -> +- (TermMap.add t (Int 1) TermMap.empty, Int 0) ++ (TermMap.add t Z.one TermMap.empty, Z.zero) + in aux t + + let linstr_of_term env t = ++(* + let mkmulstr = function +- | (_va, Int 0) -> "" +- | (va, c) -> string_of_num c ^ " * " ^ va ++ | (_va, Z.zero) -> "" ++ | (va, c) -> (Z.to_string c) ^ " * " ^ va ++*) ++ let mkmulstr = (fun (va,c) -> if Z.equal Z.zero c then "" else (Z.to_string c) ^ " * " ^ va) + in + let rec mkaddstr = function + | [] -> "" +@@ -1286,33 +1288,33 @@ let rec linstr_of_assertion env a = + in + let env,str,cst = linstr_of_term env subt in + if str = "" then +- let ncst = minus_num cst in ++ let ncst = Z.neg cst in + let is_true = match bop with +- | `Blt -> Int 0 Int 0 >/ ncst +- | `Ble -> Int 0 <=/ ncst +- | `Bge -> Int 0 >=/ ncst +- | `Beq -> Int 0 =/ ncst +- | `Bneq -> Int 0 <>/ ncst ++ | `Blt -> Z.lt Z.zero ncst ++ | `Bgt -> Z.gt Z.zero ncst ++ | `Ble -> Z.leq Z.zero ncst ++ | `Bge -> Z.geq Z.zero ncst ++ | `Beq -> Z.equal Z.zero ncst ++ | `Bneq -> not (Z.equal Z.zero ncst) + in + env, if is_true then Dnf.true_ else Dnf.false_ + else +- let cstr = string_of_num (minus_num cst) in ++ let cstr = Z.to_string (Z.neg cst) in + (* Do not use < and > with APRON, due to bugs in some versions. + Convert to equivalent non-strict. *) + let str = match bop with + | `Blt -> [[str ^ " <= " ^ +- (string_of_num (pred_num (minus_num cst)))]] ++ (Z.to_string (Z.pred (Z.neg cst)))]] + | `Bgt -> [[str ^ " >= " ^ +- (string_of_num (succ_num (minus_num cst)))]] ++ (Z.to_string (Z.succ (Z.neg cst)))]] + | `Ble -> [[str ^ " <= " ^ cstr]] + | `Bge -> [[str ^ " >= " ^ cstr]] + | `Beq -> [[str ^ " = " ^ cstr]] + | `Bneq -> + [[str ^ " <= " ^ +- (string_of_num (pred_num (minus_num cst)))]; ++ (Z.to_string (Z.pred (Z.neg cst)))]; + [str ^ " >= " ^ +- (string_of_num (succ_num (minus_num cst)))]] ++ (Z.to_string (Z.succ (Z.neg cst)))]] + in + env, str + | JCAnot a -> +@@ -1330,8 +1332,8 @@ let rec linstr_of_assertion env a = + let linstr_of_expr env e = + match Jc_effect.term_of_expr e with None -> None | Some t -> + let env,str,cst = linstr_of_term env t in +- if str = "" then Some (env, string_of_num cst) +- else Some (env, str ^ " + " ^ (string_of_num cst)) ++ if str = "" then Some (env, Z.to_string cst) ++ else Some (env, str ^ " + " ^ (Z.to_string cst)) + + let offset_linstr_of_expr env ok e = + match e#node with +@@ -1340,15 +1342,15 @@ let offset_linstr_of_expr env ok e = + else + begin match Jc_effect.term_of_expr e with None -> None | Some t -> + let env,str,cst = linstr_of_term env t in +- if str = "" then Some (env,string_of_num cst) +- else Some (env,str ^ " + " ^ (string_of_num cst)) ++ if str = "" then Some (env,Z.to_string cst) ++ else Some (env,str ^ " + " ^ (Z.to_string cst)) + end + | _ -> + if is_nonnull_pointer_type e#typ then + match Jc_effect.term_of_expr e with None -> None | Some t -> + let env,str,cst = offset_linstr_of_term env ok t in +- if str = "" then Some (env,string_of_num cst) +- else Some (env,str ^ " + " ^ (string_of_num cst)) ++ if str = "" then Some (env,Z.to_string cst) ++ else Some (env,str ^ " + " ^ (Z.to_string cst)) + else None + + +@@ -1419,13 +1421,13 @@ let mkassertion lincons = + + let rec linterms_of_term t = + let mkmulterm (t,c) = +- if c =/ Int 0 then None +- else if c =/ Int 1 then Some t +- else if c =/ Int (-1) then ++ if Z.equal c Z.zero then None ++ else if Z.equal c Z.one then Some t ++ else if Z.equal c Z.minus_one then + Some(new term ~typ:integer_type (JCTunary((`Uminus,`Integer),t))) + else + let c = +- new term ~typ:integer_type (JCTconst(JCCinteger(string_of_num c))) ++ new term ~typ:integer_type (JCTconst(JCCinteger(Z.to_string c))) + in + Some(new term ~typ:integer_type (JCTbinary(c,(`Bmul,`Integer),t))) + in +@@ -1443,30 +1445,30 @@ let rec linterms_of_term t = + let coeffs,cst = linearize t in + let posl,negl = + TermMap.fold (fun t c (pl,nl) -> +- if c >/ Int 0 then (t,c) :: pl, nl +- else if c +- if cst >/ Int 0 then cstt ++ if Z.gt cst Z.zero then cstt + else new term ~typ:integer_type (JCTconst(JCCinteger "0")) + | Some t -> +- if cst >/ Int 0 then ++ if Z.gt cst Z.zero then + new term ~typ:integer_type (JCTbinary(t,(`Badd,`Integer),cstt)) + else t + in + let negt = match mkaddterm negl with + | None -> +- if cst +- if cst +- if c >/ Int 0 then t :: pl, nl +- else if c [] | Some t1 -> + let mint = new term ~typ:integer_type +- (JCTconst (JCCinteger (Num.string_of_num ei.jc_enum_info_min))) ++ (JCTconst (JCCinteger (Z.to_string ei.jc_enum_info_min))) + in + let maxt = new term ~typ:integer_type +- (JCTconst(JCCinteger (Num.string_of_num ei.jc_enum_info_max))) ++ (JCTconst(JCCinteger (Z.to_string ei.jc_enum_info_max))) + in + let mina = new assertion (JCArelation (mint, (`Ble,`Integer), t1)) in + let maxa = new assertion (JCArelation (t1, (`Ble,`Integer), maxt)) in diff --git a/why-ocaml-4.06.patch b/why-ocaml-4.06.patch index 32f133c..872f38a 100644 --- a/why-ocaml-4.06.patch +++ b/why-ocaml-4.06.patch @@ -1,22 +1,11 @@ ---- configure.orig 2017-08-23 02:08:38.000000000 -0600 -+++ configure 2017-12-09 13:10:09.950794648 -0700 -@@ -1823,7 +1823,7 @@ case $OCAMLVERSION in - OCAMLWARN=Aer-6-41-44-45 ;; - 4.02.*) - OCAMLWARN=Aer-3-6-41-44-45-48-50 ;; -- 4.03.*|4.04.*) -+ 4.03.*|4.04.*|4.05.*|4.06.*) - OCAMLWARN=Aer-3-6-41-44-45-48-50-52-57 ;; - *) - { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: Unknown Objective Caml version" >&5 ---- Makefile.in.orig 2017-12-04 21:00:24.549232019 -0700 -+++ Makefile.in 2017-12-09 13:10:39.550655718 -0700 -@@ -213,7 +213,7 @@ jc/jc.cmx jc/jc.o: $(JCCMX_EXPORT) +--- Makefile.in.orig 2018-02-10 15:44:26.226883183 -0700 ++++ Makefile.in 2018-02-12 19:34:20.930490137 -0700 +@@ -214,7 +214,7 @@ jc/jc.cmx jc/jc.o: $(JCCMX_EXPORT) # ppc: jc/jc.cmi jc/jc.cmo jc/jc.cmx bin/jessie.opt: $(JCCMX) - $(if $(QUIET),@echo 'Linking $@' &&) $(OCAMLOPT) $(OFLAGS) $(APRONLIB) $(APRONLIBS) $(ATPLIB) -o $@ \ + $(if $(QUIET),@echo 'Linking $@' &&) $(OCAMLOPT) -runtime-variant _pic $(OFLAGS) $(APRONLIB) $(APRONLIBS) $(ATPLIB) -o $@ \ - unix.cmxa str.cmxa nums.cmxa graph.cmxa $^ + unix.cmxa str.cmxa zarith.cmxa graph.cmxa $^ $(STRIP) $@ diff --git a/why-project.patch b/why-project.patch index e50186a..b4536a8 100644 --- a/why-project.patch +++ b/why-project.patch @@ -1,6 +1,6 @@ ---- Makefile.in.orig 2017-08-23 02:08:38.000000000 -0600 -+++ Makefile.in 2017-12-04 21:00:24.549232019 -0700 -@@ -154,7 +154,7 @@ CMO_EXPORT = src/lib.cmo src/rc.cmo src +--- Makefile.in.orig 2018-01-23 03:07:35.000000000 -0700 ++++ Makefile.in 2018-02-10 15:44:26.226883183 -0700 +@@ -155,7 +155,7 @@ CMO_EXPORT = src/lib.cmo src/rc.cmo src src/effect.cmo src/pp.cmo src/option_misc.cmo \ src/report.cmo \ src/explain.cmo \ @@ -9,8 +9,8 @@ # jessie JCCML_EXPORT = src/why3_kw.ml jc/output.ml \ ---- src/options.mli.orig 2017-08-23 02:08:38.000000000 -0600 -+++ src/options.mli 2017-12-04 21:01:17.268996320 -0700 +--- src/options.mli.orig 2018-01-23 03:07:35.000000000 -0700 ++++ src/options.mli 2018-02-10 15:44:26.258883112 -0700 @@ -184,7 +184,7 @@ val files : string list (*s GUI? *) @@ -20,8 +20,8 @@ val lib_files_to_load : string list (* ---- src/pretty.ml.orig 2017-08-23 02:08:38.000000000 -0600 -+++ src/pretty.ml 2017-12-04 21:02:42.540615229 -0700 +--- src/pretty.ml.orig 2018-01-23 03:07:35.000000000 -0700 ++++ src/pretty.ml 2018-02-10 15:44:26.259883110 -0700 @@ -416,12 +416,12 @@ let output_project f = with Not_found -> functions := SMap.add fn SMap.empty !functions) @@ -58,16 +58,16 @@ - Project.save p f; + Whyproject.save p f; p ---- src/pretty.mli.orig 2017-08-23 02:08:38.000000000 -0600 -+++ src/pretty.mli 2017-12-04 21:03:05.635512035 -0700 +--- src/pretty.mli.orig 2018-01-23 03:07:35.000000000 -0700 ++++ src/pretty.mli 2018-02-10 15:44:26.259883110 -0700 @@ -50,4 +50,4 @@ val output_files : string -> unit (* [output_project f] produces a whole project description, in a file [f.wpr], together with other needed files [f_ctx.why], [f_lemmas.why], and each goal in a separate file [f_po.why] for i=1,2,... *) -val output_project : string -> Project.t +val output_project : string -> Whyproject.t ---- src/whyweb.ml.orig 2017-08-23 02:08:38.000000000 -0600 -+++ src/whyweb.ml 2017-12-04 21:04:16.932193463 -0700 +--- src/whyweb.ml.orig 2018-01-23 03:07:35.000000000 -0700 ++++ src/whyweb.ml 2018-02-10 15:44:26.259883110 -0700 @@ -29,7 +29,7 @@ (**************************************************************************) diff --git a/why-safe-string.patch b/why-safe-string.patch index 20c3406..23968d2 100644 --- a/why-safe-string.patch +++ b/why-safe-string.patch @@ -1,5 +1,5 @@ ---- jc/jc_annot_inference.ml.orig 2017-08-23 02:08:38.000000000 -0600 -+++ jc/jc_annot_inference.ml 2017-12-05 21:03:16.549749880 -0700 +--- jc/jc_annot_inference.ml.orig 2018-01-23 03:07:35.000000000 -0700 ++++ jc/jc_annot_inference.ml 2018-02-10 16:03:04.338379961 -0700 @@ -212,14 +212,14 @@ let name_of_term t = Format.fprintf str_formatter "%a" Jc_output.term t; let s = Format.flush_str_formatter () in @@ -17,51 +17,3 @@ (* support of (Nicolas) *) let rec destruct_alloc t = ---- jc/jc_region.ml.orig 2017-08-23 02:08:38.000000000 -0600 -+++ jc/jc_region.ml 2017-12-05 21:01:36.269076188 -0700 -@@ -244,8 +244,8 @@ struct - jc_reg_variable = false; - jc_reg_bitwise = false; - jc_reg_id = id; -- jc_reg_name = name; -- jc_reg_final_name = name ^ "_" ^ (string_of_int id); -+ jc_reg_name = (Bytes.to_string name); -+ jc_reg_final_name = (Bytes.to_string name) ^ "_" ^ (string_of_int id); - jc_reg_type = ty; - } - -@@ -258,8 +258,8 @@ struct - jc_reg_variable = true; - jc_reg_bitwise = false; - jc_reg_id = id; -- jc_reg_name = name; -- jc_reg_final_name = name ^ "_" ^ (string_of_int id); -+ jc_reg_name = (Bytes.to_string name); -+ jc_reg_final_name = (Bytes.to_string name) ^ "_" ^ (string_of_int id); - jc_reg_type = ty; - } - ---- src/lib.ml.orig 2017-08-23 02:08:38.000000000 -0600 -+++ src/lib.ml 2017-12-05 20:43:07.384255238 -0700 -@@ -54,7 +54,7 @@ let file_subdir ~dir ~file = - let file_copy src dest = - let cin = open_in src - and cout = open_out dest -- and buff = String.make 1024 ' ' -+ and buff = Bytes.make 1024 ' ' - and n = ref 0 - in - while n := input cin buff 0 1024; !n <> 0 do -@@ -68,10 +68,10 @@ let file_copy_if_different src dst = - - let channel_contents_buf cin = - let buf = Buffer.create 1024 -- and buff = String.make 1024 ' ' in -+ and buff = Bytes.make 1024 ' ' in - let n = ref 0 in - while n := input cin buff 0 1024; !n <> 0 do -- Buffer.add_substring buf buff 0 !n -+ Buffer.add_subbytes buf buff 0 !n - done; - buf - diff --git a/why.spec b/why.spec index 9c84a8c..51bcff0 100644 --- a/why.spec +++ b/why.spec @@ -5,12 +5,9 @@ %global has_pvs 0 %endif -# What kind of ocaml build to do -%global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0) - Name: why -Version: 2.39 -Release: 5%{?dist} +Version: 2.40 +Release: 1%{?dist} Summary: Software verification platform License: LGPLv2 with exceptions @@ -33,6 +30,8 @@ Patch0: %{name}-project.patch Patch1: %{name}-safe-string.patch # Adapt to ocaml 4.06 in general Patch2: %{name}-ocaml-4.06.patch +# Finish an incomplete Num to zarith conversion +Patch3: %{name}-num.patch BuildRequires: auto-destdir BuildRequires: desktop-file-utils @@ -41,10 +40,9 @@ BuildRequires: frama-c BuildRequires: gappalib-coq BuildRequires: ocaml BuildRequires: ocaml-apron-devel -BuildRequires: ocaml-camlp4-devel +BuildRequires: ocaml-camlp5-devel BuildRequires: ocaml-findlib BuildRequires: ocaml-mlgmpidl-devel -BuildRequires: ocaml-num-devel BuildRequires: ocaml-ocamldoc BuildRequires: ocaml-ocamlgraph-devel BuildRequires: ocaml-zarith-devel @@ -58,10 +56,6 @@ Requires: gappalib-coq Requires: hicolor-icon-theme Requires: emacs-filesystem -# This can be removed once Fedora 25 reaches EOL -Obsoletes: %{name}-coq < 2.36-1 -Provides: %{name}-coq = %{version}-%{release} - # Filter out bogus requires %global __requires_exclude ocaml\\\((Ast|Cc|Env|Error|Jc_ast|Jc_env|Loc|Logic|Logic_decl|Misc|Ptree|Types)\\\) @@ -114,7 +108,7 @@ Requires: why-jessie%{?_isa} = %{version}-%{release} %if %{has_pvs} Requires: why-pvs-support%{?_isa} = %{version}-%{release} %endif -Requires: alt-ergo z3 zenon +Requires: alt-ergo yices z3 zenon %description all This package provides a complete software verification platform suite @@ -126,6 +120,7 @@ based on Why, including various automated and interactive provers. %patch0 %patch1 %patch2 +%patch3 # The other part of avoiding the "Project" module name clash mv src/project.ml src/whyproject.ml @@ -163,10 +158,10 @@ sed -ri 's,ocaml(c|opt),& -g,' atp/Makefile sed -i 's/pvs/pvs-sbcl/' configure %build -%if ! %{opt} -%global opt_option OCAMLBEST=byte OCAMLDEP=ocamldep OCAMLYACC=ocamlyacc OCAMLLEX=ocamllex -%else +%ifarch %{ocaml_native_compiler} %global opt_option OCAMLBEST=opt +%else +%global opt_option OCAMLBEST=byte OCAMLDEP=ocamldep OCAMLYACC=ocamlyacc OCAMLLEX=ocamllex %endif %configure --enable-apron --enable-verbosemake @@ -248,6 +243,10 @@ make check %changelog +* Mon Feb 12 2018 Jerry James - 2.40-1 +- New upstream release +- Add -num patch to fix incomplete num to zarith conversion + * Fri Feb 09 2018 Fedora Release Engineering - 2.39-5 - Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild From 818c9b944e6e345ca9f9250ba57ffd4c9184cd74 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sat, 14 Jul 2018 08:49:51 +0000 Subject: [PATCH 06/22] - Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild Signed-off-by: Fedora Release Engineering --- why.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/why.spec b/why.spec index 51bcff0..3ac8549 100644 --- a/why.spec +++ b/why.spec @@ -7,7 +7,7 @@ Name: why Version: 2.40 -Release: 1%{?dist} +Release: 2%{?dist} Summary: Software verification platform License: LGPLv2 with exceptions @@ -243,6 +243,9 @@ make check %changelog +* Sat Jul 14 2018 Fedora Release Engineering - 2.40-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild + * Mon Feb 12 2018 Jerry James - 2.40-1 - New upstream release - Add -num patch to fix incomplete num to zarith conversion From e3863b543fd1b1f96d5b5b3a27a2b2db3dce698f Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sat, 26 Jan 2019 08:19:32 -0700 Subject: [PATCH 07/22] New upstream release. All patches have been upstreamed; drop them all. --- .gitignore | 5 +- sources | 2 +- why-num.patch | 596 ------------------------------------------ why-ocaml-4.06.patch | 11 - why-project.patch | 115 -------- why-safe-string.patch | 19 -- why.spec | 38 +-- 7 files changed, 14 insertions(+), 772 deletions(-) delete mode 100644 why-num.patch delete mode 100644 why-ocaml-4.06.patch delete mode 100644 why-project.patch delete mode 100644 why-safe-string.patch diff --git a/.gitignore b/.gitignore index 31ca9a5..81c4283 100644 --- a/.gitignore +++ b/.gitignore @@ -1,6 +1,3 @@ /krakatoa.pdf /why-icons.tar.xz -/why-2.36.tar.gz -/why-2.38.tar.gz -/why-2.39.tar.gz -/why-2.40.tar.gz +/why-*.tar.gz diff --git a/sources b/sources index 2db9799..aeca842 100644 --- a/sources +++ b/sources @@ -1,3 +1,3 @@ SHA512 (krakatoa.pdf) = 5d0f4e6b938ddc1eafa48264c02cf99e68f776a7e190b997e35fb2cd154627b5d27369886f570cbcfdfe5f3a1929a97a1fec9457a6f6662f83cbb2e51f65ca04 -SHA512 (why-2.40.tar.gz) = e99f528ab2a3030c5ed8509ec45e75dc2f3dc2ed92fe1213c2b92a2dc700e2d9c32bc765751b2660cc1f3a6e110b4687a4262779fdae52faaaf144c411712972 +SHA512 (why-2.41.tar.gz) = 2e31ed2642a29ecbbc05954f2aa5c841befa68959f571bcde134a56639cec49a51351e5c7781a1a50fc531f2111b5649c710fa3e60c0f71f222b192d8c41cc86 SHA512 (why-icons.tar.xz) = d6ca78cf09540f5742564912470fb8c49f7d11ca16cd8bb60c8790af10c1591198f6020bd792cff8e3464f762b7ef0a690d3e4ba1a2cf670c286c8056d266bc3 diff --git a/why-num.patch b/why-num.patch deleted file mode 100644 index 10b0164..0000000 --- a/why-num.patch +++ /dev/null @@ -1,596 +0,0 @@ ---- atp/cooper.ml.orig 2018-01-23 03:07:35.000000000 -0700 -+++ atp/cooper.ml 2018-02-11 20:48:48.754907226 -0700 -@@ -38,10 +38,10 @@ - (* Lift operations up to numerals. *) - (* ------------------------------------------------------------------------- *) - --let mk_numeral n = Fn(string_of_num n,[]);; -+let mk_numeral n = Fn(Z.to_string n,[]);; - - let dest_numeral = -- function (Fn(ns,[])) -> num_of_string ns -+ function (Fn(ns,[])) -> Z.of_string ns - | _ -> failwith "dest_numeral";; - - let is_numeral = can dest_numeral;; -@@ -59,12 +59,12 @@ let numeral2 fn m n = mk_numeral(fn (des - (* ------------------------------------------------------------------------- *) - - let rec linear_cmul n tm = -- if n =/ Int 0 then Fn("0",[]) else -+ if Z.equal n Z.zero then Fn("0",[]) else - match tm with - Fn("+",[Fn("*",[c1; x1]); rest]) -> -- Fn("+",[Fn("*",[numeral1 (( */ ) n) c1; x1]); -+ Fn("+",[Fn("*",[numeral1 (Z.mul n) c1; x1]); - linear_cmul n rest]) -- | k -> numeral1 (( */ ) n) k;; -+ | k -> numeral1 (Z.mul n) k;; - - let earlierv vars (Var x) (Var y) = earlier vars x y;; - -@@ -73,7 +73,7 @@ let rec linear_add vars tm1 tm2 = - (Fn("+",[Fn("*",[c1; x1]); rest1]), - Fn("+",[Fn("*",[c2; x2]); rest2])) -> - if x1 = x2 then -- let c = numeral2 (+/) c1 c2 in -+ let c = numeral2 Z.add c1 c2 in - if c = Fn("0",[]) then linear_add vars rest1 rest2 - else Fn("+",[Fn("*",[c; x1]); linear_add vars rest1 rest2]) - else if earlierv vars x1 x2 then -@@ -84,9 +84,9 @@ let rec linear_add vars tm1 tm2 = - Fn("+",[Fn("*",[c1; x1]); linear_add vars rest1 tm2]) - | (_,Fn("+",[Fn("*",[c2; x2]); rest2])) -> - Fn("+",[Fn("*",[c2; x2]); linear_add vars tm1 rest2]) -- | _ -> numeral2 (+/) tm1 tm2;; -+ | _ -> numeral2 Z.add tm1 tm2;; - --let linear_neg tm = linear_cmul (Int(-1)) tm;; -+let linear_neg tm = linear_cmul Z.minus_one tm;; - - let linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2);; - -@@ -116,7 +116,7 @@ let mkatom vars p t = Atom(R(p,[Fn("0",[ - let linform vars fm = - match fm with - Atom(R("divides",[c;t])) -> -- let c' = mk_numeral(abs_num(dest_numeral c)) in -+ let c' = mk_numeral(Z.abs(dest_numeral c)) in - Atom(R("divides",[c';lint vars t])) - | Atom(R("=",[s;t])) -> mkatom vars "=" (Fn("-",[t;s])) - | Atom(R("<",[s;t])) -> mkatom vars "<" (Fn("-",[t;s])) -@@ -144,11 +144,11 @@ let rec posineq fm = - let rec formlcm x fm = - match fm with - Atom(R(p,[_;Fn("+",[Fn("*",[c;y]);z])])) when y = x -> -- abs_num(dest_numeral c) -+ Z.abs(dest_numeral c) - | Not(p) -> formlcm x p - | And(p,q) -> lcm_num (formlcm x p) (formlcm x q) - | Or(p,q) -> lcm_num (formlcm x p) (formlcm x q) -- | _ -> Int 1;; -+ | _ -> Z.one;; - - (* ------------------------------------------------------------------------- *) - (* Adjust all coefficients of x in formula; fold in reduction to +/- 1. *) -@@ -157,10 +157,10 @@ let rec formlcm x fm = - let rec adjustcoeff x l fm = - match fm with - Atom(R(p,[d; Fn("+",[Fn("*",[c;y]);z])])) when y = x -> -- let m = l // dest_numeral c in -- let n = if p = "<" then abs_num(m) else m in -- let xtm = Fn("*",[mk_numeral(m // n); x]) in -- Atom(R(p,[linear_cmul (abs_num m) d; -+ let m = Z.div l (dest_numeral c) in -+ let n = if p = "<" then Z.abs(m) else m in -+ let xtm = Fn("*",[mk_numeral(Z.div m n); x]) in -+ Atom(R(p,[linear_cmul (Z.abs m) d; - Fn("+",[xtm; linear_cmul n z])])) - | Not(p) -> Not(adjustcoeff x l p) - | And(p,q) -> And(adjustcoeff x l p,adjustcoeff x l q) -@@ -174,7 +174,7 @@ let rec adjustcoeff x l fm = - let unitycoeff x fm = - let l = formlcm x fm in - let fm' = adjustcoeff x l fm in -- if l =/ Int 1 then fm' else -+ if Z.equal l Z.one then fm' else - let xp = Fn("+",[Fn("*",[Fn("1",[]);x]); Fn("0",[])]) in - And(Atom(R("divides",[mk_numeral l; xp])),adjustcoeff x l fm);; - -@@ -204,7 +204,7 @@ let rec divlcm x fm = - | Not(p) -> divlcm x p - | And(p,q) -> lcm_num (divlcm x p) (divlcm x q) - | Or(p,q) -> lcm_num (divlcm x p) (divlcm x q) -- | _ -> Int 1;; -+ | _ -> Z.one;; - - (* ------------------------------------------------------------------------- *) - (* Construct the B-set. *) -@@ -242,8 +242,8 @@ let rec linrep vars x t fm = - (* ------------------------------------------------------------------------- *) - - let operations = -- ["=",(=/); "<",(",(>/); "<=",(<=/); ">=",(>=/); -- "divides",(fun x y -> mod_num y x =/ Int 0)];; -+ ["=",(Z.equal); "<",(Z.lt); ">",(Z.gt); "<=",(Z.leq); ">=",(Z.geq); -+ "divides",(fun x y -> Z.equal (Z.rem y x) Z.zero)];; - - let evalc_atom at = - match at with -@@ -265,7 +265,7 @@ let cooper vars fm = - let x = Var x0 in - let p = unitycoeff x p0 in - let p_inf = simplify(minusinf x p) and bs = bset x p -- and js = Int 1 --- divlcm x p in -+ and js = Z.one --- divlcm x p in - let p_element j b = - linrep vars x (linear_add vars b (mk_numeral j)) p in - let stage j = list_disj ---- atp/defcnf.ml.orig 2018-01-23 03:07:35.000000000 -0700 -+++ atp/defcnf.ml 2018-02-11 14:00:03.159892859 -0700 -@@ -55,7 +55,7 @@ let rec nenf fm = - (* Make a stylized variable and update the index. *) - (* ------------------------------------------------------------------------- *) - --let mkprop n = Atom(P("p_"^(string_of_num n))),n +/ Int 1;; -+let mkprop n = Atom(P("p_"^(Z.to_string n))),Z.succ n;; - - (* ------------------------------------------------------------------------- *) - (* Make n large enough that "v_m" won't clash with s for any m >= n *) -@@ -67,7 +67,7 @@ let max_varindex pfx = - let l = String.length s in - if l <= m or String.sub s 0 m <> pfx then n else - let s' = String.sub s m (l - m) in -- if forall numeric (explode s') then max_num n (num_of_string s') -+ if forall numeric (explode s') then Z.max n (Z.of_string s') - else n;; - - (* ------------------------------------------------------------------------- *) -@@ -90,7 +90,7 @@ and defstep op (p,q) (fm,defs,n) = - - let defcnf fm = - let fm' = nenf(psimplify fm) in -- let n = Int 1 +/ overatoms (max_varindex "p_" ** pname) fm' (Int 0) in -+ let n = Z.succ (overatoms (max_varindex "p_" ** pname) fm' Z.zero) in - let (fm'',defs,_) = maincnf (fm',undefined,n) in - let deflist = map (snd ** snd) (funset defs) in - let subcnfs = itlist ((@) ** simpcnf) deflist (simpcnf fm'') in -@@ -130,7 +130,7 @@ let rec andcnf (fm,defs,n as trip) = - - let defcnfs fm = - let fm' = nenf(psimplify fm) in -- let n = Int 1 +/ overatoms (max_varindex "p_" ** pname) fm' (Int 0) in -+ let n = Z.succ (overatoms (max_varindex "p_" ** pname) fm' Z.zero) in - let (fm'',defs,_) = andcnf (fm',undefined,n) in - let deflist = map (snd ** snd) (funset defs) in - setify(itlist ((@) ** simpcnf) deflist (simpcnf fm''));; -@@ -181,7 +181,7 @@ let rec andcnf pos (fm,defs,n as trip) = - - let defcnfs imps fm = - let fm' = nenf(psimplify fm) in -- let n = Int 1 +/ overatoms (max_varindex "p_" ** pname) fm' (Int 0) in -+ let n = Z.succ (overatoms (max_varindex "p_" ** pname) fm' Z.zero) in - let (fm'',defs,_) = andcnf imps (fm',undefined,n) in - let deflist = map (snd ** snd) (funset defs) in - setify(itlist ((@) ** simpcnf) deflist (simpcnf fm''));; -@@ -209,7 +209,7 @@ let rec andcnf3 pos (fm,defs,n as trip) - - let defcnf3s imps fm = - let fm' = nenf(psimplify fm) in -- let n = Int 1 +/ overatoms (max_varindex "p_" ** pname) fm' (Int 0) in -+ let n = Z.succ (overatoms (max_varindex "p_" ** pname) fm' Z.zero) in - let (fm'',defs,_) = andcnf3 imps (fm',undefined,n) in - let deflist = map (snd ** snd) (funset defs) in - setify(itlist ((@) ** simpcnf) deflist (simpcnf fm''));; ---- atp/fourier_motzkin.ml.orig 2018-01-23 03:07:35.000000000 -0700 -+++ atp/fourier_motzkin.ml 2018-02-11 20:34:13.822886848 -0700 -@@ -71,10 +71,10 @@ let rec posineq fm = - let rec adjustcoeff x l fm = - match fm with - Atom(R(p,[d; Fn("+",[Fn("*",[c;y]);z])])) when y = x -> -- let m = l // dest_numeral c in -- let n = if p = "<=" then abs_num(m) else m in -- let xtm = Fn("*",[mk_numeral(m // n); x]) in -- Atom(R(p,[linear_cmul (abs_num m) d; -+ let m = Z.div l (dest_numeral c) in -+ let n = if p = "<=" then Z.abs(m) else m in -+ let xtm = Fn("*",[mk_numeral(Z.div m n); x]) in -+ Atom(R(p,[linear_cmul (Z.abs m) d; - Fn("+",[xtm; linear_cmul n z])])) - | Not(p) -> Not(adjustcoeff x l p) - | And(p,q) -> And(adjustcoeff x l p,adjustcoeff x l q) -@@ -88,7 +88,7 @@ let rec adjustcoeff x l fm = - let unitycoeff x fm = - let l = formlcm x fm in - let fm' = adjustcoeff x l fm in -- if l =/ Int 1 then fm' else -+ if Z.equal l Z.one then fm' else - adjustcoeff x l fm;; - - (* ------------------------------------------------------------------------- *) -@@ -98,10 +98,10 @@ let unitycoeff x fm = - let isolate x fm = - match fm with - Atom(R(p,[_;Fn("+",[Fn("*",[c;y]);z])])) when y = x -> -- let c = mk_numeral (Int 0 -/ dest_numeral c) in -+ let c = mk_numeral (Z.sub Z.zero (dest_numeral c)) in - Atom(R(p,[Fn("*",[c;y]);z])) - | Atom(R(p,[zero;Fn("*",[c;y])])) when y = x -> -- let c = mk_numeral (Int 0 -/ dest_numeral c) in -+ let c = mk_numeral (Z.sub Z.zero (dest_numeral c)) in - Atom(R(p,[Fn("*",[c;y]);zero])) - | _ -> - printer fm; -@@ -110,7 +110,7 @@ let isolate x fm = - let replace vars x t fm = - match fm with - Atom(R(p,[Fn("*",[c;y]);z])) when y = x -> -- let t = if dest_numeral c >/ Int 0 then t else linear_neg t in -+ let t = if Z.gt (dest_numeral c) Z.zero then t else linear_neg t in - linform vars (Atom(R(p,[t;z]))) - | _ -> assert false - -@@ -128,13 +128,13 @@ let fourier vars fm = - (function (Atom(R("=",_))) -> true | _ -> false) cjs in - let (Atom(R("=",[s;t]))) = eqn in - let (Fn("*",[c;_])) = s in -- let y = if dest_numeral c =/ Int 1 then t else linear_neg t in -+ let y = if Z.equal (dest_numeral c) Z.one then t else linear_neg t in - list_conj(map (replace vars x y) (subtract cjs [eqn])) - with Failure _ -> - let l,r = - partition - (fun (Atom(R("<=",[Fn("*",[c;_]);t]))) -> -- dest_numeral c =/ Int (-1)) cjs -+ Z.equal (dest_numeral c) Z.minus_one) cjs - in - let lefts = map (fun (Atom(R("<=",[_;l]))) -> linear_neg l) l - and rights = map (fun (Atom(R("<=",[_;r]))) -> r) r in ---- atp/lib.ml.orig 2018-01-23 03:07:35.000000000 -0700 -+++ atp/lib.ml 2018-02-11 13:26:57.020559495 -0700 -@@ -46,11 +46,9 @@ let ( ** ) = fun f g x -> f(g x);; - (* GCD and LCM on arbitrary-precision numbers. *) - (* ------------------------------------------------------------------------- *) - --let gcd_num n1 n2 = -- abs_num(num_of_big_int -- (Big_int.gcd_big_int (big_int_of_num n1) (big_int_of_num n2)));; -+let gcd_num n1 n2 = Z.gcd n1 n2;; - --let lcm_num n1 n2 = abs_num(n1 */ n2) // gcd_num n1 n2;; -+let lcm_num n1 n2 = Z.lcm n1 n2;; - - (* ------------------------------------------------------------------------- *) - (* A useful idiom for "non contradictory" etc. *) -@@ -73,7 +71,7 @@ let can f x = try f x; true with Failure - - let rec (--) = fun m n -> if m > n then [] else m::((m + 1) -- n);; - --let rec (---) = fun m n -> if m >/ n then [] else m::((m +/ Int 1) --- n);; -+let rec (---) = fun m n -> if Z.gt m n then [] else m::((Z.succ m) --- n);; - - let rec map2 f l1 l2 = - match (l1,l2) with -@@ -596,4 +594,4 @@ let equated (Partition f) = dom f;; - (* First number starting at n for which p succeeds. *) - (* ------------------------------------------------------------------------- *) - --let rec first n p = if p(n) then n else first (n +/ Int 1) p;; -+let rec first n p = if p(n) then n else first (Z.succ n) p;; ---- atp/Makefile.orig 2018-01-23 03:07:35.000000000 -0700 -+++ atp/Makefile 2018-02-11 13:14:15.311777144 -0700 -@@ -8,6 +8,8 @@ - # many.ml (Example relevant to many-sorted logic) - # hol.ml (Simple higher order logic setup) - -+ZARITHLIB=$(shell ocamlfind query zarith) -+ - #MLFILES = lib.ml intro.ml formulas.ml prop.ml propexamples.ml \ - defcnf.ml dp.ml stal.ml bdd.ml fol.ml skolem.ml \ - herbrand.ml unif.ml tableaux.ml resolution.ml prolog.ml \ -@@ -33,9 +35,9 @@ compiled: example.ml atp.cmx; ocamlopt - - - # Make the appropriate object for the main body of code - --atp.cmx: atp.ml; ocamlopt -w ax -c atp.ml -+atp.cmx: atp.ml; ocamlopt -I $(ZARITHLIB) -w ax -c atp.ml - --atp.cmo: atp.ml; ocamlc -w ax -c atp.ml -+atp.cmo: atp.ml; ocamlc -I $(ZARITHLIB) -w ax -c atp.ml - - # Make the camlp4 quotation expander - ---- atp/make.ml.orig 2018-01-23 03:07:35.000000000 -0700 -+++ atp/make.ml 2018-02-11 14:37:48.178019612 -0700 -@@ -44,10 +44,9 @@ - Gc.set { (Gc.get()) with Gc.stack_limit = 16777216 };; (* Up the stack size *) - Format.set_margin 72;; (* Reduce margins *) - open Format;; (* Open formatting *) --open Num;; (* Open bignums *) - let imperative_assign = (:=);; (* Preserve this *) - --let print_num n = print_string(string_of_num n);; (* Avoid range limit *) -+let print_num n = print_string(Z.to_string n);; (* Avoid range limit *) - #install_printer print_num;; (* when printing nums *) - - (* ------------------------------------------------------------------------- *) ---- atp/Mk_ml_file.orig 2018-01-23 03:07:35.000000000 -0700 -+++ atp/Mk_ml_file 2018-02-10 22:01:01.925304810 -0700 -@@ -1,4 +1,3 @@ --echo "open Num;;" - echo "open Format;;" - - cat $@ | sed 's/START_INTERACTIVE;;/(\*/' | sed 's/END_INTERACTIVE;;/\*)/' ---- jc/jc_annot_inference.ml.orig 2018-02-10 16:03:04.338379961 -0700 -+++ jc/jc_annot_inference.ml 2018-02-11 13:13:48.313855743 -0700 -@@ -49,7 +49,6 @@ open Apron - open Coeff - open Interval - open Lincons1 --open Num - - - (*****************************************************************************) -@@ -1120,7 +1119,7 @@ let linearize t = - try match t#node with - | JCTconst c -> - begin match c with -- | JCCinteger s -> (TermMap.empty, num_of_string s) -+ | JCCinteger s -> (TermMap.empty, Z.of_string s) - | JCCboolean _ | JCCvoid | JCCnull | JCCreal _ | JCCstring _ -> - err () - end -@@ -1133,7 +1132,7 @@ let linearize t = - (fun vt1 c1 acc -> - try - let c2 = TermMap.find vt1 coeffs2 in -- TermMap.add vt1 (c1 +/ c2) acc -+ TermMap.add vt1 (Z.add c1 c2) acc - with Not_found -> TermMap.add vt1 c1 acc - ) coeffs1 TermMap.empty - in -@@ -1143,55 +1142,55 @@ let linearize t = - else TermMap.add vt2 c2 acc - ) coeffs2 coeffs - in -- (coeffs, cst1 +/ cst2) -+ (coeffs, (Z.add cst1 cst2)) - | `Bsub -> - let coeffs = TermMap.fold - (fun vt1 c1 acc -> - try - let c2 = TermMap.find vt1 coeffs2 in -- TermMap.add vt1 (c1 -/ c2) acc -+ TermMap.add vt1 (Z.sub c1 c2) acc - with Not_found -> TermMap.add vt1 c1 acc - ) coeffs1 TermMap.empty - in - let coeffs = TermMap.fold - (fun vt2 c2 acc -> - if TermMap.mem vt2 coeffs then acc -- else TermMap.add vt2 (minus_num c2) acc -+ else TermMap.add vt2 (Z.neg c2) acc - ) coeffs2 coeffs - in -- (coeffs, cst1 -/ cst2) -+ (coeffs, (Z.sub cst1 cst2)) - | `Bmul when TermMap.is_empty coeffs1 || TermMap.is_empty coeffs2 -> - let coeffs = - if TermMap.is_empty coeffs1 then -- TermMap.map (fun c -> c */ cst1) coeffs2 -+ TermMap.map (fun c -> Z.mul c cst1) coeffs2 - else -- TermMap.map (fun c -> c */ cst2) coeffs1 -+ TermMap.map (fun c -> Z.mul c cst2) coeffs1 - in -- (coeffs, cst1 */ cst2) -+ (coeffs, (Z.mul cst1 cst2)) - | `Bmul - | `Bdiv - | `Bmod -> err () - end - | JCTbinary(t1,(#bitwise_op as bop,`Integer),t2) -> - let coeffs1, cst1 = aux t1 in -- if coeffs1 = TermMap.empty && cst1 =/ Int 0 then -+ if coeffs1 = TermMap.empty && Z.equal cst1 Z.zero then - match bop with - | `Bbw_and - | `Bshift_left - | `Blogical_shift_right -- | `Barith_shift_right -> TermMap.empty, Int 0 -+ | `Barith_shift_right -> TermMap.empty, Z.zero - | `Bbw_or - | `Bbw_xor -> aux t2 - | _ -> err () - else - (* Consider non-linear term as abstract variable. *) -- (TermMap.add t (Int 1) TermMap.empty, Int 0) -+ (TermMap.add t Z.one TermMap.empty, Z.zero) - | JCTunary((uop,`Integer),t1) -> - let coeffs1,cst1 = aux t1 in - begin match uop with - | `Uminus -> -- let coeffs = TermMap.map (fun c -> minus_num c) coeffs1 in -- (coeffs, minus_num cst1) -+ let coeffs = TermMap.map (fun c -> Z.neg c) coeffs1 in -+ (coeffs, Z.neg cst1) - | _ -> err () - end - | JCTvar _ | JCTderef _ | JCToffset _ | JCTapp _ | JCTbinary _ -@@ -1201,13 +1200,16 @@ let linearize t = - | JCTrange _ | JCTif _ | JCTlet _ -> - err () - with Failure "linearize" -> -- (TermMap.add t (Int 1) TermMap.empty, Int 0) -+ (TermMap.add t Z.one TermMap.empty, Z.zero) - in aux t - - let linstr_of_term env t = -+(* - let mkmulstr = function -- | (_va, Int 0) -> "" -- | (va, c) -> string_of_num c ^ " * " ^ va -+ | (_va, Z.zero) -> "" -+ | (va, c) -> (Z.to_string c) ^ " * " ^ va -+*) -+ let mkmulstr = (fun (va,c) -> if Z.equal Z.zero c then "" else (Z.to_string c) ^ " * " ^ va) - in - let rec mkaddstr = function - | [] -> "" -@@ -1286,33 +1288,33 @@ let rec linstr_of_assertion env a = - in - let env,str,cst = linstr_of_term env subt in - if str = "" then -- let ncst = minus_num cst in -+ let ncst = Z.neg cst in - let is_true = match bop with -- | `Blt -> Int 0 Int 0 >/ ncst -- | `Ble -> Int 0 <=/ ncst -- | `Bge -> Int 0 >=/ ncst -- | `Beq -> Int 0 =/ ncst -- | `Bneq -> Int 0 <>/ ncst -+ | `Blt -> Z.lt Z.zero ncst -+ | `Bgt -> Z.gt Z.zero ncst -+ | `Ble -> Z.leq Z.zero ncst -+ | `Bge -> Z.geq Z.zero ncst -+ | `Beq -> Z.equal Z.zero ncst -+ | `Bneq -> not (Z.equal Z.zero ncst) - in - env, if is_true then Dnf.true_ else Dnf.false_ - else -- let cstr = string_of_num (minus_num cst) in -+ let cstr = Z.to_string (Z.neg cst) in - (* Do not use < and > with APRON, due to bugs in some versions. - Convert to equivalent non-strict. *) - let str = match bop with - | `Blt -> [[str ^ " <= " ^ -- (string_of_num (pred_num (minus_num cst)))]] -+ (Z.to_string (Z.pred (Z.neg cst)))]] - | `Bgt -> [[str ^ " >= " ^ -- (string_of_num (succ_num (minus_num cst)))]] -+ (Z.to_string (Z.succ (Z.neg cst)))]] - | `Ble -> [[str ^ " <= " ^ cstr]] - | `Bge -> [[str ^ " >= " ^ cstr]] - | `Beq -> [[str ^ " = " ^ cstr]] - | `Bneq -> - [[str ^ " <= " ^ -- (string_of_num (pred_num (minus_num cst)))]; -+ (Z.to_string (Z.pred (Z.neg cst)))]; - [str ^ " >= " ^ -- (string_of_num (succ_num (minus_num cst)))]] -+ (Z.to_string (Z.succ (Z.neg cst)))]] - in - env, str - | JCAnot a -> -@@ -1330,8 +1332,8 @@ let rec linstr_of_assertion env a = - let linstr_of_expr env e = - match Jc_effect.term_of_expr e with None -> None | Some t -> - let env,str,cst = linstr_of_term env t in -- if str = "" then Some (env, string_of_num cst) -- else Some (env, str ^ " + " ^ (string_of_num cst)) -+ if str = "" then Some (env, Z.to_string cst) -+ else Some (env, str ^ " + " ^ (Z.to_string cst)) - - let offset_linstr_of_expr env ok e = - match e#node with -@@ -1340,15 +1342,15 @@ let offset_linstr_of_expr env ok e = - else - begin match Jc_effect.term_of_expr e with None -> None | Some t -> - let env,str,cst = linstr_of_term env t in -- if str = "" then Some (env,string_of_num cst) -- else Some (env,str ^ " + " ^ (string_of_num cst)) -+ if str = "" then Some (env,Z.to_string cst) -+ else Some (env,str ^ " + " ^ (Z.to_string cst)) - end - | _ -> - if is_nonnull_pointer_type e#typ then - match Jc_effect.term_of_expr e with None -> None | Some t -> - let env,str,cst = offset_linstr_of_term env ok t in -- if str = "" then Some (env,string_of_num cst) -- else Some (env,str ^ " + " ^ (string_of_num cst)) -+ if str = "" then Some (env,Z.to_string cst) -+ else Some (env,str ^ " + " ^ (Z.to_string cst)) - else None - - -@@ -1419,13 +1421,13 @@ let mkassertion lincons = - - let rec linterms_of_term t = - let mkmulterm (t,c) = -- if c =/ Int 0 then None -- else if c =/ Int 1 then Some t -- else if c =/ Int (-1) then -+ if Z.equal c Z.zero then None -+ else if Z.equal c Z.one then Some t -+ else if Z.equal c Z.minus_one then - Some(new term ~typ:integer_type (JCTunary((`Uminus,`Integer),t))) - else - let c = -- new term ~typ:integer_type (JCTconst(JCCinteger(string_of_num c))) -+ new term ~typ:integer_type (JCTconst(JCCinteger(Z.to_string c))) - in - Some(new term ~typ:integer_type (JCTbinary(c,(`Bmul,`Integer),t))) - in -@@ -1443,30 +1445,30 @@ let rec linterms_of_term t = - let coeffs,cst = linearize t in - let posl,negl = - TermMap.fold (fun t c (pl,nl) -> -- if c >/ Int 0 then (t,c) :: pl, nl -- else if c -- if cst >/ Int 0 then cstt -+ if Z.gt cst Z.zero then cstt - else new term ~typ:integer_type (JCTconst(JCCinteger "0")) - | Some t -> -- if cst >/ Int 0 then -+ if Z.gt cst Z.zero then - new term ~typ:integer_type (JCTbinary(t,(`Badd,`Integer),cstt)) - else t - in - let negt = match mkaddterm negl with - | None -> -- if cst -- if cst -- if c >/ Int 0 then t :: pl, nl -- else if c [] | Some t1 -> - let mint = new term ~typ:integer_type -- (JCTconst (JCCinteger (Num.string_of_num ei.jc_enum_info_min))) -+ (JCTconst (JCCinteger (Z.to_string ei.jc_enum_info_min))) - in - let maxt = new term ~typ:integer_type -- (JCTconst(JCCinteger (Num.string_of_num ei.jc_enum_info_max))) -+ (JCTconst(JCCinteger (Z.to_string ei.jc_enum_info_max))) - in - let mina = new assertion (JCArelation (mint, (`Ble,`Integer), t1)) in - let maxa = new assertion (JCArelation (t1, (`Ble,`Integer), maxt)) in diff --git a/why-ocaml-4.06.patch b/why-ocaml-4.06.patch deleted file mode 100644 index 872f38a..0000000 --- a/why-ocaml-4.06.patch +++ /dev/null @@ -1,11 +0,0 @@ ---- Makefile.in.orig 2018-02-10 15:44:26.226883183 -0700 -+++ Makefile.in 2018-02-12 19:34:20.930490137 -0700 -@@ -214,7 +214,7 @@ jc/jc.cmx jc/jc.o: $(JCCMX_EXPORT) - # ppc: jc/jc.cmi jc/jc.cmo jc/jc.cmx - - bin/jessie.opt: $(JCCMX) -- $(if $(QUIET),@echo 'Linking $@' &&) $(OCAMLOPT) $(OFLAGS) $(APRONLIB) $(APRONLIBS) $(ATPLIB) -o $@ \ -+ $(if $(QUIET),@echo 'Linking $@' &&) $(OCAMLOPT) -runtime-variant _pic $(OFLAGS) $(APRONLIB) $(APRONLIBS) $(ATPLIB) -o $@ \ - unix.cmxa str.cmxa zarith.cmxa graph.cmxa $^ - $(STRIP) $@ - diff --git a/why-project.patch b/why-project.patch deleted file mode 100644 index b4536a8..0000000 --- a/why-project.patch +++ /dev/null @@ -1,115 +0,0 @@ ---- Makefile.in.orig 2018-01-23 03:07:35.000000000 -0700 -+++ Makefile.in 2018-02-10 15:44:26.226883183 -0700 -@@ -155,7 +155,7 @@ CMO_EXPORT = src/lib.cmo src/rc.cmo src - src/effect.cmo src/pp.cmo src/option_misc.cmo \ - src/report.cmo \ - src/explain.cmo \ -- src/xml.cmo src/project.cmo -+ src/xml.cmo src/whyproject.cmo - - # jessie - JCCML_EXPORT = src/why3_kw.ml jc/output.ml \ ---- src/options.mli.orig 2018-01-23 03:07:35.000000000 -0700 -+++ src/options.mli 2018-02-10 15:44:26.258883112 -0700 -@@ -184,7 +184,7 @@ val files : string list - (*s GUI? *) - - val gui : bool ref --val gui_project : Project.t option ref -+val gui_project : Whyproject.t option ref - val lib_files_to_load : string list - - (* ---- src/pretty.ml.orig 2018-01-23 03:07:35.000000000 -0700 -+++ src/pretty.ml 2018-02-10 15:44:26.259883110 -0700 -@@ -416,12 +416,12 @@ let output_project f = - with Not_found -> - functions := SMap.add fn SMap.empty !functions) - Util.program_locs ; -- let p = Project.create (Filename.basename f) in -- Project.set_project_context_file p (f ^ "_ctx.why"); -+ let p = Whyproject.create (Filename.basename f) in -+ Whyproject.set_project_context_file p (f ^ "_ctx.why"); - List.iter - (fun (expl,fpo) -> - let n = expl.lemma_or_fun_name in -- let _ = Project.add_lemma p n expl fpo in ()) -+ let _ = Whyproject.add_lemma p n expl fpo in ()) - !lemmas; - SMap.iter - (fun fname behs -> -@@ -431,15 +431,15 @@ let output_project f = - floc - with Not_found -> Loc.dummy_floc - in -- let f = Project.add_function p fname floc in -+ let f = Whyproject.add_function p fname floc in - SMap.iter - (fun beh vcs -> -- let be = Project.add_behavior f beh floc in -+ let be = Whyproject.add_behavior f beh floc in - List.iter - (fun (expl,fpo) -> -- let _ = Project.add_goal be expl fpo in ()) -+ let _ = Whyproject.add_goal be expl fpo in ()) - vcs) - behs) - !functions; -- Project.save p f; -+ Whyproject.save p f; - p ---- src/pretty.mli.orig 2018-01-23 03:07:35.000000000 -0700 -+++ src/pretty.mli 2018-02-10 15:44:26.259883110 -0700 -@@ -50,4 +50,4 @@ val output_files : string -> unit - (* [output_project f] produces a whole project description, in a file - [f.wpr], together with other needed files [f_ctx.why], [f_lemmas.why], - and each goal in a separate file [f_po.why] for i=1,2,... *) --val output_project : string -> Project.t -+val output_project : string -> Whyproject.t ---- src/whyweb.ml.orig 2018-01-23 03:07:35.000000000 -0700 -+++ src/whyweb.ml 2018-02-10 15:44:26.259883110 -0700 -@@ -29,7 +29,7 @@ - (**************************************************************************) - - open Format --open Project -+open Whyproject - - (*prover*) - let provers = [Ergo ; Simplify ; Z3 ; Yices ; Cvc3] -@@ -168,7 +168,7 @@ let file = match !file with - | None -> () - | Some f -> Arg.usage spec usage; exit 1 - --let proj = ref (Project.create "") -+let proj = ref (Whyproject.create "") - - let proj_file = ref "" - -@@ -260,7 +260,7 @@ let interp_com c = - let _ = Thread.create (launch_behavior Cvc3) b in () - | `LaunchCvc3Function f -> - let _ = Thread.create (launch_function Cvc3) f in () -- | `Save -> Project.save !proj !proj.project_name -+ | `Save -> Whyproject.save !proj !proj.project_name - end; - loc - with Not_found -> ("",0,0,0) -@@ -343,7 +343,7 @@ let main_page msg = - let load_prj file = - eprintf "Reading file %s@." file; - try -- proj := Project.load file; -+ proj := Whyproject.load file; - proj_file := file; - with - Sys_error _ -> -@@ -526,7 +526,7 @@ wprint "
Save Proj -
%s%s
" ns; - wprint ""; - List.iter (fun prover -> -- wprint "" (Project.provers_name prover)) -+ wprint "" (Whyproject.provers_name prover)) - provers; - wprint " - "; diff --git a/why-safe-string.patch b/why-safe-string.patch deleted file mode 100644 index 23968d2..0000000 --- a/why-safe-string.patch +++ /dev/null @@ -1,19 +0,0 @@ ---- jc/jc_annot_inference.ml.orig 2018-01-23 03:07:35.000000000 -0700 -+++ jc/jc_annot_inference.ml 2018-02-10 16:03:04.338379961 -0700 -@@ -212,14 +212,14 @@ let name_of_term t = - Format.fprintf str_formatter "%a" Jc_output.term t; - let s = Format.flush_str_formatter () in - let s = filter_alphanumeric s in -- "T" ^ unique_term_name t s -+ "T" ^ unique_term_name t (Bytes.to_string s) - - let name_of_assertion a = - ignore (Format.flush_str_formatter ()); - Format.fprintf str_formatter "%a" Jc_output.assertion a; - let s = Format.flush_str_formatter () in - let s = filter_alphanumeric s in -- "A" ^ unique_assertion_name a s -+ "A" ^ unique_assertion_name a (Bytes.to_string s) - - (* support of (Nicolas) *) - let rec destruct_alloc t = diff --git a/why.spec b/why.spec index 3ac8549..9bead76 100644 --- a/why.spec +++ b/why.spec @@ -6,8 +6,8 @@ %endif Name: why -Version: 2.40 -Release: 2%{?dist} +Version: 2.41 +Release: 1%{?dist} Summary: Software verification platform License: LGPLv2 with exceptions @@ -23,15 +23,6 @@ Source7: rem.pvs Source8: patch_jessie_pvs # Created with gimp from official upstream icon Source9: %{name}-icons.tar.xz -# Avoid a clash between Frama-C and why modules both named "Project". -# Sent upstream 26 Jun 2014. -Patch0: %{name}-project.patch -# Adapt to the safe string feature of ocaml 4.06 -Patch1: %{name}-safe-string.patch -# Adapt to ocaml 4.06 in general -Patch2: %{name}-ocaml-4.06.patch -# Finish an incomplete Num to zarith conversion -Patch3: %{name}-num.patch BuildRequires: auto-destdir BuildRequires: desktop-file-utils @@ -117,14 +108,6 @@ based on Why, including various automated and interactive provers. %prep %setup -q %setup -q -T -D -a 9 -%patch0 -%patch1 -%patch2 -%patch3 - -# The other part of avoiding the "Project" module name clash -mv src/project.ml src/whyproject.ml -mv src/project.mli src/whyproject.mli cp -p %SOURCE2 ./ @@ -157,6 +140,9 @@ sed -ri 's,ocaml(c|opt),& -g,' atp/Makefile # Command "pvs" is LVM2's /sbin/pvs, so rename "pvs" to pvs-sbcl: sed -i 's/pvs/pvs-sbcl/' configure +# Allow building with why3 1.1.1 +sed -i 's,0\.88\.\*,&|1.1.1,' configure + %build %ifarch %{ocaml_native_compiler} %global opt_option OCAMLBEST=opt @@ -206,22 +192,18 @@ cp -p %{SOURCE8} %{buildroot}%{_bindir}/ # Fix up documentation and examples mkdir -p %{buildroot}%{why_doc_dir} -cp -p %{SOURCE1} %{SOURCE3} CHANGES README Version %{buildroot}%{why_doc_dir} +cp -p %{SOURCE1} %{SOURCE2} %{SOURCE3} CHANGES README Version \ + %{buildroot}%{why_doc_dir} %check make check %files -%doc README.why-coq.Fedora %license COPYING LICENSE -%{_bindir}/* +%{_bindir}/krakatoa %{_libdir}/why/ %{_datadir}/icons/hicolor/*/apps/%{name}.png %{why_doc_dir}/ -# why-jessie -%exclude %{_bindir}/jessie -# why-pvs-support: -%exclude %{_bindir}/patch_jessie_pvs %files jessie %{_bindir}/jessie @@ -243,6 +225,10 @@ make check %changelog +* Sat Jan 26 2018 Jerry James - 2.41-1 +- New upstream release +- All patches have been upstreamed; drop them all + * Sat Jul 14 2018 Fedora Release Engineering - 2.40-2 - Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild From 6472c2a08f7f2d882531d3535056abd184e1dbf5 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sat, 26 Jan 2019 08:20:53 -0700 Subject: [PATCH 08/22] Welcome to 2019, Jerry. --- why.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/why.spec b/why.spec index 9bead76..e68251e 100644 --- a/why.spec +++ b/why.spec @@ -225,7 +225,7 @@ make check %changelog -* Sat Jan 26 2018 Jerry James - 2.41-1 +* Sat Jan 26 2019 Jerry James - 2.41-1 - New upstream release - All patches have been upstreamed; drop them all From 1341b9c9efe30f35da0c93d09ecdbb5f1c44df1d Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sun, 3 Feb 2019 11:41:51 +0000 Subject: [PATCH 09/22] - Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild Signed-off-by: Fedora Release Engineering --- why.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/why.spec b/why.spec index e68251e..6113f5d 100644 --- a/why.spec +++ b/why.spec @@ -7,7 +7,7 @@ Name: why Version: 2.41 -Release: 1%{?dist} +Release: 2%{?dist} Summary: Software verification platform License: LGPLv2 with exceptions @@ -225,6 +225,9 @@ make check %changelog +* Sun Feb 03 2019 Fedora Release Engineering - 2.41-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild + * Sat Jan 26 2019 Jerry James - 2.41-1 - New upstream release - All patches have been upstreamed; drop them all From 26b175fd3299d48bbbb3e0e10d82426d8c409162 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 5 Jun 2019 20:08:47 -0600 Subject: [PATCH 10/22] Rebuild for coq 8.9.1, why3 1.2.0, and frama-c 18.0. --- why-frama-c.patch | 757 ++++++++++++++++++++++++++++++++++++++++++++++ why.spec | 18 +- 2 files changed, 772 insertions(+), 3 deletions(-) create mode 100644 why-frama-c.patch diff --git a/why-frama-c.patch b/why-frama-c.patch new file mode 100644 index 0000000..eab0a6b --- /dev/null +++ b/why-frama-c.patch @@ -0,0 +1,757 @@ +--- frama-c-plugin/common.ml.orig 2018-06-28 16:43:25.000000000 -0600 ++++ frama-c-plugin/common.ml 2019-06-03 09:39:40.876316289 -0600 +@@ -56,8 +56,9 @@ let fatal fmt = Jessie_options.fatal ~cu + + let unsupported fmt = + Jessie_options.with_failure +- (fun evt -> +- raise (Unsupported evt.Log.evt_message) ++ (function ++ | (Some evt) -> raise (Unsupported evt.Log.evt_message) ++ | None -> raise (Unsupported "No message") + ) ~current:true fmt + + let warning fmt = Jessie_options.warning ~current:true fmt +--- frama-c-plugin/common.mli.orig 2018-06-28 16:43:25.000000000 -0600 ++++ frama-c-plugin/common.mli 2019-06-03 09:38:56.727035437 -0600 +@@ -102,7 +102,7 @@ val term_of_var : Cil_types.varinfo -> C + val mkterm : + Cil_types.term_node -> + Cil_types.logic_type -> +- Lexing.position * Lexing.position -> Cil_types.term ++ Filepath.position * Filepath.position -> Cil_types.term + + val mkInfo : Cil_types.exp -> Cil_types.exp + +--- frama-c-plugin/interp.ml.orig 2018-06-28 16:43:25.000000000 -0600 ++++ frama-c-plugin/interp.ml 2019-06-03 11:55:36.722081449 -0600 +@@ -702,14 +702,14 @@ let rec coerce_floats t = + if isLogicFloatType t.term_type then + List.map + (fun e -> +- mkexpr (JCPEcast(e, mktype (JCPTnative Treal))) t.term_loc) ++ mkexpr (JCPEcast(e, mktype (JCPTnative Treal))) (Location.to_lexing_loc t.term_loc)) + (terms t) + else terms t + + and terms t = + CurrentLoc.set t.term_loc; + let enode = match constFoldTermNodeAtTop t.term_node with +- | TConst c -> [logic_const t.term_loc c] ++ | TConst c -> [logic_const (Location.to_lexing_loc t.term_loc) c] + + | TDataCons({ctor_type = {lt_name = name} } as d,_args) + when name = Utf8_logic.boolean -> +@@ -727,7 +727,7 @@ and terms t = + | Toffset _ -> Common.unsupported "logic offset" + + | TLval lv -> +- List.map (fun x -> x#node) (terms_lval t.term_loc lv) ++ List.map (fun x -> x#node) (terms_lval (Location.to_lexing_loc t.term_loc) lv) + + | TSizeOf _ | TSizeOfE _ | TSizeOfStr _ | TAlignOf _ | TAlignOfE _ -> + assert false (* Should be removed by constant folding *) +@@ -741,7 +741,7 @@ and terms t = + let t1 = terms t1 in + let t2 = terms t2 in + let expr x y = +- let sube = mkexpr (JCPEbinary(x,`Bsub,y)) t.term_loc in ++ let sube = mkexpr (JCPEbinary(x,`Bsub,y)) (Location.to_lexing_loc t.term_loc) in + JCPEbinary(sube,binop op,zero_expr) + in product expr t1 t2 + +@@ -867,7 +867,7 @@ and terms t = + | TAddrOf _tlv -> assert false (* Should have been rewritten *) + + | TStartOf tlv -> +- List.map (fun x -> x#node) (terms_lval t.term_loc tlv) ++ List.map (fun x -> x#node) (terms_lval (Location.to_lexing_loc t.term_loc) tlv) + + | Tapp(linfo,labels,tlist) -> + begin +@@ -887,7 +887,7 @@ and terms t = + then + List.map + (fun t' -> +- mkexpr (JCPEcast(t', mktype (JCPTnative Treal))) t.term_loc) ++ mkexpr (JCPEcast(t', mktype (JCPTnative Treal))) (Location.to_lexing_loc t.term_loc)) + t' + else t') + prof +@@ -950,17 +950,17 @@ and terms t = + | TLogic_coerce(_,t) -> List.map (fun x -> x#node) (terms t) + + in +- List.map (swap mkexpr t.term_loc) enode ++ List.map (swap mkexpr (Location.to_lexing_loc t.term_loc)) enode + + and tag t = + let tag_node = match t.term_node with + | Ttypeof t -> JCPTtypeof (term t) + | Ttype ty -> +- let id = mkidentifier (get_struct_name (pointed_type ty)) t.term_loc in ++ let id = mkidentifier (get_struct_name (pointed_type ty)) (Location.to_lexing_loc t.term_loc) in + JCPTtag id + | _ -> assert false (* Not a tag *) + in +- mktag tag_node t.term_loc ++ mktag tag_node (Location.to_lexing_loc t.term_loc) + + and terms_lval pos lv = + match lv with +@@ -1042,6 +1042,7 @@ and term t = + *) + and pred p = + CurrentLoc.set p.pred_loc; ++ let ploc = Location.to_lexing_loc p.pred_loc in + let enode = match p.pred_content with + | Pfalse -> JCPEconst(JCCboolean false) + +@@ -1060,7 +1061,7 @@ and pred p = + let t' = term t in + if isLogicFloatType t.term_type && isLogicRealType lv.lv_type + then +- mkexpr (JCPEcast(t', mktype (JCPTnative Treal))) t.term_loc ++ mkexpr (JCPEcast(t', mktype (JCPTnative Treal))) (Location.to_lexing_loc t.term_loc) + else t') + pinfo.l_profile + tl +@@ -1072,7 +1073,7 @@ and pred p = + | Prel((Rlt | Rgt | Rle | Rge as rel),t1,t2) + when app_term_type isPointerType false t1.term_type -> + (* Pointer comparison is translated as subtraction *) +- let sube = mkexpr (JCPEbinary(term t1,`Bsub,term t2)) p.pred_loc in ++ let sube = mkexpr (JCPEbinary(term t1,`Bsub,term t2)) ploc in + JCPEbinary(sube,relation rel,zero_expr) + + (* | Prel((Req | Rneq as rel),t1,t2) *) +@@ -1087,14 +1088,14 @@ and pred p = + JCPEeqtype(tag t1,tag t2) + + | Prel(Rneq,t1,t2) when isTypeTagType t1.term_type -> +- let eq = mkexpr (JCPEeqtype(tag t1,tag t2)) p.pred_loc in ++ let eq = mkexpr (JCPEeqtype(tag t1,tag t2)) ploc in + JCPEunary(`Unot,eq) + + | Prel(rel,t1,t2) -> + let res = +- product (fun t1 t2 -> mkexpr (JCPEbinary(t1,relation rel,t2)) p.pred_loc) ++ product (fun t1 t2 -> mkexpr (JCPEbinary(t1,relation rel,t2)) ploc) + (coerce_floats t1) (coerce_floats t2) +- in (mkconjunct res p.pred_loc)#node ++ in (mkconjunct res ploc)#node + | Pand(p1,p2) -> + JCPEbinary(pred p1,`Bland,pred p2) + +@@ -1170,21 +1171,21 @@ and pred p = + | None,None -> true_expr + | Some t2,None -> + let e2 = term t2 in +- let eoffmin = mkexpr (JCPEoffset(Offset_min,e1)) p.pred_loc in +- mkexpr (JCPEbinary(eoffmin,`Ble,e2)) p.pred_loc ++ let eoffmin = mkexpr (JCPEoffset(Offset_min,e1)) ploc in ++ mkexpr (JCPEbinary(eoffmin,`Ble,e2)) ploc + | None, Some t3 -> + let e3 = term t3 in +- let eoffmax = mkexpr (JCPEoffset(Offset_max,e1)) p.pred_loc in +- mkexpr (JCPEbinary(eoffmax,`Bge,e3)) p.pred_loc ++ let eoffmax = mkexpr (JCPEoffset(Offset_max,e1)) ploc in ++ mkexpr (JCPEbinary(eoffmax,`Bge,e3)) ploc + | Some t2,Some t3 -> + let e2 = term t2 in + let e3 = term t3 in +- let eoffmin = mkexpr (JCPEoffset(Offset_min,e1)) p.pred_loc in +- let emin = mkexpr (JCPEbinary(eoffmin,`Ble,e2)) p.pred_loc in +- let eoffmax = mkexpr (JCPEoffset(Offset_max,e1)) p.pred_loc in +- let emax = mkexpr (JCPEbinary(eoffmax,`Bge,e3)) p.pred_loc in +- mkconjunct [emin; emax] p.pred_loc +- in (mkconjunct (List.map mk_one_pred e1) p.pred_loc)#node ++ let eoffmin = mkexpr (JCPEoffset(Offset_min,e1)) ploc in ++ let emin = mkexpr (JCPEbinary(eoffmin,`Ble,e2)) ploc in ++ let eoffmax = mkexpr (JCPEoffset(Offset_max,e1)) ploc in ++ let emax = mkexpr (JCPEbinary(eoffmax,`Bge,e3)) ploc in ++ mkconjunct [emin; emax] ploc ++ in (mkconjunct (List.map mk_one_pred e1) ploc)#node + + | Pvalid(_lab,{ term_node = TBinOp(PlusPI,t1,t2)}) -> + let e1 = terms t1 in +@@ -1193,23 +1194,23 @@ and pred p = + (List.flatten + (List.map + (fun e1 -> +- let eoffmin = mkexpr (JCPEoffset(Offset_min,e1)) p.pred_loc in +- let emin = mkexpr (JCPEbinary(eoffmin,`Ble,e2)) p.pred_loc in +- let eoffmax = mkexpr (JCPEoffset(Offset_max,e1)) p.pred_loc in +- let emax = mkexpr (JCPEbinary(eoffmax,`Bge,e2)) p.pred_loc in ++ let eoffmin = mkexpr (JCPEoffset(Offset_min,e1)) ploc in ++ let emin = mkexpr (JCPEbinary(eoffmin,`Ble,e2)) ploc in ++ let eoffmax = mkexpr (JCPEoffset(Offset_max,e1)) ploc in ++ let emax = mkexpr (JCPEbinary(eoffmax,`Bge,e2)) ploc in + [emin; emax]) +- e1)) p.pred_loc)#node ++ e1)) ploc)#node + | Pvalid (_lab,t) -> + let elist = + List.flatten (List.map (fun e -> +- let eoffmin = mkexpr (JCPEoffset(Offset_min,e)) p.pred_loc in +- let emin = mkexpr (JCPEbinary(eoffmin,`Ble,zero_expr)) p.pred_loc in +- let eoffmax = mkexpr (JCPEoffset(Offset_max,e)) p.pred_loc in +- let emax = mkexpr (JCPEbinary(eoffmax,`Bge,zero_expr)) p.pred_loc in ++ let eoffmin = mkexpr (JCPEoffset(Offset_min,e)) ploc in ++ let emin = mkexpr (JCPEbinary(eoffmin,`Ble,zero_expr)) ploc in ++ let eoffmax = mkexpr (JCPEoffset(Offset_max,e)) ploc in ++ let emax = mkexpr (JCPEbinary(eoffmax,`Bge,zero_expr)) ploc in + [emin; emax] + ) (terms t)) + in +- (mkconjunct elist p.pred_loc)#node ++ (mkconjunct elist ploc)#node + + | Pvalid_read _ -> Common.unsupported "\\valid_read operator" + +@@ -1236,7 +1237,7 @@ and pred p = + | Pvalid_function _ -> Common.unsupported "\\valid_function" + + in +- mkexpr enode p.pred_loc ++ mkexpr enode ploc + + (* Keep names associated to predicate *) + let named_pred p = +@@ -1492,14 +1493,15 @@ let set_curFundec, get_curFundec = + + let rec expr e = + ++ let eloc = Location.to_lexing_loc e.eloc in + let enode = + let e = stripInfo e in + match e.enode with + | Info _ -> assert false + +- | Const c -> const e.eloc c ++ | Const c -> const eloc c + +- | Lval lv -> (lval e.eloc lv)#node ++ | Lval lv -> (lval eloc lv)#node + + | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ -> + assert false (* Should be removed by constant folding *) +@@ -1509,7 +1511,7 @@ let rec expr e = + + | UnOp(op,e,_ty) -> + let e = +- locate (mkexpr (JCPEunary(unop op,expr e)) e.eloc) ++ locate (mkexpr (JCPEunary(unop op,expr e)) eloc) + in + e#node + +@@ -1518,24 +1520,24 @@ let rec expr e = + + | BinOp(op,e1,e2,_ty) -> + let e = +- locate (mkexpr (JCPEbinary(expr e1,binop op,expr e2)) e.eloc) ++ locate (mkexpr (JCPEbinary(expr e1,binop op,expr e2)) eloc) + in + e#node + + | CastE(ty,e') + when isIntegralType ty && isFloatingType (typeOf e') -> + let e1 = +- locate (mkexpr (JCPEcast(expr e',mktype (JCPTnative Treal))) e.eloc) ++ locate (mkexpr (JCPEcast(expr e',mktype (JCPTnative Treal))) eloc) + in + let e = +- locate (mkexpr (JCPEapp("\\truncate_real_to_int",[],[e1])) e.eloc) ++ locate (mkexpr (JCPEapp("\\truncate_real_to_int",[],[e1])) eloc) + in e#node + + | CastE(ty,e') when isIntegralType ty && isArithmeticType (typeOf e') -> + (integral_expr e)#node + + | CastE(ty,e') when isFloatingType ty && isArithmeticType (typeOf e') -> +- let e = locate (mkexpr (JCPEcast(expr e',ctype ty)) e.eloc) in ++ let e = locate (mkexpr (JCPEcast(expr e',ctype ty)) eloc) in + e#node + + | CastE(ty,e') when isIntegralType ty && isPointerType (typeOf e') -> +@@ -1572,7 +1574,7 @@ let rec expr e = + (* else *) + (* bitwise cast *) + let enode = JCPEcast(expr e,ctype ptrty) in +- let e = locate (mkexpr enode e.eloc) in ++ let e = locate (mkexpr enode eloc) in + e#node + (* let _,ptr_to_ptr = type_conversion ptrty ety in *) + (* JCPEapp(ptr_to_ptr,[],[expr e]) *) +@@ -1600,9 +1602,9 @@ let rec expr e = + + | AddrOf _lv -> assert false (* Should have been rewritten *) + +- | StartOf lv -> (lval e.eloc lv)#node ++ | StartOf lv -> (lval eloc lv)#node + in +- mkexpr enode e.eloc ++ mkexpr enode eloc + + (* Function called when expecting a boolean in Jessie, i.e. when translating + a test or a sub-expression of an "or" or "and". +@@ -1614,6 +1616,7 @@ and boolean_expr e = + else assert false + in + ++ let eloc = Location.to_lexing_loc e.eloc in + let enode = match (stripInfo e).enode with + | Info _ -> assert false + +@@ -1633,43 +1636,44 @@ and boolean_expr e = + JCPEbinary(expr e1,binop op,expr e2) + else + (* Pointer comparison is translated as subtraction *) +- let sube = mkexpr (JCPEbinary(expr e1,`Bsub,expr e2)) e.eloc in ++ let sube = mkexpr (JCPEbinary(expr e1,`Bsub,expr e2)) eloc in + JCPEbinary(sube,binop op,zero_expr) + + | _ -> boolean_node_from_expr (typeOf e) (expr e) + in +- mkexpr enode e.eloc ++ mkexpr enode eloc + + (* Function called instead of plain [expr] when the evaluation result should + * fit in a C integral type. + *) + and integral_expr e = + ++ let eloc = (Location.to_lexing_loc e.eloc) in + let rec int_expr e = + let node_from_boolean_expr e = JCPEif(e,one_expr,zero_expr) in + + let enode = match e.enode with + | UnOp(LNot,e',_ty) -> +- let e = mkexpr (JCPEunary(unop LNot,boolean_expr e')) e.eloc in ++ let e = mkexpr (JCPEunary(unop LNot,boolean_expr e')) eloc in + node_from_boolean_expr e + + | UnOp(op,e',_ty) -> + let e = +- locate (mkexpr (JCPEunary(unop op,expr e')) e.eloc) ++ locate (mkexpr (JCPEunary(unop op,expr e')) eloc) + in + e#node + + | BinOp((LAnd | LOr) as op,e1,e2,_ty) -> + let e = +- mkexpr (JCPEbinary(boolean_expr e1,binop op,boolean_expr e2)) e.eloc ++ mkexpr (JCPEbinary(boolean_expr e1,binop op,boolean_expr e2)) eloc + in + node_from_boolean_expr e + + | BinOp((Lt | Gt | Le | Ge as op),e1,e2,_ty) + when isPointerType (typeOf e1) -> + (* Pointer comparison is translated as subtraction *) +- let sube = mkexpr (JCPEbinary(expr e1,`Bsub,expr e2)) e.eloc in +- let e = mkexpr (JCPEbinary(sube,binop op,zero_expr)) e.eloc in ++ let sube = mkexpr (JCPEbinary(expr e1,`Bsub,expr e2)) eloc in ++ let e = mkexpr (JCPEbinary(sube,binop op,zero_expr)) eloc in + node_from_boolean_expr e + + (* | BinOp((Eq | Ne as op),e1,e2,_ty) *) +@@ -1681,11 +1685,11 @@ and integral_expr e = + (* node_from_boolean_expr e *) + + | BinOp((Eq | Ne) as op,e1,e2,_ty) -> +- let e = mkexpr (JCPEbinary(expr e1,binop op,expr e2)) e.eloc in ++ let e = mkexpr (JCPEbinary(expr e1,binop op,expr e2)) eloc in + node_from_boolean_expr e + + | BinOp((Lt | Gt | Le | Ge) as op,e1,e2,_ty) -> +- let e = mkexpr (JCPEbinary(expr e1,binop op,expr e2)) e.eloc in ++ let e = mkexpr (JCPEbinary(expr e1,binop op,expr e2)) eloc in + node_from_boolean_expr e + + | BinOp(Shiftrt,e1,e2,_ty) -> +@@ -1694,13 +1698,13 @@ and integral_expr e = + Integer.lt i (Integer.of_int 63) -> + (* Right shift by constant is division by constant *) + let pow = constant_expr (Integer.two_power i) in +- locate (mkexpr (JCPEbinary(expr e1,`Bdiv,expr pow)) e.eloc) ++ locate (mkexpr (JCPEbinary(expr e1,`Bdiv,expr pow)) eloc) + | _ -> + let op = + if isSignedInteger (typeOf e1) then `Barith_shift_right + else `Blogical_shift_right + in +- locate (mkexpr (JCPEbinary(expr e1,op,expr e2)) e.eloc) ++ locate (mkexpr (JCPEbinary(expr e1,op,expr e2)) eloc) + in + e#node + +@@ -1710,36 +1714,36 @@ and integral_expr e = + Integer.lt i (Integer.of_int 63) -> + (* Left shift by constant is multiplication by constant *) + let pow = constant_expr (Integer.two_power i) in +- locate (mkexpr (JCPEbinary(expr e1,`Bmul,expr pow)) e.eloc) ++ locate (mkexpr (JCPEbinary(expr e1,`Bmul,expr pow)) eloc) + | _ -> +- locate (mkexpr (JCPEbinary(expr e1,binop op,expr e2)) e.eloc) ++ locate (mkexpr (JCPEbinary(expr e1,binop op,expr e2)) eloc) + in + e#node + + | BinOp(op,e1,e2,_ty) -> + let e = +- locate (mkexpr (JCPEbinary(expr e1,binop op,expr e2)) e.eloc) ++ locate (mkexpr (JCPEbinary(expr e1,binop op,expr e2)) eloc) + in + e#node + + | CastE(ty,e1) when isFloatingType (typeOf e1) -> +- let e1' = locate (mkexpr (JCPEcast(expr e1,ltype Linteger)) e.eloc) in ++ let e1' = locate (mkexpr (JCPEcast(expr e1,ltype Linteger)) eloc) in + if !int_model = IMexact then + e1'#node + else +- let e2' = locate (mkexpr (JCPEcast(e1',ctype ty)) e.eloc) in ++ let e2' = locate (mkexpr (JCPEcast(e1',ctype ty)) eloc) in + e2'#node + + | CastE(ty,e1) when isIntegralType (typeOf e1) -> + if !int_model = IMexact then + (int_expr e1)#node + else +- let e = locate (mkexpr (JCPEcast(int_expr e1,ctype ty)) e.eloc) in ++ let e = locate (mkexpr (JCPEcast(int_expr e1,ctype ty)) eloc) in + e#node + + | _ -> (expr e)#node + in +- mkexpr enode e.eloc ++ mkexpr enode eloc + in + + match e.enode with +@@ -1814,8 +1818,9 @@ let keep_only_declared_nb_of_arguments v + + let instruction = function + | Set(lv,e,pos) -> +- let enode = JCPEassign(lval pos lv,expr e) in +- (locate (mkexpr enode pos))#node ++ let lpos = Location.to_lexing_loc pos in ++ let enode = JCPEassign(lval lpos lv,expr e) in ++ (locate (mkexpr enode lpos))#node + + | Call(None,{enode = Lval(Var v,NoOffset)},eargs,pos) -> + if is_assert_function v then +@@ -1834,9 +1839,10 @@ let instruction = function + v + (List.map expr eargs)) + in +- (locate (mkexpr enode pos))#node ++ (locate (mkexpr enode (Location.to_lexing_loc pos)))#node + + | Call(Some lv,{enode = Lval(Var v,NoOffset)},eargs,pos) -> ++ let lpos = Location.to_lexing_loc pos in + let enode = + if is_malloc_function v || is_realloc_function v then + let lvtyp = pointed_type (typeOfLval lv) in +@@ -1867,7 +1873,7 @@ let instruction = function + let siznode = + JCPEconst(JCCinteger(Integer.to_string allocsiz)) + in +- lvtyp, mkexpr siznode pos ++ lvtyp, mkexpr siznode lpos + | BinOp(Mult,({enode = Const c} as arg),nelem,_ty) + when is_integral_const c -> aux arg nelem + | BinOp(Mult,nelem,({enode = Const c} as arg),_ty) +@@ -1928,24 +1934,24 @@ let instruction = function + (List.map expr eargs)) + in + let lvty = typeOfLval lv in +- let call = locate (mkexpr enode pos) in ++ let call = locate (mkexpr enode lpos) in + let enode = + if Typ.equal lvty (getReturnType v.vtype) + || is_malloc_function v + || is_realloc_function v + || is_calloc_function v + then +- JCPEassign(lval pos lv,call) ++ JCPEassign(lval lpos lv,call) + else + let tmpv = makeTempVar (get_curFundec()) (getReturnType v.vtype) in + let tmplv = Var tmpv, NoOffset in + let cast = + new_exp ~loc:pos (CastE(lvty,new_exp ~loc:pos (Lval tmplv))) + in +- let tmpassign = JCPEassign(lval pos lv,expr cast) in +- JCPElet(None,tmpv.vname,Some call,locate (mkexpr tmpassign pos)) ++ let tmpassign = JCPEassign(lval lpos lv,expr cast) in ++ JCPElet(None,tmpv.vname,Some call,locate (mkexpr tmpassign lpos)) + in +- (locate (mkexpr enode pos))#node ++ (locate (mkexpr enode lpos))#node + + | Call _ -> Common.unsupported ~current:true "function pointers" + +@@ -1976,9 +1982,10 @@ let rec statement s = + in + *) + ++ let lpos = Location.to_lexing_loc pos in + let assert_before, contract = + Annotations.fold_code_annot +- (fun _ ca acc -> code_annot pos acc ca) s ([],None) ++ (fun _ ca acc -> code_annot lpos acc ca) s ([],None) + in + let snode = match s.skind with + | Instr i -> instruction i +@@ -1986,7 +1993,7 @@ let rec statement s = + | Return(Some e,_) -> JCPEreturn(expr e) + + | Return(None,_pos) -> +- JCPEreturn(mkexpr (JCPEconst JCCvoid) pos) ++ JCPEreturn(mkexpr (JCPEconst JCCvoid) lpos) + + | Goto(sref,_pos) -> + (* Pick the first non-case label in the list of labels associated to +@@ -2050,7 +2057,7 @@ let rec statement s = + | case_stmt :: _ as slist -> + let switch_labels = List.filter is_case_label case_stmt.labels in + let labs = List.map switch_label switch_labels in +- let slist = mkexpr (JCPEblock(statement_list slist)) pos in ++ let slist = mkexpr (JCPEblock(statement_list slist)) (Location.to_lexing_loc pos) in + labs, slist + in + let case_list = List.map case (case_blocks bl.bstmts slist) in +@@ -2098,7 +2105,7 @@ let rec statement s = + let inv = + match invs with + | [] -> None +- | _ -> Some (mkconjunct invs pos) ++ | _ -> Some (mkconjunct invs lpos) + in + let ass = assigns ass in + (beh_names,inv,ass)) +@@ -2119,7 +2126,7 @@ let rec statement s = + in + (* Prefix statement by all non-case labels *) + let labels = filter_out is_case_label s.labels in +- let s = mkexpr snode pos in ++ let s = mkexpr snode lpos in + let s = + match contract with + | None -> s +@@ -2145,13 +2152,13 @@ let rec statement s = + in + mkexpr + (JCPEcontract(requires, decreases, behaviors, s)) +- pos ++ lpos + in + let s = match assert_before @ [s] with + | [s] -> s +- | slist -> mkexpr (JCPEblock slist) pos ++ | slist -> mkexpr (JCPEblock slist) lpos + in +- List.fold_left (fun s lab -> mkexpr (JCPElabel(label lab,s)) pos) s labels ++ List.fold_left (fun s lab -> mkexpr (JCPElabel(label lab,s)) lpos) s labels + + and statement_list slist = List.rev (List.rev_map statement slist) + +@@ -2228,7 +2235,7 @@ let rec annotation is_axiomatic annot = + if _attr <> [] then warning "ignoring attributes of axiom %s" name; + ignore + (reg_position ~id:name +- ~name:("Lemma " ^ name) pos); ++ ~name:("Lemma " ^ name) (Location.to_lexing_loc pos)); + begin try + [JCDlemma(name,is_axiom,[],logic_labels labels,pred property)] + with (Unsupported _ | Log.FeatureRequest _) +@@ -2263,6 +2270,7 @@ let rec annotation is_axiomatic annot = + + | Dtype (info,pos) when info.lt_params=[] -> + CurrentLoc.set pos; ++ let lpos = Location.to_lexing_loc pos in + let myself = mktype (JCPTidentifier (info.lt_name,[])) in + let mydecl = JCDlogic_type (info.lt_name,[]) in + let axiomatic ctors = +@@ -2295,8 +2303,8 @@ let rec annotation is_axiomatic annot = + (* TODO: give unique name *) + (fun x -> + mkexpr (JCPEquantifier(Forall,ltype t, +- [new identifier prms_name], [],x)) pos), +- mkexpr (JCPEvar prms_name) pos ++ [new identifier prms_name], [],x)) lpos), ++ mkexpr (JCPEvar prms_name) lpos + in + let (quant,args) = + List.fold_right +@@ -2314,17 +2322,17 @@ let rec annotation is_axiomatic annot = + (mkexpr + (JCPEbinary + (mkexpr (JCPEapp (info.lt_name ^ "_tag",[], +- [mkexpr expr pos])) pos, ++ [mkexpr expr lpos])) lpos, + `Beq, +- mkexpr(JCPEconst(JCCinteger (Int64.to_string i))) pos)) +- pos) ++ mkexpr(JCPEconst(JCCinteger (Int64.to_string i))) lpos)) ++ lpos) + in + (i+one, + JCDlemma(cons.ctor_name ^ "_tag_val",true,[],[], pred) + ::axioms) + in + let (_,axioms) = List.fold_right tag_axiom ctors (zero,[]) in +- let xvar = mkexpr (JCPEvar "x") pos in (* TODO: give unique name *) ++ let xvar = mkexpr (JCPEvar "x") lpos in (* TODO: give unique name *) + let one_case cons = + let prms = ref(-1) in + let param t = +@@ -2333,8 +2341,8 @@ let rec annotation is_axiomatic annot = + (* TODO: give unique name *) + ((fun x -> + mkexpr (JCPEquantifier(Exists,ltype t, +- [new identifier prms_name], [],x)) pos), +- mkexpr (JCPEvar prms_name) pos) ++ [new identifier prms_name], [],x)) lpos), ++ mkexpr (JCPEvar prms_name) lpos) + in let (quant,args) = + List.fold_right + (fun arg (quants,args) -> +@@ -2345,7 +2353,7 @@ let rec annotation is_axiomatic annot = + quant + (mkexpr + (JCPEbinary(xvar,`Beq, +- mkexpr (JCPEapp(cons.ctor_name,[],args)) pos)) pos) ++ mkexpr (JCPEapp(cons.ctor_name,[],args)) lpos)) lpos) + in + match ctors with + [] -> cons +@@ -2354,7 +2362,7 @@ let rec annotation is_axiomatic annot = + [JCDlemma(info.lt_name ^ "_inductive", true, [], [], + (mkexpr (JCPEquantifier + (Forall,myself, +- [new identifier "x"], [],one_case x)) pos))] ++ [new identifier "x"], [],one_case x)) lpos))] + | x::l -> + tag_fun :: cons @ axioms @ + [JCDlemma(info.lt_name ^ "_inductive", true, [], [], +@@ -2365,8 +2373,8 @@ let rec annotation is_axiomatic annot = + List.fold_right + (fun cons case -> + mkexpr (JCPEbinary(case,`Blor, +- one_case cons)) pos) +- l (one_case x))) pos)] ++ one_case cons)) lpos) ++ l (one_case x))) lpos)] + in + (*NB: axioms stating that two values beginning with different + symbols are different are not generated. *) +@@ -2380,7 +2388,7 @@ let rec annotation is_axiomatic annot = + | _ when is_axiomatic -> axiomatic + | _ -> + [JCDaxiomatic (info.lt_name ^ "_axiomatic", +- List.map (fun x -> mkdecl x pos) axiomatic)]) ++ List.map (fun x -> mkdecl x lpos) axiomatic)]) + + | Dtype _ -> unsupported "type definitions" + | Dvolatile _ -> Common.unsupported "volatile variables" +@@ -2395,8 +2403,9 @@ let rec annotation is_axiomatic annot = + Format.eprintf "Translating axiomatic %s into jessie code@." id; + *) + let l = List.fold_left (fun acc d -> (annotation true d)@acc) [] l in +- [JCDaxiomatic(id,List.map (fun d -> mkdecl d pos) ++ [JCDaxiomatic(id,List.map (fun d -> mkdecl d (Location.to_lexing_loc pos)) + (List.rev l))] ++ | Dextended _ -> unsupported "extended global annotation" + + let default_field_modifiers = (false,false) + +@@ -2457,7 +2466,7 @@ let global vardefs g = + ignore(Typ.Hashtbl.find Norm.generated_union_types ty); + [JCDtag(compinfo.cname,[],None,fields,[])] + with Not_found -> +- let id = mkidentifier compinfo.cname pos in ++ let id = mkidentifier compinfo.cname (Location.to_lexing_loc pos) in + [ + JCDtag(compinfo.cname,[],None,fields,[]); + JCDvariant_type(compinfo.cname,[id]) +@@ -2466,9 +2475,10 @@ let global vardefs g = + + | GCompTag(compinfo,pos) -> (* union type *) + assert (not compinfo.cstruct); ++ let lpos = Location.to_lexing_loc pos in + let field fi = + let ty = pointed_type fi.ftype in +- mkidentifier (get_struct_name ty) pos ++ mkidentifier (get_struct_name ty) lpos + in + (* match pointed_type fi.ftype with *) + (* | TComp(compinfo,_) -> *) +@@ -2483,7 +2493,7 @@ let global vardefs g = + (* | _ -> *) + (* assert false *) + (* in *) +- let union_id = mkidentifier compinfo.cname pos in ++ let union_id = mkidentifier compinfo.cname lpos in + let union_size = match compinfo.cfields with + | [] -> 0 + | fi::_ -> +@@ -2558,7 +2568,7 @@ let global vardefs g = + | TFun(rt,_,_,_) -> rt + | _ -> assert false + in +- let id = mkidentifier v.vname pos in ++ let id = mkidentifier v.vname (Location.to_lexing_loc pos) in + let kf = Globals.Functions.get v in + Jessie_options.debug + "Getting spec of %s" (Kernel_function.get_name kf); +@@ -2587,22 +2597,23 @@ let global vardefs g = + if f.svar.vname = name_of_assert + || f.svar.vname = name_of_free then [] + else ++ let lpos = Location.to_lexing_loc pos in + let rty = match unrollType f.svar.vtype with + | TFun(ty,_,_,_) -> ty + | _ -> assert false + in + let formal v = true, ctype v.vtype, v.vname in + let formals = List.map formal f.sformals in +- let id = mkidentifier f.svar.vname f.svar.vdecl in ++ let id = mkidentifier f.svar.vname (Location.to_lexing_loc f.svar.vdecl) in + let funspec = + Annotations.funspec (Globals.Functions.get f.svar) + in + begin try + let local v = +- mkexpr (JCPEdecl(ctype v.vtype,v.vname,None)) v.vdecl ++ mkexpr (JCPEdecl(ctype v.vtype,v.vname,None)) (Location.to_lexing_loc v.vdecl) + in + let locals = List.rev (List.rev_map local f.slocals) in +- let body = mkexpr (JCPEblock(statement_list f.sbody.bstmts)) pos in ++ let body = mkexpr (JCPEblock(statement_list f.sbody.bstmts)) lpos in + let s,cba,dba = spec f.svar.vname funspec in + let body = + List.fold_left +@@ -2630,10 +2641,10 @@ let global vardefs g = + :: acc) + body dba + in +- let body = mkexpr (JCPEblock body) pos in ++ let body = mkexpr (JCPEblock body) lpos in + ignore + (reg_position ~id:f.svar.vname +- ~name:("Function " ^ f.svar.vname) f.svar.vdecl); ++ ~name:("Function " ^ f.svar.vname) (Location.to_lexing_loc f.svar.vdecl)); + [JCDfun(ctype rty,id,formals,s,Some body)] + with (Unsupported _ | Log.FeatureRequest _) + when drop_on_unsupported_feature -> +@@ -2652,7 +2663,7 @@ let global vardefs g = + | GAnnot(la,_) -> annotation false la + + in +- List.map (fun dnode -> mkdecl dnode pos) dnodes ++ List.map (fun dnode -> mkdecl dnode (Location.to_lexing_loc pos)) dnodes + + let integral_type name ty bitsize = + let min = min_value_of_integral_type ~bitsize ty in diff --git a/why.spec b/why.spec index 6113f5d..f546127 100644 --- a/why.spec +++ b/why.spec @@ -7,7 +7,7 @@ Name: why Version: 2.41 -Release: 2%{?dist} +Release: 3%{?dist} Summary: Software verification platform License: LGPLv2 with exceptions @@ -23,6 +23,8 @@ Source7: rem.pvs Source8: patch_jessie_pvs # Created with gimp from official upstream icon Source9: %{name}-icons.tar.xz +# Adapt to Frama-C 18.0 +Patch0: %{name}-frama-c.patch BuildRequires: auto-destdir BuildRequires: desktop-file-utils @@ -108,6 +110,7 @@ based on Why, including various automated and interactive provers. %prep %setup -q %setup -q -T -D -a 9 +%patch0 cp -p %SOURCE2 ./ @@ -140,8 +143,14 @@ sed -ri 's,ocaml(c|opt),& -g,' atp/Makefile # Command "pvs" is LVM2's /sbin/pvs, so rename "pvs" to pvs-sbcl: sed -i 's/pvs/pvs-sbcl/' configure -# Allow building with why3 1.1.1 -sed -i 's,0\.88\.\*,&|1.1.1,' configure +# Allow building with ocaml 4.07 and 4.08 +sed -i 's,4\.06\.\*,&|4.07.*|4.08.*,' configure + +# Allow building with why3 1.2.0 +sed -i 's,0\.88\.\*,&|1.2.0,' configure + +# Allow building with Frama-C 18.0 +sed -i 's,Chlorine-20180501,18.0*,' configure %build %ifarch %{ocaml_native_compiler} @@ -225,6 +234,9 @@ make check %changelog +* Wed Jun 5 2019 Jerry James - 2.41-3 +- Rebuild for coq 8.9.1, why3 1.2.0, and frama-c 18.0 + * Sun Feb 03 2019 Fedora Release Engineering - 2.41-2 - Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild From 01dc32708faa4eb24bf34eca192cbfd4a735cdfe Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sat, 27 Jul 2019 03:27:05 +0000 Subject: [PATCH 11/22] - Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild Signed-off-by: Fedora Release Engineering --- why.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/why.spec b/why.spec index f546127..77408c6 100644 --- a/why.spec +++ b/why.spec @@ -7,7 +7,7 @@ Name: why Version: 2.41 -Release: 3%{?dist} +Release: 4%{?dist} Summary: Software verification platform License: LGPLv2 with exceptions @@ -234,6 +234,9 @@ make check %changelog +* Sat Jul 27 2019 Fedora Release Engineering - 2.41-4 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild + * Wed Jun 5 2019 Jerry James - 2.41-3 - Rebuild for coq 8.9.1, why3 1.2.0, and frama-c 18.0 From 6aa1f91c4be3c8350926df5ab873c3984143499b Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 2 Aug 2019 13:18:07 -0600 Subject: [PATCH 12/22] Rebuild for frama-c 19.0. --- why-frama-c.patch | 58 ++++++++++++++++++++++++++++++++++++++++++++--- why.spec | 9 +++++--- 2 files changed, 61 insertions(+), 6 deletions(-) diff --git a/why-frama-c.patch b/why-frama-c.patch index eab0a6b..a439b78 100644 --- a/why-frama-c.patch +++ b/why-frama-c.patch @@ -1,5 +1,5 @@ --- frama-c-plugin/common.ml.orig 2018-06-28 16:43:25.000000000 -0600 -+++ frama-c-plugin/common.ml 2019-06-03 09:39:40.876316289 -0600 ++++ frama-c-plugin/common.ml 2019-08-02 12:09:33.202030622 -0600 @@ -56,8 +56,9 @@ let fatal fmt = Jessie_options.fatal ~cu let unsupported fmt = @@ -12,6 +12,15 @@ ) ~current:true fmt let warning fmt = Jessie_options.warning ~current:true fmt +@@ -1173,7 +1174,7 @@ let rec force_exp_to_predicate e = + { pred_name = []; pred_loc = e.eloc; pred_content = pnode; } + + let force_exp_to_assertion e = +- Logic_const.new_code_annotation (AAssert([], force_exp_to_predicate e)) ++ Logic_const.new_code_annotation (AAssert([], Assert, force_exp_to_predicate e)) + + + (* Visitor methods for sharing preaction/postaction between exp/term/tsets *) --- frama-c-plugin/common.mli.orig 2018-06-28 16:43:25.000000000 -0600 +++ frama-c-plugin/common.mli 2019-06-03 09:38:56.727035437 -0600 @@ -102,7 +102,7 @@ val term_of_var : Cil_types.varinfo -> C @@ -24,7 +33,7 @@ val mkInfo : Cil_types.exp -> Cil_types.exp --- frama-c-plugin/interp.ml.orig 2018-06-28 16:43:25.000000000 -0600 -+++ frama-c-plugin/interp.ml 2019-06-03 11:55:36.722081449 -0600 ++++ frama-c-plugin/interp.ml 2019-08-02 12:44:32.970899836 -0600 @@ -702,14 +702,14 @@ let rec coerce_floats t = if isLogicFloatType t.term_type then List.map @@ -218,6 +227,15 @@ (* Keep names associated to predicate *) let named_pred p = +@@ -1447,7 +1448,7 @@ let built_behavior_ids = function + let code_annot pos ((acc_assert_before,contract) as acc) a = + let push s = s::acc_assert_before,contract in + match a.annot_content with +- | AAssert (behav,p) -> ++ | AAssert (behav,_,p) -> + let behav = built_behavior_ids behav in + let asrt = Aassert in (* [VP] Needs to retrieve exact status *) + push @@ -1492,14 +1493,15 @@ let set_curFundec, get_curFundec = let rec expr e = @@ -453,7 +471,22 @@ let enode = if is_malloc_function v || is_realloc_function v then let lvtyp = pointed_type (typeOfLval lv) in -@@ -1867,7 +1873,7 @@ let instruction = function +@@ -1849,7 +1855,7 @@ let instruction = function + let arg = stripInfo arg in + let loc = arg.eloc in + let aux arg nelem = +- let factor = Integer.div (value_of_integral_expr arg) lvsiz in ++ let factor = Integer.e_div (value_of_integral_expr arg) lvsiz in + let siz = + if Integer.equal factor Integer.one then expr nelem + else +@@ -1862,12 +1868,12 @@ let instruction = function + let ty,arg = match arg.enode with + | Info _ -> assert false + | Const c when is_integral_const c -> +- let allocsiz = Integer.div (value_of_integral_expr arg) lvsiz ++ let allocsiz = Integer.e_div (value_of_integral_expr arg) lvsiz + in let siznode = JCPEconst(JCCinteger(Integer.to_string allocsiz)) in @@ -462,6 +495,15 @@ | BinOp(Mult,({enode = Const c} as arg),nelem,_ty) when is_integral_const c -> aux arg nelem | BinOp(Mult,nelem,({enode = Const c} as arg),_ty) +@@ -1895,7 +1901,7 @@ let instruction = function + | Const c when is_integral_const c -> + let lvtyp = pointed_type (typeOfLval lv) in + let lvsiz = Integer.of_int64 ((bits_sizeof lvtyp) lsr 3) in +- let factor = Integer.div (value_of_integral_expr arg) lvsiz in ++ let factor = Integer.e_div (value_of_integral_expr arg) lvsiz in + let siz = + if Integer.equal factor Integer.one then + expr nelem @@ -1928,24 +1934,24 @@ let instruction = function (List.map expr eargs)) in @@ -755,3 +797,13 @@ let integral_type name ty bitsize = let min = min_value_of_integral_type ~bitsize ty in +--- frama-c-plugin/norm.ml.orig 2018-06-28 16:43:25.000000000 -0600 ++++ frama-c-plugin/norm.ml 2019-08-02 12:24:56.510573782 -0600 +@@ -471,6 +471,7 @@ object + end; + DoChildren (* FIXME: correct ? *) + | Dcustom_annot _ -> DoChildren (* FIXME: correct ? *) ++ | Dextended _ -> DoChildren (* FIXME: correct ? *) + in annot + + method! vterm_lval tlv = diff --git a/why.spec b/why.spec index 77408c6..4578228 100644 --- a/why.spec +++ b/why.spec @@ -132,7 +132,7 @@ for f in CHANGES COPYING; do done # APRON support: add a missing rpath and adapt to newer versions of apron -sed -e "s|-lpolkaMPQ_caml|-Wl,-rpath,%{_libdir}/ocaml/apron|" \ +sed -e "s|-lpolkaMPQ_caml|-Wl,-rpath,%{_libdir}/ocaml/apron|;s| -lbigarray||" \ -e "s|box\.cmxa polka.cmxa|boxMPQ.cmxa polkaMPQ.cmxa octMPQ.cmxa|" \ -i configure @@ -149,8 +149,8 @@ sed -i 's,4\.06\.\*,&|4.07.*|4.08.*,' configure # Allow building with why3 1.2.0 sed -i 's,0\.88\.\*,&|1.2.0,' configure -# Allow building with Frama-C 18.0 -sed -i 's,Chlorine-20180501,18.0*,' configure +# Allow building with Frama-C 19.0 +sed -i 's,Chlorine-20180501,19.0*,' configure %build %ifarch %{ocaml_native_compiler} @@ -234,6 +234,9 @@ make check %changelog +* Fri Aug 2 2109 Jerry James - 2.41-4 +- Rebuild for frama-c 19.0 + * Sat Jul 27 2019 Fedora Release Engineering - 2.41-4 - Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild From d4041358df010b9a2aa5316a63e7bd98f6398dfc Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 6 Sep 2019 12:02:05 -0600 Subject: [PATCH 13/22] Rebuild for ocaml-zarith 1.9. --- why.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/why.spec b/why.spec index 4578228..0828ad4 100644 --- a/why.spec +++ b/why.spec @@ -7,7 +7,7 @@ Name: why Version: 2.41 -Release: 4%{?dist} +Release: 5%{?dist} Summary: Software verification platform License: LGPLv2 with exceptions @@ -234,6 +234,9 @@ make check %changelog +* Fri Sep 6 2019 Jerry James - 2.41-5 +- Rebuild for ocaml-zarith 1.9 + * Fri Aug 2 2109 Jerry James - 2.41-4 - Rebuild for frama-c 19.0 From d626ea58982d4b8f28202e0402f9a2ac92b73d4f Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 6 Sep 2019 12:04:30 -0600 Subject: [PATCH 14/22] Fix egregious date typo in the changelog. --- why.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/why.spec b/why.spec index 0828ad4..c68a858 100644 --- a/why.spec +++ b/why.spec @@ -237,7 +237,7 @@ make check * Fri Sep 6 2019 Jerry James - 2.41-5 - Rebuild for ocaml-zarith 1.9 -* Fri Aug 2 2109 Jerry James - 2.41-4 +* Fri Aug 2 2019 Jerry James - 2.41-4 - Rebuild for frama-c 19.0 * Sat Jul 27 2019 Fedora Release Engineering - 2.41-4 From 2ff5e9754d2cb45331b413d1842054607e4f65c4 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 23 Sep 2019 09:16:09 -0600 Subject: [PATCH 15/22] Rebuild for frama-c 19.1. --- why.spec | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/why.spec b/why.spec index c68a858..93076ad 100644 --- a/why.spec +++ b/why.spec @@ -7,7 +7,7 @@ Name: why Version: 2.41 -Release: 5%{?dist} +Release: 6%{?dist} Summary: Software verification platform License: LGPLv2 with exceptions @@ -149,8 +149,8 @@ sed -i 's,4\.06\.\*,&|4.07.*|4.08.*,' configure # Allow building with why3 1.2.0 sed -i 's,0\.88\.\*,&|1.2.0,' configure -# Allow building with Frama-C 19.0 -sed -i 's,Chlorine-20180501,19.0*,' configure +# Allow building with Frama-C 19.1 +sed -i 's,Chlorine-20180501,19.1*,' configure %build %ifarch %{ocaml_native_compiler} @@ -234,6 +234,9 @@ make check %changelog +* Mon Sep 23 2019 Jerry James - 2.41-6 +- Rebuild for frama-c 19.1 + * Fri Sep 6 2019 Jerry James - 2.41-5 - Rebuild for ocaml-zarith 1.9 From 81014a5a53d856d492a68bbc01bf9fd7463e3ce0 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 11 Oct 2019 09:02:30 -0600 Subject: [PATCH 16/22] Rebuild for ocaml-mlgmpidl 1.2.11. --- why.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/why.spec b/why.spec index 93076ad..1f62530 100644 --- a/why.spec +++ b/why.spec @@ -7,7 +7,7 @@ Name: why Version: 2.41 -Release: 6%{?dist} +Release: 7%{?dist} Summary: Software verification platform License: LGPLv2 with exceptions @@ -234,6 +234,9 @@ make check %changelog +* Fri Oct 11 2019 Jerry James - 2.41-7 +- Rebuild for ocaml-mlgmpidl 1.2.11 + * Mon Sep 23 2019 Jerry James - 2.41-6 - Rebuild for frama-c 19.1 From ee09cbc0858f858f6a3524d400e161d6a0be5cbc Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 29 Oct 2019 08:25:14 -0600 Subject: [PATCH 17/22] Rebuild for why3 1.2.1. --- why.rpmlintrc | 27 +++++++++++++++++++++++++++ why.spec | 11 +++++++---- 2 files changed, 34 insertions(+), 4 deletions(-) create mode 100644 why.rpmlintrc diff --git a/why.rpmlintrc b/why.rpmlintrc new file mode 100644 index 0000000..d790618 --- /dev/null +++ b/why.rpmlintrc @@ -0,0 +1,27 @@ +# THIS FILE IS FOR WHITELISTING RPMLINT ERRORS AND WARNINGS IN TASKOTRON +# https://fedoraproject.org/wiki/Taskotron/Tasks/dist.rpmlint#Whitelisting_errors + +# The dictionary lacks some technical words +addFilter(r'W: spelling-error .* (frama|provers)') + +# Caused by ocaml; this package cannot fix it +addFilter(r'why[^:]+: E: missing-call-to-chdir-with-chroot') + +# Oh yes, we have no manual page +addFilter(r'W: no-manual-page-for-binary (jessie|krakatoa|patch_jessie_pvs)') + +# Indeed there is no documentation +addFilter(r'why.[^:]+: W: no-documentation') +addFilter(r'why-(jessie|pvs-support).[^:]*: W: no-documentation') + +# This is a devel package +addFilter(r'why-jessie\.[^:]+: W: devel-file-in-non-devel-package') + +# PVS creates, and requires, hidden files +addFilter(r'why-pvs-support\.[^:]+: W: hidden-file-or-dir .*\.pvscontext') + +# This package has no binary bits +addFilter(r'why-pvs-support\.[^:]+: W: only-non-binary-in-usr-lib') + +# The icons were created by the Fedora packager; there is no URL +addFilter(r'why\.spec: W: invalid-url Source[^:]+: why-icons\.tar\.xz') diff --git a/why.spec b/why.spec index 1f62530..8909b82 100644 --- a/why.spec +++ b/why.spec @@ -7,7 +7,7 @@ Name: why Version: 2.41 -Release: 7%{?dist} +Release: 8%{?dist} Summary: Software verification platform License: LGPLv2 with exceptions @@ -146,8 +146,8 @@ sed -i 's/pvs/pvs-sbcl/' configure # Allow building with ocaml 4.07 and 4.08 sed -i 's,4\.06\.\*,&|4.07.*|4.08.*,' configure -# Allow building with why3 1.2.0 -sed -i 's,0\.88\.\*,&|1.2.0,' configure +# Allow building with why3 1.2.1 +sed -i 's,0\.88\.\*,&|1.2.1,' configure # Allow building with Frama-C 19.1 sed -i 's,Chlorine-20180501,19.1*,' configure @@ -194,7 +194,7 @@ sed -i "s|%{buildroot}||" %{buildroot}%{_libdir}/pvs/lib/why/top.out mkdir -p %{buildroot}%{_libdir}/pvs/lib/ints/ cp -p %{SOURCE6} %{SOURCE7} %{buildroot}%{_libdir}/pvs/lib/ints/ -cp -p %{SOURCE8} %{buildroot}%{_bindir}/ +install -m755 -p %{SOURCE8} %{buildroot}%{_bindir}/ %endif %global why_doc_dir %{?_pkgdocdir}%{!?_pkgdocdir:%{_docdir}/%{name}-%{version}} @@ -234,6 +234,9 @@ make check %changelog +* Tue Oct 29 2019 Jerry James - 2.41-8 +- Rebuild for why3 1.2.1 + * Fri Oct 11 2019 Jerry James - 2.41-7 - Rebuild for ocaml-mlgmpidl 1.2.11 From 219f4f021bd7a32e95f794164f3bdca257a5ac7d Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 9 Dec 2019 14:20:20 -0700 Subject: [PATCH 18/22] OCaml 4.09.0 (final) rebuild. --- why.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/why.spec b/why.spec index 8909b82..078efce 100644 --- a/why.spec +++ b/why.spec @@ -7,7 +7,7 @@ Name: why Version: 2.41 -Release: 8%{?dist} +Release: 9%{?dist} Summary: Software verification platform License: LGPLv2 with exceptions @@ -234,6 +234,9 @@ make check %changelog +* Mon Dec 9 2019 Jerry James - 2.41-9 +- OCaml 4.09.0 (final) rebuild. + * Tue Oct 29 2019 Jerry James - 2.41-8 - Rebuild for why3 1.2.1 From a55ef6338d7be2c5ccdab44cfa5b83e9f488a77b Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 23 Jan 2020 16:07:50 -0700 Subject: [PATCH 19/22] Rebuild for apron 0.9.12. --- why.spec | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/why.spec b/why.spec index 078efce..7061f56 100644 --- a/why.spec +++ b/why.spec @@ -7,7 +7,7 @@ Name: why Version: 2.41 -Release: 9%{?dist} +Release: 10%{?dist} Summary: Software verification platform License: LGPLv2 with exceptions @@ -143,8 +143,8 @@ sed -ri 's,ocaml(c|opt),& -g,' atp/Makefile # Command "pvs" is LVM2's /sbin/pvs, so rename "pvs" to pvs-sbcl: sed -i 's/pvs/pvs-sbcl/' configure -# Allow building with ocaml 4.07 and 4.08 -sed -i 's,4\.06\.\*,&|4.07.*|4.08.*,' configure +# Allow building with ocaml 4.07 through 4.10 +sed -i 's,4\.06\.\*,&|4.07.*|4.08.*|4.09.*|4.10.*,' configure # Allow building with why3 1.2.1 sed -i 's,0\.88\.\*,&|1.2.1,' configure @@ -234,6 +234,9 @@ make check %changelog +* Thu Jan 23 2020 Jerry James - 2.41-10 +- Rebuild for apron 0.9.12 + * Mon Dec 9 2019 Jerry James - 2.41-9 - OCaml 4.09.0 (final) rebuild. From 4d6840f78218dcfa5f5a721984cfee7746b611c3 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 23 Jan 2020 21:25:20 -0700 Subject: [PATCH 20/22] Fix building with OCaml 4.10. --- why.spec | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/why.spec b/why.spec index 7061f56..4110d51 100644 --- a/why.spec +++ b/why.spec @@ -143,8 +143,9 @@ sed -ri 's,ocaml(c|opt),& -g,' atp/Makefile # Command "pvs" is LVM2's /sbin/pvs, so rename "pvs" to pvs-sbcl: sed -i 's/pvs/pvs-sbcl/' configure -# Allow building with ocaml 4.07 through 4.10 -sed -i 's,4\.06\.\*,&|4.07.*|4.08.*|4.09.*|4.10.*,' configure +# Allow building with ocaml 4.07 and up +sed -i 's,4\.06\.\*,&|4.07.*|4.08.*|4.09.*|4.1*,' configure +sed -i 's,4\.0\*,4.*,' Makefile.in # Allow building with why3 1.2.1 sed -i 's,0\.88\.\*,&|1.2.1,' configure From 4ea920bebe1b2b1a1b50a8c499579350f4c47bd1 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Fri, 31 Jan 2020 03:41:17 +0000 Subject: [PATCH 21/22] - Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild Signed-off-by: Fedora Release Engineering --- why.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/why.spec b/why.spec index 4110d51..5aa375a 100644 --- a/why.spec +++ b/why.spec @@ -7,7 +7,7 @@ Name: why Version: 2.41 -Release: 10%{?dist} +Release: 11%{?dist} Summary: Software verification platform License: LGPLv2 with exceptions @@ -235,6 +235,9 @@ make check %changelog +* Fri Jan 31 2020 Fedora Release Engineering - 2.41-11 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild + * Thu Jan 23 2020 Jerry James - 2.41-10 - Rebuild for apron 0.9.12 From a8d84c45d49b59c72c1e0161fbb63397ffb01629 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 30 Mar 2020 08:51:13 -0600 Subject: [PATCH 22/22] Abandoned by upstream and fails to build from source --- .gitignore | 3 - README.why | 8 - README.why-coq.Fedora | 6 - dead.package | 1 + div.pvs | 35 -- jessie.appdata.xml | 43 --- jessie.desktop | 7 - patch_jessie_pvs | 59 --- rem.pvs | 35 -- sources | 3 - why-frama-c.patch | 809 ------------------------------------------ why.rpmlintrc | 27 -- why.spec | 634 --------------------------------- 13 files changed, 1 insertion(+), 1669 deletions(-) delete mode 100644 .gitignore delete mode 100644 README.why delete mode 100644 README.why-coq.Fedora create mode 100644 dead.package delete mode 100644 div.pvs delete mode 100644 jessie.appdata.xml delete mode 100644 jessie.desktop delete mode 100755 patch_jessie_pvs delete mode 100644 rem.pvs delete mode 100644 sources delete mode 100644 why-frama-c.patch delete mode 100644 why.rpmlintrc delete mode 100644 why.spec diff --git a/.gitignore b/.gitignore deleted file mode 100644 index 81c4283..0000000 --- a/.gitignore +++ /dev/null @@ -1,3 +0,0 @@ -/krakatoa.pdf -/why-icons.tar.xz -/why-*.tar.gz diff --git a/README.why b/README.why deleted file mode 100644 index ba95dfa..0000000 --- a/README.why +++ /dev/null @@ -1,8 +0,0 @@ -Fedora why package: - -Contains the main why executable and supporting tools. - -Consider visiting the main Why site - http://why.lri.fr - for more -documentation. Also, there is more information about the tools -Caduceus and Krakatoa at http://caduceus.lri.fr and -http://krakatoa.lri.fr respectively. \ No newline at end of file diff --git a/README.why-coq.Fedora b/README.why-coq.Fedora deleted file mode 100644 index 406a7a9..0000000 --- a/README.why-coq.Fedora +++ /dev/null @@ -1,6 +0,0 @@ -Fedora why-coq package: - -Contains libraries for interfacing why with Coq. - -You shouldn't have to do anything extra - you should now just be able -to use the Coq-related capabilities of Why. \ No newline at end of file diff --git a/dead.package b/dead.package new file mode 100644 index 0000000..497866a --- /dev/null +++ b/dead.package @@ -0,0 +1 @@ +Abandoned by upstream and fails to build from source diff --git a/div.pvs b/div.pvs deleted file mode 100644 index 4005fe3..0000000 --- a/div.pvs +++ /dev/null @@ -1,35 +0,0 @@ -% Copyright (c) 2010 Jerry James. -% -% Permission is hereby granted, free of charge, to any person obtaining a copy -% of this software and associated documentation files (the "Software"), to deal -% in the Software without restriction, including without limitation the rights -% to use, copy, modify, merge, publish, distribute, sublicense, and/or sell -% copies of the Software, and to permit persons to whom the Software is -% furnished to do so, subject to the following conditions: -% -% The above copyright notice and this permission notice shall be included in -% all copies or substantial portions of the Software. -% -% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR -% IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, -% FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE -% AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER -% LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, -% OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN -% THE SOFTWARE. - -div: THEORY -BEGIN - - x : VAR int - nzy : VAR nzint - - div(x, nzy): int = - IF (x >= 0 AND nzy > 0) THEN ndiv(x, nzy) - ELSIF (x >= 0 AND nzy < 0) THEN -ndiv(x, -nzy) - ELSIF (x < 0 AND nzy > 0) THEN -ndiv(-x, nzy) - ELSE ndiv(-x, -nzy) - ENDIF - -END div - diff --git a/jessie.appdata.xml b/jessie.appdata.xml deleted file mode 100644 index 3cbd299..0000000 --- a/jessie.appdata.xml +++ /dev/null @@ -1,43 +0,0 @@ - - - jessie.desktop - CC0-1.0 - LGPL-2.1 - jessie - Interface between why and Frama-C - -

- Jessie is an interface between why and Frama-C. -

-

- Why is a software verification platform that applies formal proving tools to - annotated programs. The Jessie plugin provide the ability to analyze C - programs by invoking Frama-C. -

- - - - http://krakatoa.lri.fr/jessie/max_why3ide.png - - - - http://krakatoa.lri.fr/jessie/max_ptr_why3ide.png - - - - http://krakatoa.lri.fr/jessie/binary_search_raw.png - - - - http://krakatoa.lri.fr/jessie/binary_search_ovfl.png - - - - http://krakatoa.lri.fr/jessie/binary_search_behav.png - - - - loganjerry@gmail.com - http://krakatoa.lri.fr/ - https://gforge.inria.fr/tracker/?atid=4012&group_id=999&func=browse - diff --git a/jessie.desktop b/jessie.desktop deleted file mode 100644 index 099b3ad..0000000 --- a/jessie.desktop +++ /dev/null @@ -1,7 +0,0 @@ -[Desktop Entry] -Name=jessie -Comment=Verify C program using Jessie plug-in -Exec=frama-c -jessie %F -Icon=why -Type=Application -Categories=Development; diff --git a/patch_jessie_pvs b/patch_jessie_pvs deleted file mode 100755 index 3e4abca..0000000 --- a/patch_jessie_pvs +++ /dev/null @@ -1,59 +0,0 @@ -#!/bin/sh - -# To use PVS with frama-c without the NASA Langley PVS library: -# frama-c -jessie -jessie-atp pvs FILE.c # Generates PVS files -# cd FILE.jessie/pvs -# patch_jessie_pvs # Patch jessie_why.pvs to not need NASA Langley library. -# You can then run PVS to prove the generated theorems with: -# pvs-sbcl FILE_why.pvs -# -# Copyright (c) 2010 David A. Wheeler -# -# Permission is hereby granted, free of charge, to any person obtaining a copy -# of this software and associated documentation files (the "Software"), to deal -# in the Software without restriction, including without limitation the rights -# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell -# copies of the Software, and to permit persons to whom the Software is -# furnished to do so, subject to the following conditions: -# -# The above copyright notice and this permission notice shall be included in -# all copies or substantial portions of the Software. -# -# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR -# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, -# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE -# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER -# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, -# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN -# THE SOFTWARE. - - -if [ ! -f jessie_why.pvs ] ; then - echo "Did not find file jessie_why.pvs in current directory" - exit 1 -fi - -patch -p0 -N << END_OF_PATCH ---- jessie_why.pvs.ORIGINAL 2010-10-05 14:41:58.965970651 -0400 -+++ jessie_why.pvs 2010-10-06 14:28:39.250971269 -0400 -@@ -169,14 +169,14 @@ - (FORALL (x: real): (FORALL (y: real): min(x, y) = x OR min(x, y) = y)) - - %% Why axiom sqrt_pos -- sqrt_pos: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES sqrt(x) >= 0.0)) -+ % sqrt_pos: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES sqrt(x) >= 0.0)) - - %% Why axiom sqrt_sqr -- sqrt_sqr: AXIOM -- (FORALL (x: real): (x >= 0.0 IMPLIES sqr_real(sqrt(x)) = x)) -+ % sqrt_sqr: AXIOM -+ % (FORALL (x: real): (x >= 0.0 IMPLIES sqr_real(sqrt(x)) = x)) - - %% Why axiom sqr_sqrt -- sqr_sqrt: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES sqrt(x * x) = x)) -+ % sqr_sqrt: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES sqrt(x * x) = x)) - - %% Why axiom abs_real_pos - abs_real_pos: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES abs(x) = x)) -END_OF_PATCH - diff --git a/rem.pvs b/rem.pvs deleted file mode 100644 index 4f126a6..0000000 --- a/rem.pvs +++ /dev/null @@ -1,35 +0,0 @@ -% Copyright (c) 2010 Jerry James. -% -% Permission is hereby granted, free of charge, to any person obtaining a copy -% of this software and associated documentation files (the "Software"), to deal -% in the Software without restriction, including without limitation the rights -% to use, copy, modify, merge, publish, distribute, sublicense, and/or sell -% copies of the Software, and to permit persons to whom the Software is -% furnished to do so, subject to the following conditions: -% -% The above copyright notice and this permission notice shall be included in -% all copies or substantial portions of the Software. -% -% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR -% IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, -% FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE -% AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER -% LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, -% OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN -% THE SOFTWARE. - -rem: THEORY -BEGIN - - x : VAR int - nzy : VAR nzint - - rem(x, nzy): int = - IF (x >= 0 AND nzy > 0) THEN rem(nzy)(x) - ELSIF (x >= 0 AND nzy < 0) THEN rem(-nzy)(x) - ELSIF (x < 0 AND nzy > 0) THEN -rem(nzy)(-x) - ELSE -rem(-nzy)(-x) - ENDIF - -END rem - diff --git a/sources b/sources deleted file mode 100644 index aeca842..0000000 --- a/sources +++ /dev/null @@ -1,3 +0,0 @@ -SHA512 (krakatoa.pdf) = 5d0f4e6b938ddc1eafa48264c02cf99e68f776a7e190b997e35fb2cd154627b5d27369886f570cbcfdfe5f3a1929a97a1fec9457a6f6662f83cbb2e51f65ca04 -SHA512 (why-2.41.tar.gz) = 2e31ed2642a29ecbbc05954f2aa5c841befa68959f571bcde134a56639cec49a51351e5c7781a1a50fc531f2111b5649c710fa3e60c0f71f222b192d8c41cc86 -SHA512 (why-icons.tar.xz) = d6ca78cf09540f5742564912470fb8c49f7d11ca16cd8bb60c8790af10c1591198f6020bd792cff8e3464f762b7ef0a690d3e4ba1a2cf670c286c8056d266bc3 diff --git a/why-frama-c.patch b/why-frama-c.patch deleted file mode 100644 index a439b78..0000000 --- a/why-frama-c.patch +++ /dev/null @@ -1,809 +0,0 @@ ---- frama-c-plugin/common.ml.orig 2018-06-28 16:43:25.000000000 -0600 -+++ frama-c-plugin/common.ml 2019-08-02 12:09:33.202030622 -0600 -@@ -56,8 +56,9 @@ let fatal fmt = Jessie_options.fatal ~cu - - let unsupported fmt = - Jessie_options.with_failure -- (fun evt -> -- raise (Unsupported evt.Log.evt_message) -+ (function -+ | (Some evt) -> raise (Unsupported evt.Log.evt_message) -+ | None -> raise (Unsupported "No message") - ) ~current:true fmt - - let warning fmt = Jessie_options.warning ~current:true fmt -@@ -1173,7 +1174,7 @@ let rec force_exp_to_predicate e = - { pred_name = []; pred_loc = e.eloc; pred_content = pnode; } - - let force_exp_to_assertion e = -- Logic_const.new_code_annotation (AAssert([], force_exp_to_predicate e)) -+ Logic_const.new_code_annotation (AAssert([], Assert, force_exp_to_predicate e)) - - - (* Visitor methods for sharing preaction/postaction between exp/term/tsets *) ---- frama-c-plugin/common.mli.orig 2018-06-28 16:43:25.000000000 -0600 -+++ frama-c-plugin/common.mli 2019-06-03 09:38:56.727035437 -0600 -@@ -102,7 +102,7 @@ val term_of_var : Cil_types.varinfo -> C - val mkterm : - Cil_types.term_node -> - Cil_types.logic_type -> -- Lexing.position * Lexing.position -> Cil_types.term -+ Filepath.position * Filepath.position -> Cil_types.term - - val mkInfo : Cil_types.exp -> Cil_types.exp - ---- frama-c-plugin/interp.ml.orig 2018-06-28 16:43:25.000000000 -0600 -+++ frama-c-plugin/interp.ml 2019-08-02 12:44:32.970899836 -0600 -@@ -702,14 +702,14 @@ let rec coerce_floats t = - if isLogicFloatType t.term_type then - List.map - (fun e -> -- mkexpr (JCPEcast(e, mktype (JCPTnative Treal))) t.term_loc) -+ mkexpr (JCPEcast(e, mktype (JCPTnative Treal))) (Location.to_lexing_loc t.term_loc)) - (terms t) - else terms t - - and terms t = - CurrentLoc.set t.term_loc; - let enode = match constFoldTermNodeAtTop t.term_node with -- | TConst c -> [logic_const t.term_loc c] -+ | TConst c -> [logic_const (Location.to_lexing_loc t.term_loc) c] - - | TDataCons({ctor_type = {lt_name = name} } as d,_args) - when name = Utf8_logic.boolean -> -@@ -727,7 +727,7 @@ and terms t = - | Toffset _ -> Common.unsupported "logic offset" - - | TLval lv -> -- List.map (fun x -> x#node) (terms_lval t.term_loc lv) -+ List.map (fun x -> x#node) (terms_lval (Location.to_lexing_loc t.term_loc) lv) - - | TSizeOf _ | TSizeOfE _ | TSizeOfStr _ | TAlignOf _ | TAlignOfE _ -> - assert false (* Should be removed by constant folding *) -@@ -741,7 +741,7 @@ and terms t = - let t1 = terms t1 in - let t2 = terms t2 in - let expr x y = -- let sube = mkexpr (JCPEbinary(x,`Bsub,y)) t.term_loc in -+ let sube = mkexpr (JCPEbinary(x,`Bsub,y)) (Location.to_lexing_loc t.term_loc) in - JCPEbinary(sube,binop op,zero_expr) - in product expr t1 t2 - -@@ -867,7 +867,7 @@ and terms t = - | TAddrOf _tlv -> assert false (* Should have been rewritten *) - - | TStartOf tlv -> -- List.map (fun x -> x#node) (terms_lval t.term_loc tlv) -+ List.map (fun x -> x#node) (terms_lval (Location.to_lexing_loc t.term_loc) tlv) - - | Tapp(linfo,labels,tlist) -> - begin -@@ -887,7 +887,7 @@ and terms t = - then - List.map - (fun t' -> -- mkexpr (JCPEcast(t', mktype (JCPTnative Treal))) t.term_loc) -+ mkexpr (JCPEcast(t', mktype (JCPTnative Treal))) (Location.to_lexing_loc t.term_loc)) - t' - else t') - prof -@@ -950,17 +950,17 @@ and terms t = - | TLogic_coerce(_,t) -> List.map (fun x -> x#node) (terms t) - - in -- List.map (swap mkexpr t.term_loc) enode -+ List.map (swap mkexpr (Location.to_lexing_loc t.term_loc)) enode - - and tag t = - let tag_node = match t.term_node with - | Ttypeof t -> JCPTtypeof (term t) - | Ttype ty -> -- let id = mkidentifier (get_struct_name (pointed_type ty)) t.term_loc in -+ let id = mkidentifier (get_struct_name (pointed_type ty)) (Location.to_lexing_loc t.term_loc) in - JCPTtag id - | _ -> assert false (* Not a tag *) - in -- mktag tag_node t.term_loc -+ mktag tag_node (Location.to_lexing_loc t.term_loc) - - and terms_lval pos lv = - match lv with -@@ -1042,6 +1042,7 @@ and term t = - *) - and pred p = - CurrentLoc.set p.pred_loc; -+ let ploc = Location.to_lexing_loc p.pred_loc in - let enode = match p.pred_content with - | Pfalse -> JCPEconst(JCCboolean false) - -@@ -1060,7 +1061,7 @@ and pred p = - let t' = term t in - if isLogicFloatType t.term_type && isLogicRealType lv.lv_type - then -- mkexpr (JCPEcast(t', mktype (JCPTnative Treal))) t.term_loc -+ mkexpr (JCPEcast(t', mktype (JCPTnative Treal))) (Location.to_lexing_loc t.term_loc) - else t') - pinfo.l_profile - tl -@@ -1072,7 +1073,7 @@ and pred p = - | Prel((Rlt | Rgt | Rle | Rge as rel),t1,t2) - when app_term_type isPointerType false t1.term_type -> - (* Pointer comparison is translated as subtraction *) -- let sube = mkexpr (JCPEbinary(term t1,`Bsub,term t2)) p.pred_loc in -+ let sube = mkexpr (JCPEbinary(term t1,`Bsub,term t2)) ploc in - JCPEbinary(sube,relation rel,zero_expr) - - (* | Prel((Req | Rneq as rel),t1,t2) *) -@@ -1087,14 +1088,14 @@ and pred p = - JCPEeqtype(tag t1,tag t2) - - | Prel(Rneq,t1,t2) when isTypeTagType t1.term_type -> -- let eq = mkexpr (JCPEeqtype(tag t1,tag t2)) p.pred_loc in -+ let eq = mkexpr (JCPEeqtype(tag t1,tag t2)) ploc in - JCPEunary(`Unot,eq) - - | Prel(rel,t1,t2) -> - let res = -- product (fun t1 t2 -> mkexpr (JCPEbinary(t1,relation rel,t2)) p.pred_loc) -+ product (fun t1 t2 -> mkexpr (JCPEbinary(t1,relation rel,t2)) ploc) - (coerce_floats t1) (coerce_floats t2) -- in (mkconjunct res p.pred_loc)#node -+ in (mkconjunct res ploc)#node - | Pand(p1,p2) -> - JCPEbinary(pred p1,`Bland,pred p2) - -@@ -1170,21 +1171,21 @@ and pred p = - | None,None -> true_expr - | Some t2,None -> - let e2 = term t2 in -- let eoffmin = mkexpr (JCPEoffset(Offset_min,e1)) p.pred_loc in -- mkexpr (JCPEbinary(eoffmin,`Ble,e2)) p.pred_loc -+ let eoffmin = mkexpr (JCPEoffset(Offset_min,e1)) ploc in -+ mkexpr (JCPEbinary(eoffmin,`Ble,e2)) ploc - | None, Some t3 -> - let e3 = term t3 in -- let eoffmax = mkexpr (JCPEoffset(Offset_max,e1)) p.pred_loc in -- mkexpr (JCPEbinary(eoffmax,`Bge,e3)) p.pred_loc -+ let eoffmax = mkexpr (JCPEoffset(Offset_max,e1)) ploc in -+ mkexpr (JCPEbinary(eoffmax,`Bge,e3)) ploc - | Some t2,Some t3 -> - let e2 = term t2 in - let e3 = term t3 in -- let eoffmin = mkexpr (JCPEoffset(Offset_min,e1)) p.pred_loc in -- let emin = mkexpr (JCPEbinary(eoffmin,`Ble,e2)) p.pred_loc in -- let eoffmax = mkexpr (JCPEoffset(Offset_max,e1)) p.pred_loc in -- let emax = mkexpr (JCPEbinary(eoffmax,`Bge,e3)) p.pred_loc in -- mkconjunct [emin; emax] p.pred_loc -- in (mkconjunct (List.map mk_one_pred e1) p.pred_loc)#node -+ let eoffmin = mkexpr (JCPEoffset(Offset_min,e1)) ploc in -+ let emin = mkexpr (JCPEbinary(eoffmin,`Ble,e2)) ploc in -+ let eoffmax = mkexpr (JCPEoffset(Offset_max,e1)) ploc in -+ let emax = mkexpr (JCPEbinary(eoffmax,`Bge,e3)) ploc in -+ mkconjunct [emin; emax] ploc -+ in (mkconjunct (List.map mk_one_pred e1) ploc)#node - - | Pvalid(_lab,{ term_node = TBinOp(PlusPI,t1,t2)}) -> - let e1 = terms t1 in -@@ -1193,23 +1194,23 @@ and pred p = - (List.flatten - (List.map - (fun e1 -> -- let eoffmin = mkexpr (JCPEoffset(Offset_min,e1)) p.pred_loc in -- let emin = mkexpr (JCPEbinary(eoffmin,`Ble,e2)) p.pred_loc in -- let eoffmax = mkexpr (JCPEoffset(Offset_max,e1)) p.pred_loc in -- let emax = mkexpr (JCPEbinary(eoffmax,`Bge,e2)) p.pred_loc in -+ let eoffmin = mkexpr (JCPEoffset(Offset_min,e1)) ploc in -+ let emin = mkexpr (JCPEbinary(eoffmin,`Ble,e2)) ploc in -+ let eoffmax = mkexpr (JCPEoffset(Offset_max,e1)) ploc in -+ let emax = mkexpr (JCPEbinary(eoffmax,`Bge,e2)) ploc in - [emin; emax]) -- e1)) p.pred_loc)#node -+ e1)) ploc)#node - | Pvalid (_lab,t) -> - let elist = - List.flatten (List.map (fun e -> -- let eoffmin = mkexpr (JCPEoffset(Offset_min,e)) p.pred_loc in -- let emin = mkexpr (JCPEbinary(eoffmin,`Ble,zero_expr)) p.pred_loc in -- let eoffmax = mkexpr (JCPEoffset(Offset_max,e)) p.pred_loc in -- let emax = mkexpr (JCPEbinary(eoffmax,`Bge,zero_expr)) p.pred_loc in -+ let eoffmin = mkexpr (JCPEoffset(Offset_min,e)) ploc in -+ let emin = mkexpr (JCPEbinary(eoffmin,`Ble,zero_expr)) ploc in -+ let eoffmax = mkexpr (JCPEoffset(Offset_max,e)) ploc in -+ let emax = mkexpr (JCPEbinary(eoffmax,`Bge,zero_expr)) ploc in - [emin; emax] - ) (terms t)) - in -- (mkconjunct elist p.pred_loc)#node -+ (mkconjunct elist ploc)#node - - | Pvalid_read _ -> Common.unsupported "\\valid_read operator" - -@@ -1236,7 +1237,7 @@ and pred p = - | Pvalid_function _ -> Common.unsupported "\\valid_function" - - in -- mkexpr enode p.pred_loc -+ mkexpr enode ploc - - (* Keep names associated to predicate *) - let named_pred p = -@@ -1447,7 +1448,7 @@ let built_behavior_ids = function - let code_annot pos ((acc_assert_before,contract) as acc) a = - let push s = s::acc_assert_before,contract in - match a.annot_content with -- | AAssert (behav,p) -> -+ | AAssert (behav,_,p) -> - let behav = built_behavior_ids behav in - let asrt = Aassert in (* [VP] Needs to retrieve exact status *) - push -@@ -1492,14 +1493,15 @@ let set_curFundec, get_curFundec = - - let rec expr e = - -+ let eloc = Location.to_lexing_loc e.eloc in - let enode = - let e = stripInfo e in - match e.enode with - | Info _ -> assert false - -- | Const c -> const e.eloc c -+ | Const c -> const eloc c - -- | Lval lv -> (lval e.eloc lv)#node -+ | Lval lv -> (lval eloc lv)#node - - | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ -> - assert false (* Should be removed by constant folding *) -@@ -1509,7 +1511,7 @@ let rec expr e = - - | UnOp(op,e,_ty) -> - let e = -- locate (mkexpr (JCPEunary(unop op,expr e)) e.eloc) -+ locate (mkexpr (JCPEunary(unop op,expr e)) eloc) - in - e#node - -@@ -1518,24 +1520,24 @@ let rec expr e = - - | BinOp(op,e1,e2,_ty) -> - let e = -- locate (mkexpr (JCPEbinary(expr e1,binop op,expr e2)) e.eloc) -+ locate (mkexpr (JCPEbinary(expr e1,binop op,expr e2)) eloc) - in - e#node - - | CastE(ty,e') - when isIntegralType ty && isFloatingType (typeOf e') -> - let e1 = -- locate (mkexpr (JCPEcast(expr e',mktype (JCPTnative Treal))) e.eloc) -+ locate (mkexpr (JCPEcast(expr e',mktype (JCPTnative Treal))) eloc) - in - let e = -- locate (mkexpr (JCPEapp("\\truncate_real_to_int",[],[e1])) e.eloc) -+ locate (mkexpr (JCPEapp("\\truncate_real_to_int",[],[e1])) eloc) - in e#node - - | CastE(ty,e') when isIntegralType ty && isArithmeticType (typeOf e') -> - (integral_expr e)#node - - | CastE(ty,e') when isFloatingType ty && isArithmeticType (typeOf e') -> -- let e = locate (mkexpr (JCPEcast(expr e',ctype ty)) e.eloc) in -+ let e = locate (mkexpr (JCPEcast(expr e',ctype ty)) eloc) in - e#node - - | CastE(ty,e') when isIntegralType ty && isPointerType (typeOf e') -> -@@ -1572,7 +1574,7 @@ let rec expr e = - (* else *) - (* bitwise cast *) - let enode = JCPEcast(expr e,ctype ptrty) in -- let e = locate (mkexpr enode e.eloc) in -+ let e = locate (mkexpr enode eloc) in - e#node - (* let _,ptr_to_ptr = type_conversion ptrty ety in *) - (* JCPEapp(ptr_to_ptr,[],[expr e]) *) -@@ -1600,9 +1602,9 @@ let rec expr e = - - | AddrOf _lv -> assert false (* Should have been rewritten *) - -- | StartOf lv -> (lval e.eloc lv)#node -+ | StartOf lv -> (lval eloc lv)#node - in -- mkexpr enode e.eloc -+ mkexpr enode eloc - - (* Function called when expecting a boolean in Jessie, i.e. when translating - a test or a sub-expression of an "or" or "and". -@@ -1614,6 +1616,7 @@ and boolean_expr e = - else assert false - in - -+ let eloc = Location.to_lexing_loc e.eloc in - let enode = match (stripInfo e).enode with - | Info _ -> assert false - -@@ -1633,43 +1636,44 @@ and boolean_expr e = - JCPEbinary(expr e1,binop op,expr e2) - else - (* Pointer comparison is translated as subtraction *) -- let sube = mkexpr (JCPEbinary(expr e1,`Bsub,expr e2)) e.eloc in -+ let sube = mkexpr (JCPEbinary(expr e1,`Bsub,expr e2)) eloc in - JCPEbinary(sube,binop op,zero_expr) - - | _ -> boolean_node_from_expr (typeOf e) (expr e) - in -- mkexpr enode e.eloc -+ mkexpr enode eloc - - (* Function called instead of plain [expr] when the evaluation result should - * fit in a C integral type. - *) - and integral_expr e = - -+ let eloc = (Location.to_lexing_loc e.eloc) in - let rec int_expr e = - let node_from_boolean_expr e = JCPEif(e,one_expr,zero_expr) in - - let enode = match e.enode with - | UnOp(LNot,e',_ty) -> -- let e = mkexpr (JCPEunary(unop LNot,boolean_expr e')) e.eloc in -+ let e = mkexpr (JCPEunary(unop LNot,boolean_expr e')) eloc in - node_from_boolean_expr e - - | UnOp(op,e',_ty) -> - let e = -- locate (mkexpr (JCPEunary(unop op,expr e')) e.eloc) -+ locate (mkexpr (JCPEunary(unop op,expr e')) eloc) - in - e#node - - | BinOp((LAnd | LOr) as op,e1,e2,_ty) -> - let e = -- mkexpr (JCPEbinary(boolean_expr e1,binop op,boolean_expr e2)) e.eloc -+ mkexpr (JCPEbinary(boolean_expr e1,binop op,boolean_expr e2)) eloc - in - node_from_boolean_expr e - - | BinOp((Lt | Gt | Le | Ge as op),e1,e2,_ty) - when isPointerType (typeOf e1) -> - (* Pointer comparison is translated as subtraction *) -- let sube = mkexpr (JCPEbinary(expr e1,`Bsub,expr e2)) e.eloc in -- let e = mkexpr (JCPEbinary(sube,binop op,zero_expr)) e.eloc in -+ let sube = mkexpr (JCPEbinary(expr e1,`Bsub,expr e2)) eloc in -+ let e = mkexpr (JCPEbinary(sube,binop op,zero_expr)) eloc in - node_from_boolean_expr e - - (* | BinOp((Eq | Ne as op),e1,e2,_ty) *) -@@ -1681,11 +1685,11 @@ and integral_expr e = - (* node_from_boolean_expr e *) - - | BinOp((Eq | Ne) as op,e1,e2,_ty) -> -- let e = mkexpr (JCPEbinary(expr e1,binop op,expr e2)) e.eloc in -+ let e = mkexpr (JCPEbinary(expr e1,binop op,expr e2)) eloc in - node_from_boolean_expr e - - | BinOp((Lt | Gt | Le | Ge) as op,e1,e2,_ty) -> -- let e = mkexpr (JCPEbinary(expr e1,binop op,expr e2)) e.eloc in -+ let e = mkexpr (JCPEbinary(expr e1,binop op,expr e2)) eloc in - node_from_boolean_expr e - - | BinOp(Shiftrt,e1,e2,_ty) -> -@@ -1694,13 +1698,13 @@ and integral_expr e = - Integer.lt i (Integer.of_int 63) -> - (* Right shift by constant is division by constant *) - let pow = constant_expr (Integer.two_power i) in -- locate (mkexpr (JCPEbinary(expr e1,`Bdiv,expr pow)) e.eloc) -+ locate (mkexpr (JCPEbinary(expr e1,`Bdiv,expr pow)) eloc) - | _ -> - let op = - if isSignedInteger (typeOf e1) then `Barith_shift_right - else `Blogical_shift_right - in -- locate (mkexpr (JCPEbinary(expr e1,op,expr e2)) e.eloc) -+ locate (mkexpr (JCPEbinary(expr e1,op,expr e2)) eloc) - in - e#node - -@@ -1710,36 +1714,36 @@ and integral_expr e = - Integer.lt i (Integer.of_int 63) -> - (* Left shift by constant is multiplication by constant *) - let pow = constant_expr (Integer.two_power i) in -- locate (mkexpr (JCPEbinary(expr e1,`Bmul,expr pow)) e.eloc) -+ locate (mkexpr (JCPEbinary(expr e1,`Bmul,expr pow)) eloc) - | _ -> -- locate (mkexpr (JCPEbinary(expr e1,binop op,expr e2)) e.eloc) -+ locate (mkexpr (JCPEbinary(expr e1,binop op,expr e2)) eloc) - in - e#node - - | BinOp(op,e1,e2,_ty) -> - let e = -- locate (mkexpr (JCPEbinary(expr e1,binop op,expr e2)) e.eloc) -+ locate (mkexpr (JCPEbinary(expr e1,binop op,expr e2)) eloc) - in - e#node - - | CastE(ty,e1) when isFloatingType (typeOf e1) -> -- let e1' = locate (mkexpr (JCPEcast(expr e1,ltype Linteger)) e.eloc) in -+ let e1' = locate (mkexpr (JCPEcast(expr e1,ltype Linteger)) eloc) in - if !int_model = IMexact then - e1'#node - else -- let e2' = locate (mkexpr (JCPEcast(e1',ctype ty)) e.eloc) in -+ let e2' = locate (mkexpr (JCPEcast(e1',ctype ty)) eloc) in - e2'#node - - | CastE(ty,e1) when isIntegralType (typeOf e1) -> - if !int_model = IMexact then - (int_expr e1)#node - else -- let e = locate (mkexpr (JCPEcast(int_expr e1,ctype ty)) e.eloc) in -+ let e = locate (mkexpr (JCPEcast(int_expr e1,ctype ty)) eloc) in - e#node - - | _ -> (expr e)#node - in -- mkexpr enode e.eloc -+ mkexpr enode eloc - in - - match e.enode with -@@ -1814,8 +1818,9 @@ let keep_only_declared_nb_of_arguments v - - let instruction = function - | Set(lv,e,pos) -> -- let enode = JCPEassign(lval pos lv,expr e) in -- (locate (mkexpr enode pos))#node -+ let lpos = Location.to_lexing_loc pos in -+ let enode = JCPEassign(lval lpos lv,expr e) in -+ (locate (mkexpr enode lpos))#node - - | Call(None,{enode = Lval(Var v,NoOffset)},eargs,pos) -> - if is_assert_function v then -@@ -1834,9 +1839,10 @@ let instruction = function - v - (List.map expr eargs)) - in -- (locate (mkexpr enode pos))#node -+ (locate (mkexpr enode (Location.to_lexing_loc pos)))#node - - | Call(Some lv,{enode = Lval(Var v,NoOffset)},eargs,pos) -> -+ let lpos = Location.to_lexing_loc pos in - let enode = - if is_malloc_function v || is_realloc_function v then - let lvtyp = pointed_type (typeOfLval lv) in -@@ -1849,7 +1855,7 @@ let instruction = function - let arg = stripInfo arg in - let loc = arg.eloc in - let aux arg nelem = -- let factor = Integer.div (value_of_integral_expr arg) lvsiz in -+ let factor = Integer.e_div (value_of_integral_expr arg) lvsiz in - let siz = - if Integer.equal factor Integer.one then expr nelem - else -@@ -1862,12 +1868,12 @@ let instruction = function - let ty,arg = match arg.enode with - | Info _ -> assert false - | Const c when is_integral_const c -> -- let allocsiz = Integer.div (value_of_integral_expr arg) lvsiz -+ let allocsiz = Integer.e_div (value_of_integral_expr arg) lvsiz - in - let siznode = - JCPEconst(JCCinteger(Integer.to_string allocsiz)) - in -- lvtyp, mkexpr siznode pos -+ lvtyp, mkexpr siznode lpos - | BinOp(Mult,({enode = Const c} as arg),nelem,_ty) - when is_integral_const c -> aux arg nelem - | BinOp(Mult,nelem,({enode = Const c} as arg),_ty) -@@ -1895,7 +1901,7 @@ let instruction = function - | Const c when is_integral_const c -> - let lvtyp = pointed_type (typeOfLval lv) in - let lvsiz = Integer.of_int64 ((bits_sizeof lvtyp) lsr 3) in -- let factor = Integer.div (value_of_integral_expr arg) lvsiz in -+ let factor = Integer.e_div (value_of_integral_expr arg) lvsiz in - let siz = - if Integer.equal factor Integer.one then - expr nelem -@@ -1928,24 +1934,24 @@ let instruction = function - (List.map expr eargs)) - in - let lvty = typeOfLval lv in -- let call = locate (mkexpr enode pos) in -+ let call = locate (mkexpr enode lpos) in - let enode = - if Typ.equal lvty (getReturnType v.vtype) - || is_malloc_function v - || is_realloc_function v - || is_calloc_function v - then -- JCPEassign(lval pos lv,call) -+ JCPEassign(lval lpos lv,call) - else - let tmpv = makeTempVar (get_curFundec()) (getReturnType v.vtype) in - let tmplv = Var tmpv, NoOffset in - let cast = - new_exp ~loc:pos (CastE(lvty,new_exp ~loc:pos (Lval tmplv))) - in -- let tmpassign = JCPEassign(lval pos lv,expr cast) in -- JCPElet(None,tmpv.vname,Some call,locate (mkexpr tmpassign pos)) -+ let tmpassign = JCPEassign(lval lpos lv,expr cast) in -+ JCPElet(None,tmpv.vname,Some call,locate (mkexpr tmpassign lpos)) - in -- (locate (mkexpr enode pos))#node -+ (locate (mkexpr enode lpos))#node - - | Call _ -> Common.unsupported ~current:true "function pointers" - -@@ -1976,9 +1982,10 @@ let rec statement s = - in - *) - -+ let lpos = Location.to_lexing_loc pos in - let assert_before, contract = - Annotations.fold_code_annot -- (fun _ ca acc -> code_annot pos acc ca) s ([],None) -+ (fun _ ca acc -> code_annot lpos acc ca) s ([],None) - in - let snode = match s.skind with - | Instr i -> instruction i -@@ -1986,7 +1993,7 @@ let rec statement s = - | Return(Some e,_) -> JCPEreturn(expr e) - - | Return(None,_pos) -> -- JCPEreturn(mkexpr (JCPEconst JCCvoid) pos) -+ JCPEreturn(mkexpr (JCPEconst JCCvoid) lpos) - - | Goto(sref,_pos) -> - (* Pick the first non-case label in the list of labels associated to -@@ -2050,7 +2057,7 @@ let rec statement s = - | case_stmt :: _ as slist -> - let switch_labels = List.filter is_case_label case_stmt.labels in - let labs = List.map switch_label switch_labels in -- let slist = mkexpr (JCPEblock(statement_list slist)) pos in -+ let slist = mkexpr (JCPEblock(statement_list slist)) (Location.to_lexing_loc pos) in - labs, slist - in - let case_list = List.map case (case_blocks bl.bstmts slist) in -@@ -2098,7 +2105,7 @@ let rec statement s = - let inv = - match invs with - | [] -> None -- | _ -> Some (mkconjunct invs pos) -+ | _ -> Some (mkconjunct invs lpos) - in - let ass = assigns ass in - (beh_names,inv,ass)) -@@ -2119,7 +2126,7 @@ let rec statement s = - in - (* Prefix statement by all non-case labels *) - let labels = filter_out is_case_label s.labels in -- let s = mkexpr snode pos in -+ let s = mkexpr snode lpos in - let s = - match contract with - | None -> s -@@ -2145,13 +2152,13 @@ let rec statement s = - in - mkexpr - (JCPEcontract(requires, decreases, behaviors, s)) -- pos -+ lpos - in - let s = match assert_before @ [s] with - | [s] -> s -- | slist -> mkexpr (JCPEblock slist) pos -+ | slist -> mkexpr (JCPEblock slist) lpos - in -- List.fold_left (fun s lab -> mkexpr (JCPElabel(label lab,s)) pos) s labels -+ List.fold_left (fun s lab -> mkexpr (JCPElabel(label lab,s)) lpos) s labels - - and statement_list slist = List.rev (List.rev_map statement slist) - -@@ -2228,7 +2235,7 @@ let rec annotation is_axiomatic annot = - if _attr <> [] then warning "ignoring attributes of axiom %s" name; - ignore - (reg_position ~id:name -- ~name:("Lemma " ^ name) pos); -+ ~name:("Lemma " ^ name) (Location.to_lexing_loc pos)); - begin try - [JCDlemma(name,is_axiom,[],logic_labels labels,pred property)] - with (Unsupported _ | Log.FeatureRequest _) -@@ -2263,6 +2270,7 @@ let rec annotation is_axiomatic annot = - - | Dtype (info,pos) when info.lt_params=[] -> - CurrentLoc.set pos; -+ let lpos = Location.to_lexing_loc pos in - let myself = mktype (JCPTidentifier (info.lt_name,[])) in - let mydecl = JCDlogic_type (info.lt_name,[]) in - let axiomatic ctors = -@@ -2295,8 +2303,8 @@ let rec annotation is_axiomatic annot = - (* TODO: give unique name *) - (fun x -> - mkexpr (JCPEquantifier(Forall,ltype t, -- [new identifier prms_name], [],x)) pos), -- mkexpr (JCPEvar prms_name) pos -+ [new identifier prms_name], [],x)) lpos), -+ mkexpr (JCPEvar prms_name) lpos - in - let (quant,args) = - List.fold_right -@@ -2314,17 +2322,17 @@ let rec annotation is_axiomatic annot = - (mkexpr - (JCPEbinary - (mkexpr (JCPEapp (info.lt_name ^ "_tag",[], -- [mkexpr expr pos])) pos, -+ [mkexpr expr lpos])) lpos, - `Beq, -- mkexpr(JCPEconst(JCCinteger (Int64.to_string i))) pos)) -- pos) -+ mkexpr(JCPEconst(JCCinteger (Int64.to_string i))) lpos)) -+ lpos) - in - (i+one, - JCDlemma(cons.ctor_name ^ "_tag_val",true,[],[], pred) - ::axioms) - in - let (_,axioms) = List.fold_right tag_axiom ctors (zero,[]) in -- let xvar = mkexpr (JCPEvar "x") pos in (* TODO: give unique name *) -+ let xvar = mkexpr (JCPEvar "x") lpos in (* TODO: give unique name *) - let one_case cons = - let prms = ref(-1) in - let param t = -@@ -2333,8 +2341,8 @@ let rec annotation is_axiomatic annot = - (* TODO: give unique name *) - ((fun x -> - mkexpr (JCPEquantifier(Exists,ltype t, -- [new identifier prms_name], [],x)) pos), -- mkexpr (JCPEvar prms_name) pos) -+ [new identifier prms_name], [],x)) lpos), -+ mkexpr (JCPEvar prms_name) lpos) - in let (quant,args) = - List.fold_right - (fun arg (quants,args) -> -@@ -2345,7 +2353,7 @@ let rec annotation is_axiomatic annot = - quant - (mkexpr - (JCPEbinary(xvar,`Beq, -- mkexpr (JCPEapp(cons.ctor_name,[],args)) pos)) pos) -+ mkexpr (JCPEapp(cons.ctor_name,[],args)) lpos)) lpos) - in - match ctors with - [] -> cons -@@ -2354,7 +2362,7 @@ let rec annotation is_axiomatic annot = - [JCDlemma(info.lt_name ^ "_inductive", true, [], [], - (mkexpr (JCPEquantifier - (Forall,myself, -- [new identifier "x"], [],one_case x)) pos))] -+ [new identifier "x"], [],one_case x)) lpos))] - | x::l -> - tag_fun :: cons @ axioms @ - [JCDlemma(info.lt_name ^ "_inductive", true, [], [], -@@ -2365,8 +2373,8 @@ let rec annotation is_axiomatic annot = - List.fold_right - (fun cons case -> - mkexpr (JCPEbinary(case,`Blor, -- one_case cons)) pos) -- l (one_case x))) pos)] -+ one_case cons)) lpos) -+ l (one_case x))) lpos)] - in - (*NB: axioms stating that two values beginning with different - symbols are different are not generated. *) -@@ -2380,7 +2388,7 @@ let rec annotation is_axiomatic annot = - | _ when is_axiomatic -> axiomatic - | _ -> - [JCDaxiomatic (info.lt_name ^ "_axiomatic", -- List.map (fun x -> mkdecl x pos) axiomatic)]) -+ List.map (fun x -> mkdecl x lpos) axiomatic)]) - - | Dtype _ -> unsupported "type definitions" - | Dvolatile _ -> Common.unsupported "volatile variables" -@@ -2395,8 +2403,9 @@ let rec annotation is_axiomatic annot = - Format.eprintf "Translating axiomatic %s into jessie code@." id; - *) - let l = List.fold_left (fun acc d -> (annotation true d)@acc) [] l in -- [JCDaxiomatic(id,List.map (fun d -> mkdecl d pos) -+ [JCDaxiomatic(id,List.map (fun d -> mkdecl d (Location.to_lexing_loc pos)) - (List.rev l))] -+ | Dextended _ -> unsupported "extended global annotation" - - let default_field_modifiers = (false,false) - -@@ -2457,7 +2466,7 @@ let global vardefs g = - ignore(Typ.Hashtbl.find Norm.generated_union_types ty); - [JCDtag(compinfo.cname,[],None,fields,[])] - with Not_found -> -- let id = mkidentifier compinfo.cname pos in -+ let id = mkidentifier compinfo.cname (Location.to_lexing_loc pos) in - [ - JCDtag(compinfo.cname,[],None,fields,[]); - JCDvariant_type(compinfo.cname,[id]) -@@ -2466,9 +2475,10 @@ let global vardefs g = - - | GCompTag(compinfo,pos) -> (* union type *) - assert (not compinfo.cstruct); -+ let lpos = Location.to_lexing_loc pos in - let field fi = - let ty = pointed_type fi.ftype in -- mkidentifier (get_struct_name ty) pos -+ mkidentifier (get_struct_name ty) lpos - in - (* match pointed_type fi.ftype with *) - (* | TComp(compinfo,_) -> *) -@@ -2483,7 +2493,7 @@ let global vardefs g = - (* | _ -> *) - (* assert false *) - (* in *) -- let union_id = mkidentifier compinfo.cname pos in -+ let union_id = mkidentifier compinfo.cname lpos in - let union_size = match compinfo.cfields with - | [] -> 0 - | fi::_ -> -@@ -2558,7 +2568,7 @@ let global vardefs g = - | TFun(rt,_,_,_) -> rt - | _ -> assert false - in -- let id = mkidentifier v.vname pos in -+ let id = mkidentifier v.vname (Location.to_lexing_loc pos) in - let kf = Globals.Functions.get v in - Jessie_options.debug - "Getting spec of %s" (Kernel_function.get_name kf); -@@ -2587,22 +2597,23 @@ let global vardefs g = - if f.svar.vname = name_of_assert - || f.svar.vname = name_of_free then [] - else -+ let lpos = Location.to_lexing_loc pos in - let rty = match unrollType f.svar.vtype with - | TFun(ty,_,_,_) -> ty - | _ -> assert false - in - let formal v = true, ctype v.vtype, v.vname in - let formals = List.map formal f.sformals in -- let id = mkidentifier f.svar.vname f.svar.vdecl in -+ let id = mkidentifier f.svar.vname (Location.to_lexing_loc f.svar.vdecl) in - let funspec = - Annotations.funspec (Globals.Functions.get f.svar) - in - begin try - let local v = -- mkexpr (JCPEdecl(ctype v.vtype,v.vname,None)) v.vdecl -+ mkexpr (JCPEdecl(ctype v.vtype,v.vname,None)) (Location.to_lexing_loc v.vdecl) - in - let locals = List.rev (List.rev_map local f.slocals) in -- let body = mkexpr (JCPEblock(statement_list f.sbody.bstmts)) pos in -+ let body = mkexpr (JCPEblock(statement_list f.sbody.bstmts)) lpos in - let s,cba,dba = spec f.svar.vname funspec in - let body = - List.fold_left -@@ -2630,10 +2641,10 @@ let global vardefs g = - :: acc) - body dba - in -- let body = mkexpr (JCPEblock body) pos in -+ let body = mkexpr (JCPEblock body) lpos in - ignore - (reg_position ~id:f.svar.vname -- ~name:("Function " ^ f.svar.vname) f.svar.vdecl); -+ ~name:("Function " ^ f.svar.vname) (Location.to_lexing_loc f.svar.vdecl)); - [JCDfun(ctype rty,id,formals,s,Some body)] - with (Unsupported _ | Log.FeatureRequest _) - when drop_on_unsupported_feature -> -@@ -2652,7 +2663,7 @@ let global vardefs g = - | GAnnot(la,_) -> annotation false la - - in -- List.map (fun dnode -> mkdecl dnode pos) dnodes -+ List.map (fun dnode -> mkdecl dnode (Location.to_lexing_loc pos)) dnodes - - let integral_type name ty bitsize = - let min = min_value_of_integral_type ~bitsize ty in ---- frama-c-plugin/norm.ml.orig 2018-06-28 16:43:25.000000000 -0600 -+++ frama-c-plugin/norm.ml 2019-08-02 12:24:56.510573782 -0600 -@@ -471,6 +471,7 @@ object - end; - DoChildren (* FIXME: correct ? *) - | Dcustom_annot _ -> DoChildren (* FIXME: correct ? *) -+ | Dextended _ -> DoChildren (* FIXME: correct ? *) - in annot - - method! vterm_lval tlv = diff --git a/why.rpmlintrc b/why.rpmlintrc deleted file mode 100644 index d790618..0000000 --- a/why.rpmlintrc +++ /dev/null @@ -1,27 +0,0 @@ -# THIS FILE IS FOR WHITELISTING RPMLINT ERRORS AND WARNINGS IN TASKOTRON -# https://fedoraproject.org/wiki/Taskotron/Tasks/dist.rpmlint#Whitelisting_errors - -# The dictionary lacks some technical words -addFilter(r'W: spelling-error .* (frama|provers)') - -# Caused by ocaml; this package cannot fix it -addFilter(r'why[^:]+: E: missing-call-to-chdir-with-chroot') - -# Oh yes, we have no manual page -addFilter(r'W: no-manual-page-for-binary (jessie|krakatoa|patch_jessie_pvs)') - -# Indeed there is no documentation -addFilter(r'why.[^:]+: W: no-documentation') -addFilter(r'why-(jessie|pvs-support).[^:]*: W: no-documentation') - -# This is a devel package -addFilter(r'why-jessie\.[^:]+: W: devel-file-in-non-devel-package') - -# PVS creates, and requires, hidden files -addFilter(r'why-pvs-support\.[^:]+: W: hidden-file-or-dir .*\.pvscontext') - -# This package has no binary bits -addFilter(r'why-pvs-support\.[^:]+: W: only-non-binary-in-usr-lib') - -# The icons were created by the Fedora packager; there is no URL -addFilter(r'why\.spec: W: invalid-url Source[^:]+: why-icons\.tar\.xz') diff --git a/why.spec b/why.spec deleted file mode 100644 index 5aa375a..0000000 --- a/why.spec +++ /dev/null @@ -1,634 +0,0 @@ -# Whether PVS is available -%ifarch %{ix86} x86_64 ppc sparcv9 -%global has_pvs 1 -%else -%global has_pvs 0 -%endif - -Name: why -Version: 2.41 -Release: 11%{?dist} -Summary: Software verification platform - -License: LGPLv2 with exceptions -URL: http://why.lri.fr/ -Source0: http://why.lri.fr/download/%{name}-%{version}.tar.gz -Source1: http://krakatoa.lri.fr/manual/krakatoa.pdf -Source2: README.why-coq.Fedora -Source3: README.why -Source4: jessie.desktop -Source5: jessie.appdata.xml -Source6: div.pvs -Source7: rem.pvs -Source8: patch_jessie_pvs -# Created with gimp from official upstream icon -Source9: %{name}-icons.tar.xz -# Adapt to Frama-C 18.0 -Patch0: %{name}-frama-c.patch - -BuildRequires: auto-destdir -BuildRequires: desktop-file-utils -BuildRequires: xemacs xemacs-packages-extra -BuildRequires: frama-c -BuildRequires: gappalib-coq -BuildRequires: ocaml -BuildRequires: ocaml-apron-devel -BuildRequires: ocaml-camlp5-devel -BuildRequires: ocaml-findlib -BuildRequires: ocaml-mlgmpidl-devel -BuildRequires: ocaml-ocamldoc -BuildRequires: ocaml-ocamlgraph-devel -BuildRequires: ocaml-zarith-devel -BuildRequires: why3 -BuildRequires: coq -%if %{has_pvs} -BuildRequires: pvs -%endif - -Requires: gappalib-coq -Requires: hicolor-icon-theme -Requires: emacs-filesystem - -# Filter out bogus requires -%global __requires_exclude ocaml\\\((Ast|Cc|Env|Error|Jc_ast|Jc_env|Loc|Logic|Logic_decl|Misc|Ptree|Types)\\\) - -%description -Why is a software verification platform that applies formal proving -tools to annotated programs. It is currently capable of analysis of C -(through "Frama-C"), Java (through the included tool "Krakatoa"), and -potentially ML programs with some modification into Why's own ML-like -language. Furthermore, Why is capable of analysis of any program that -is mapped onto its own internal language. It uses a weakest -precondition involving calculus to generate potential theorems necessary -for the proof of a program's correctness. It translates these theorems -into formats that can be used by external proof assistants (without any -extra work Coq, PVS, HOL Light, and Mizar are supported - having one is -recommended and both Coq and PVS are packaged for Fedora) and automated -theorem provers (without any extra work Simplify, Alt-Ergo, Yices, Z3, -CVC3, and Zenon are supported and Alt-Ergo, Z3, and Zenon are packaged -for Fedora) so that these results can be externally proven, resulting in -a proof of program correctness. - -Note: Each user account must be set up by running "why-config" at the -command line (to set up a configuration file). - -%package jessie -Summary: Interface between why and frama-c -Requires: %{name}%{?_isa} = %{version}-%{release} -Requires: frama-c - -%description jessie -The Jessie plugin, an interface between why and frama-c. Invoke it with: - frama-c -jessie FILE.c - -%if %{has_pvs} -# Why's integration with PVS depends on the NASA Langley PVS Libraries, -# which have no license information. This provides an alternative: -%package pvs-support -Summary: Complete Why software verification platform suite -Requires: %{name}%{?_isa} = %{version}-%{release} -Requires: pvs - -%description pvs-support -This package provides support definitions so that the Why software -verification platform suite can invoke PVS without licensing issues. -%endif - -%package all -Summary: Complete Why software verification platform suite -Requires: why%{?_isa} = %{version}-%{release} -Requires: why-jessie%{?_isa} = %{version}-%{release} -%if %{has_pvs} -Requires: why-pvs-support%{?_isa} = %{version}-%{release} -%endif -Requires: alt-ergo yices z3 zenon - -%description all -This package provides a complete software verification platform suite -based on Why, including various automated and interactive provers. - -%prep -%setup -q -%setup -q -T -D -a 9 -%patch0 - -cp -p %SOURCE2 ./ - -# Link with Fedora LDFLAGS -for flag in $RPM_LD_FLAGS; do - sed -e "\%^bin/jessie\.opt%,\%^bin/jessie\.byte%s|-o|-ccopt $flag &|" \ - -e "/gtkThread\.cmx/s|-o|-ccopt $flag &|" \ - -i Makefile.in -done - -%define fix_encoding() \ - iconv -f %2 -t %3 %1 > %1.utf8; \ - touch -r %1 %1.utf8; \ - mv -f %1.utf8 %1; - -# Fix encodings -for f in CHANGES COPYING; do - %fix_encoding $f ISO-8859-1 UTF-8 -done - -# APRON support: add a missing rpath and adapt to newer versions of apron -sed -e "s|-lpolkaMPQ_caml|-Wl,-rpath,%{_libdir}/ocaml/apron|;s| -lbigarray||" \ - -e "s|box\.cmxa polka.cmxa|boxMPQ.cmxa polkaMPQ.cmxa octMPQ.cmxa|" \ - -i configure - -# Enable debuginfo -sed -i 's,@STRIP@,/usr/bin/true,;s,-dtypes [^-],-g &,' Makefile.in -sed -ri 's,ocaml(c|opt),& -g,' atp/Makefile - -# Command "pvs" is LVM2's /sbin/pvs, so rename "pvs" to pvs-sbcl: -sed -i 's/pvs/pvs-sbcl/' configure - -# Allow building with ocaml 4.07 and up -sed -i 's,4\.06\.\*,&|4.07.*|4.08.*|4.09.*|4.1*,' configure -sed -i 's,4\.0\*,4.*,' Makefile.in - -# Allow building with why3 1.2.1 -sed -i 's,0\.88\.\*,&|1.2.1,' configure - -# Allow building with Frama-C 19.1 -sed -i 's,Chlorine-20180501,19.1*,' configure - -%build -%ifarch %{ocaml_native_compiler} -%global opt_option OCAMLBEST=opt -%else -%global opt_option OCAMLBEST=byte OCAMLDEP=ocamldep OCAMLYACC=ocamlyacc OCAMLLEX=ocamllex -%endif - -%configure --enable-apron --enable-verbosemake -make %{opt_option} - -%install -# Avoid a bug in PVS batch mode when using emacs -make install DESTDIR=%{buildroot} %{opt_option} \ - PVSLIB=%{buildroot}%{_libdir}/pvs/lib PVSEMACS=xemacs - -# Fix permissions -chmod a-x %{buildroot}%{_libdir}/frama-c/plugins/META.frama-c-jessie -chmod a-x %{buildroot}%{_libdir}/frama-c/plugins/Jessie.cmi -chmod a-x %{buildroot}%{_libdir}/frama-c/plugins/top/Jessie.cm{a,o,x} - -# If no PVS, no .pvs files should be installed -%if ! %{has_pvs} -rm -fr %{buildroot}%{_libdir}/pvs -%endif - -# Install desktop file -desktop-file-install --dir=%{buildroot}%{_datadir}/applications %{SOURCE4} - -# Install AppData files -mkdir -p %{buildroot}%{_datadir}/appdata -install -pm 644 %{SOURCE5} %{buildroot}%{_datadir}/appdata - -# Install the icons -mkdir -p %{buildroot}%{_datadir}/icons -cp -a icons %{buildroot}%{_datadir}/icons/hicolor - -%if %{has_pvs} -# Get rid of a BUILDROOT reference in a log file (fails QA_CHECK_RPATHS) -sed -i "s|%{buildroot}||" %{buildroot}%{_libdir}/pvs/lib/why/top.out - -mkdir -p %{buildroot}%{_libdir}/pvs/lib/ints/ -cp -p %{SOURCE6} %{SOURCE7} %{buildroot}%{_libdir}/pvs/lib/ints/ -install -m755 -p %{SOURCE8} %{buildroot}%{_bindir}/ -%endif - -%global why_doc_dir %{?_pkgdocdir}%{!?_pkgdocdir:%{_docdir}/%{name}-%{version}} - -# Fix up documentation and examples -mkdir -p %{buildroot}%{why_doc_dir} -cp -p %{SOURCE1} %{SOURCE2} %{SOURCE3} CHANGES README Version \ - %{buildroot}%{why_doc_dir} - -%check -make check - -%files -%license COPYING LICENSE -%{_bindir}/krakatoa -%{_libdir}/why/ -%{_datadir}/icons/hicolor/*/apps/%{name}.png -%{why_doc_dir}/ - -%files jessie -%{_bindir}/jessie -%{_libdir}/frama-c/plugins/Jessie.cmi -%{_libdir}/frama-c/plugins/META.frama-c-jessie -%{_libdir}/frama-c/plugins/top/Jessie.* -%{_datadir}/appdata/jessie.appdata.xml -%{_datadir}/applications/jessie.desktop - -%if %{has_pvs} -%files pvs-support -%{_libdir}/pvs/lib/* -%{_bindir}/patch_jessie_pvs -%endif - -# "why-all" is a meta-package; it just depends on other packages, so that -# it's easier to install a useful suite of tools. Thus, it has no files: -%files all - - -%changelog -* Fri Jan 31 2020 Fedora Release Engineering - 2.41-11 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild - -* Thu Jan 23 2020 Jerry James - 2.41-10 -- Rebuild for apron 0.9.12 - -* Mon Dec 9 2019 Jerry James - 2.41-9 -- OCaml 4.09.0 (final) rebuild. - -* Tue Oct 29 2019 Jerry James - 2.41-8 -- Rebuild for why3 1.2.1 - -* Fri Oct 11 2019 Jerry James - 2.41-7 -- Rebuild for ocaml-mlgmpidl 1.2.11 - -* Mon Sep 23 2019 Jerry James - 2.41-6 -- Rebuild for frama-c 19.1 - -* Fri Sep 6 2019 Jerry James - 2.41-5 -- Rebuild for ocaml-zarith 1.9 - -* Fri Aug 2 2019 Jerry James - 2.41-4 -- Rebuild for frama-c 19.0 - -* Sat Jul 27 2019 Fedora Release Engineering - 2.41-4 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild - -* Wed Jun 5 2019 Jerry James - 2.41-3 -- Rebuild for coq 8.9.1, why3 1.2.0, and frama-c 18.0 - -* Sun Feb 03 2019 Fedora Release Engineering - 2.41-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild - -* Sat Jan 26 2019 Jerry James - 2.41-1 -- New upstream release -- All patches have been upstreamed; drop them all - -* Sat Jul 14 2018 Fedora Release Engineering - 2.40-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild - -* Mon Feb 12 2018 Jerry James - 2.40-1 -- New upstream release -- Add -num patch to fix incomplete num to zarith conversion - -* Fri Feb 09 2018 Fedora Release Engineering - 2.39-5 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild - -* Thu Jan 18 2018 Igor Gnatenko - 2.39-4 -- Remove obsolete scriptlets - -* Sat Dec 9 2017 Jerry James - 2.39-3 -- Bring back the -project patch, still needed (bz 1520483) -- Add the -safe-string patch for building with ocaml 4.06.0 -- Build the Jessie plugin with -runtime-variant _pic - -* Sat Dec 02 2017 Richard W.M. Jones - 2.39-3 -- OCaml 4.06.0 rebuild. - -* Sat Oct 7 2017 Jerry James - 2.39-2 -- Rebuild for why3 0.88.0 - -* Thu Sep 7 2017 Jerry James - 2.39-1 -- New upstream release - -* Wed Sep 06 2017 Richard W.M. Jones - 2.38-6 -- OCaml 4.05.0 rebuild. - -* Thu Aug 03 2017 Fedora Release Engineering - 2.38-5 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Binutils_Mass_Rebuild - -* Thu Jul 27 2017 Fedora Release Engineering - 2.38-4 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild - -* Sat Jul 01 2017 Richard W.M. Jones - 2.38-3 -- Rebuild for OCaml 4.04.2. - -* Mon May 15 2017 Richard W.M. Jones - 2.38-2 -- Rebuild for OCaml 4.04.1. - -* Fri Mar 24 2017 Jerry James - 2.38-1 -- New upstream release - -* Sat Feb 11 2017 Fedora Release Engineering - 2.36-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild - -* Thu Jan 12 2017 Jerry James - 2.36-1 -- New upstream release - -* Wed Nov 30 2016 Jerry James - 2.35-23 -- Rebuild for gappalib-coq 1.3.2 - -* Sun Nov 06 2016 Richard W.M. Jones - 2.35-21 -- Rebuild for OCaml 4.04.0. -- Modify configure script to allow building with OCaml 4.04. -- Modify configure script to use octMPQ library (part of Apron). - -* Fri Oct 28 2016 Jerry James - 2.35-20 -- Rebuild for coq 8.5pl3 -- Remove obsolete scriptlets - -* Thu Sep 29 2016 Jerry James - 2.35-19 -- Rebuild for flocq 2.5.2 and gappalib-coq 1.3.1 - -* Fri Sep 2 2016 Jerry James - 2.35-18 -- Rebuild for why3 0.87.2 - -* Fri Jul 22 2016 Jerry James - 2.35-17 -- Rebuild for apron 0.9.11 and gappalib-coq 1.3.0 - -* Wed Jul 13 2016 Jerry James - 2.35-16 -- Rebuild for coq 8.5pl2 - -* Wed Jun 1 2016 Jerry James - 2.35-15 -- Rebuild for why3 0.87.1 and Frama-C Aluminium - -* Fri Apr 22 2016 Jerry James - 2.35-14 -- Rebuild for coq 8.5pl1 - -* Sat Apr 16 2016 Jerry James - 2.35-13 -- Rebuild for ocaml-ocamlgraph 1.8.7 - -* Fri Mar 18 2016 Jerry James - 2.35-12 -- Rebuild for why3 0.87.0 - -* Fri Feb 12 2016 Jerry James - 2.35-11 -- Rebuild for coq 8.5, flocq 2.5.1, gappalib-coq 1.2.1, why3 0.86.3, and - Frama-C Magnesium -- Use camlp4 in preference to camlp5 -- Drop cvc3 support -- Update appdata for latest specification - -* Fri Feb 05 2016 Fedora Release Engineering - 2.35-10 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild - -* Wed Oct 14 2015 Jerry James - 2.35-9 -- Rebuild for flocq 2.5.0, gappalib-coq 1.2.0, and why3 0.86.2 - -* Thu Jul 30 2015 Richard W.M. Jones - 2.35-8 -- OCaml 4.02.3 rebuild. - -* Mon Jun 22 2015 Jerry James - 2.35-7 -- Rebuild for why3 0.86.1 - -* Fri Jun 19 2015 Richard W.M. Jones - 2.35-6 -- Rebuild for ocaml-4.02.2. - -* Fri Jun 19 2015 Fedora Release Engineering - 2.35-5 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_23_Mass_Rebuild - -* Sat May 16 2015 Jerry James - 2.35-4 -- Rebuild for why3 0.86 - -* Mon Apr 13 2015 Jerry James - 2.35-3 -- Rebuild for coq 8.4pl6 - -* Wed Apr 1 2015 Jerry James - 2.35-2 -- Adjust requires filter - -* Tue Mar 31 2015 Jerry James - 2.35-1 -- New upstream release -- Drop upstreamed -flocq24 and -frama-c-sodium patches -- Drop all gwhy-related sources, as gwhy has been retired -- Merge (X)Emacs files into the main package due to change in policy - -* Thu Mar 19 2015 Jerry James - 2.34-18 -- Rebuild for Frama-C Sodium -- Add -ocamlgraph186 patch to adapt to ocamlgraph 1.8.6 -- Add -frama-c-sodium patch to adapt to Frama-C Sodium - -* Thu Feb 19 2015 Richard W.M. Jones - 2.34-17 -- ocaml-4.02.1 rebuild. - -* Sat Nov 15 2014 Jerry James - 2.34-16 -- Fix gwhy-2.33.patch (bz 1164470) - -* Thu Nov 13 2014 Richard W.M. Jones - 2.34-15 -- Bump and rebuild for broken dependencies. - -* Thu Oct 30 2014 Jerry James - 2.34-14 -- Rebuild for coq 8.4pl5 - -* Thu Sep 18 2014 Jerry James - 2.34-13 -- Rebuild for why3 0.85 - -* Mon Sep 8 2014 Jerry James - 2.34-12 -- Rebuild for fixed frama-c -- Fix license handling - -* Tue Sep 2 2014 Jerry James - 2.34-11 -- Rebuild for the final ocaml 4.02.0 release - -* Mon Aug 25 2014 Jerry James - 2.34-10 -- ocaml-4.02.0+rc1 rebuild. - -* Mon Aug 18 2014 Fedora Release Engineering - 2.34-9 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild - -* Mon Aug 4 2014 Jerry James - 2.34-8 -- OCaml 4.02.0 beta rebuild -- BR emacs instead of emacs-nox, which no longer exists - -* Tue Jun 24 2014 Jerry James - 2.34-7 -- Omit "-z now" when building with relro (bz 1105265) -- Resolve a conflict between Frama-C and why modules both named "Project" - -* Sun Jun 08 2014 Fedora Release Engineering - 2.34-6 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild - -* Tue May 13 2014 Jerry James - 2.34-5 -- Rebuild for coq 8.4pl4 - -* Mon Apr 21 2014 Jerry James - 2.34-4 -- Rebuild for ocamlgraph 1.8.5 and flocq 2.3.0 -- Drop has_coq macro, since coq is now universally available -- Add -flocq23 patch to adapt to flocq 2.3.0 - -* Tue Apr 15 2014 Richard W.M. Jones - 2.34-3 -- Remove ocaml_arches macro (RHBZ#1087794). - -* Mon Mar 24 2014 Jerry James - 2.34-2 -- Remove dropped patches -- Add icons -- Fix the desktop icon entries - -* Tue Mar 18 2014 Jerry James - 2.34-1 -- New upstream release -- Drop upstreamed -hashtbl, -flocq, and -or patches -- Add ocaml-findlib BR - -* Wed Feb 26 2014 Jerry James - 2.33-6 -- Rebuild for ocamlgraph 1.8.4 -- Update desktop files -- Add AppData files for gwhy and jessie - -* Tue Sep 17 2013 Jerry James - 2.33-5 -- Rebuild for OCaml 4.01.0 -- Enable debuginfo -- Add -or patch to fix warnings, since warnings are errors - -* Sat Jul 27 2013 Ville Skyttä - 2.33-4 -- Install docs to %%{_pkgdocdir} where available. - -* Fri Jun 21 2013 Jerry James - 2.33-3 -- Rebuild for frama-c Fluorine 20130601 - -* Thu May 23 2013 Jerry James - 2.33-2 -- Rebuild for new frama-c and why3 builds - -* Tue May 14 2013 Jerry James - 2.33-1 -- New upstream release -- Drop upstreamed -warning, -coq84, and -ocaml4 patches -- Add -hashtbl patch -- Enable Jessie plugin again - -* Sat Feb 09 2013 Parag Nemade - 2.31-7 -- Remove vendor tag from desktop file as per https://fedorahosted.org/fesco/ticket/1077 - -* Mon Jan 14 2013 Jerry James - 2.31-6 -- Rebuild for alt-ergo 0.95 - -* Mon Jan 7 2013 Jerry James - 2.31-5 -- Rebuild for coq 8.4pl1 - -* Fri Oct 19 2012 Jerry James - 2.31-4 -- Rebuild for OCaml 4.00.1 and frama-c Oxygen -- Recripple the Jessie plugin until it works with frama-c Oxygen - -* Tue Sep 11 2012 Jerry James - 2.31-3 -- Rebuild for new frama-c build with altered API. - -* Mon Aug 27 2012 Jerry James - 2.31-2 -- Frama-c is fixed; rebuild with the Jessie plugin enabled and functioning - -* Thu Aug 23 2012 Jerry James - 2.31-1 -- New upstream version -- Drop upstreamed patches -- Add ocaml-mlgmpidl-devel and why3 BRs -- Add -warning, -ocaml4, and -coq84 patches to fix the build -- Cripple the Jessie plugin until problems with frama-c and hashtables are fixed - -* Mon Jul 30 2012 Richard W.M. Jones - 2.30-7 -- Rebuild for OCaml 4.00.0 official. - -* Sun Jul 22 2012 Fedora Release Engineering - 2.30-6 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild - -* Wed Jan 11 2012 Jerry James - 2.30-5 -- Patch to work with flocq 2.0.0 - -* Tue Dec 27 2011 Jerry James - 2.30-4 -- Rebuild for coq 8.3pl3 - -* Tue Dec 6 2011 Jerry James - 2.30-3 -- Update alt_ergo and yices "okay" version numbers - -* Wed Nov 23 2011 Jerry James - 2.30-2 -- Rebuild with APRON and gappalib-coq support - -* Fri Oct 28 2011 Jerry James - 2.30-1 -- New upstream release - -* Thu Jul 14 2011 Jerry James - 2.29-2 -- Fix broken conditionals - -* Mon Jul 11 2011 Jerry James - 2.29-1 -- New upstream release (fixes FTBFS: bz 715902) -- Remove unnecessary spec file elements (BuildRoot, etc.) -- Update approach to filtering provides and requires -- Add has_pvs analogously to has_coq, and simplify macro usage -- Add (X)Emacs support packages -- New subpackage for the jessie plugin to avoid unowned directories and - permit a direct dependency on frama-c -- Prepare for the eventual availability of APRON - -* Thu Apr 14 2011 Karsten Hopp 2.28-2.2 -- add ppc to excludearch, too. No pvs-sbcl available there - -* Wed Apr 13 2011 Karsten Hopp 2.28-2.1 -- add ppc64 to excludearch, no sbcl available there - -* Mon Feb 07 2011 Fedora Release Engineering - 2.28-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_15_Mass_Rebuild - -* Fri Jan 21 2011 Richard W.M. Jones - 2.28-1 -- Since 2.26 FTBFS, try latest upstream (2.28). -- Rebase Makefile.in patch. -- Fix(?) test result. -- No libdir/frama-c directory is created any more. - -* Fri Jan 21 2011 Richard W.M. Jones - 2.26-2 -- Bump and rebuild for OCaml 3.12. - -* Sat Oct 09 2010 David A. Wheeler + Mark Rader - 2.26-1 -- Upgrade to upstream version 2.26 (inc. update of krakatoa.pdf) -- Integrated with Frama-C and PVS (as pvs-sbcl) - -* Mon Jan 11 2010 Richard W.M. Jones - 2.23-2 -- Rebuild to fix dependencies. - -* Fri Jan 08 2010 Alan Dunn - 2.23-1 -- Upgrade to upstream version 2.23 -- Move execstack fixing to spec file from patch -- Moved patch descriptions to initial patch declaration as in examples - in Fedora documentation -- New Caduceus, Krakatoa documentation -- Update test result from small test min.mlw -- Added CVC3 interfacing capabilities -- Removed patch for gwhy configuration, as there is a new mechanism for this - -* Tue Sep 22 2009 Dennis Gilmore - 2.17-5 -- Exclude sparc64 s390 s390x there is no ocaml there - -* Fri Aug 07 2009 Alan Dunn - 2.17-4 -- Removed now irrelevant check for no OCaml in Fedora < 9 (those - distributions are EOL) -- Changed ExcludeArch to proper Fedora versions -- Builds coq subpackage exactly when Coq can be built, thus making - build independent of whether Coq can be built -- define -> global -- Fixed accidental use of in tar ocamlgraph instead of one that is - separately packaged - -* Mon Jul 27 2009 Fedora Release Engineering - 2.17-3 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_12_Mass_Rebuild - -* Wed Feb 25 2009 Fedora Release Engineering - 2.17-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_11_Mass_Rebuild - -* Wed Dec 24 2008 Alan Dunn 2.17-1 -- Upgrade to version 2.17 (bz: 477790) -- Add ownership of two directories common with Coq, but neither program requires the other (bz: 474016) -- Minor filename change in 2.17 (GPL -> LICENSE) -- Added back Coq .v files to match policy for Coq -- Changed directory structure re: jessie and krakatoa to match new structure in 2.17 -- Minor changes to patches to ensure they still work in 2.17 -- Corrected package location gwhy-icon.png (should only be in gwhy) -* Tue Aug 5 2008 Alan Dunn 2.14-2.1 -- ExcludeArch ppc64 on Fedora 8 due to no ocaml. -* Fri Aug 1 2008 Alan Dunn 2.14-2 -- Fixed minor issues in response to package review: -- Inclusion of COPYING, GPL license-related files -- Added config.mll patch to make default config file created nicer -- Changes subpackage dependencies to be fully versioned. -- Makes during build allowed to be noisy (allowed to print). -* Wed Jul 30 2008 Alan Dunn 2.14-1 -- Changed to new version of why, removed previous why-cpulimit name - change, zenon output format patches as the issues were fixed in - why 2.14. -- Moved doc subpackage back into main package. -- Added example files to documentation subpackage. -- Added check section with test on small why file. -- Reformatted some macro names for greater readability. -* Thu Jul 24 2008 Alan Dunn 2.13-2 -- Added several patches: fixed Zenon output, completed fix of rename - of cpulimit -> why-cpulimit. -* Wed Jul 23 2008 Alan Dunn 2.13-1 -- Initial Fedora RPM version.
%s%s
Interactive proof sessionMax function proofBinary search function proofBinary search arithmetic overflowBinar search function behavior