The package rpms/why.git has added or updated architecture specific content in its spec file (ExclusiveArch/ExcludeArch or %ifarch/%ifnarch) in commit(s): https://src.fedoraproject.org/cgit/rpms/why.git/commit/?id=a8d84c45d49b59c72....
Change: -%ifarch %{ocaml_native_compiler}
Thanks.
Full change: ============
commit a8d84c45d49b59c72c1e0161fbb63397ffb01629 Author: Jerry James loganjerry@gmail.com Date: Mon Mar 30 08:51:13 2020 -0600
Abandoned by upstream and fails to build from source
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 @@ -<?xml version="1.0" encoding="UTF-8"?> -<component type="desktop"> - <id>jessie.desktop</id> - <metadata_license>CC0-1.0</metadata_license> - <project_license>LGPL-2.1</project_license> - <name>jessie</name> - <summary>Interface between why and Frama-C</summary> - <description> - <p> - Jessie is an interface between why and Frama-C. - </p> - <p> - 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. - </p> - </description> - <screenshots> - <screenshot type="default"> - <image>http://krakatoa.lri.fr/jessie/max_why3ide.png</image> - <caption>Interactive proof session</caption> - </screenshot> - <screenshot> - <image>http://krakatoa.lri.fr/jessie/max_ptr_why3ide.png</image> - <caption>Max function proof</caption> - </screenshot> - <screenshot> - <image>http://krakatoa.lri.fr/jessie/binary_search_raw.png</image> - <caption>Binary search function proof</caption> - </screenshot> - <screenshot> - <image>http://krakatoa.lri.fr/jessie/binary_search_ovfl.png</image> - <caption>Binary search arithmetic overflow</caption> - </screenshot> - <screenshot> - <image>http://krakatoa.lri.fr/jessie/binary_search_behav.png</image> - <caption>Binar search function behavior</caption> - </screenshot> - </screenshots> - <update_contact>loganjerry@gmail.com</update_contact> - <url type="homepage">http://krakatoa.lri.fr/</url> - <url type="bugtracker">https://gforge.inria.fr/tracker/?atid=4012&group_id=999&func=browse</url> -</component> 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_err... - -# 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/%%7Bname%7D-%%7Bversion%7D.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 releng@fedoraproject.org - 2.41-11 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild - -* Thu Jan 23 2020 Jerry James loganjerry@gmail.com - 2.41-10 -- Rebuild for apron 0.9.12 - -* Mon Dec 9 2019 Jerry James loganjerry@gmail.com - 2.41-9 -- OCaml 4.09.0 (final) rebuild. - -* Tue Oct 29 2019 Jerry James loganjerry@gmail.com - 2.41-8 -- Rebuild for why3 1.2.1 - -* Fri Oct 11 2019 Jerry James loganjerry@gmail.com - 2.41-7 -- Rebuild for ocaml-mlgmpidl 1.2.11 - -* Mon Sep 23 2019 Jerry James loganjerry@gmail.com - 2.41-6 -- Rebuild for frama-c 19.1 - -* Fri Sep 6 2019 Jerry James loganjerry@gmail.com - 2.41-5 -- Rebuild for ocaml-zarith 1.9 - -* Fri Aug 2 2019 Jerry James loganjerry@gmail.com - 2.41-4 -- Rebuild for frama-c 19.0 - -* Sat Jul 27 2019 Fedora Release Engineering releng@fedoraproject.org - 2.41-4 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild - -* Wed Jun 5 2019 Jerry James loganjerry@gmail.com - 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 releng@fedoraproject.org - 2.41-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild - -* Sat Jan 26 2019 Jerry James loganjerry@gmail.com - 2.41-1 -- New upstream release -- All patches have been upstreamed; drop them all - -* Sat Jul 14 2018 Fedora Release Engineering releng@fedoraproject.org - 2.40-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild - -* Mon Feb 12 2018 Jerry James loganjerry@gmail.com - 2.40-1 -- New upstream release -- Add -num patch to fix incomplete num to zarith conversion - -* Fri Feb 09 2018 Fedora Release Engineering releng@fedoraproject.org - 2.39-5 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild - -* Thu Jan 18 2018 Igor Gnatenko ignatenkobrain@fedoraproject.org - 2.39-4 -- Remove obsolete scriptlets - -* Sat Dec 9 2017 Jerry James loganjerry@gmail.com - 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 rjones@redhat.com - 2.39-3 -- OCaml 4.06.0 rebuild. - -* Sat Oct 7 2017 Jerry James loganjerry@gmail.com - 2.39-2 -- Rebuild for why3 0.88.0 - -* Thu Sep 7 2017 Jerry James loganjerry@gmail.com - 2.39-1 -- New upstream release - -* Wed Sep 06 2017 Richard W.M. Jones rjones@redhat.com - 2.38-6 -- OCaml 4.05.0 rebuild. - -* Thu Aug 03 2017 Fedora Release Engineering releng@fedoraproject.org - 2.38-5 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Binutils_Mass_Rebuild - -* Thu Jul 27 2017 Fedora Release Engineering releng@fedoraproject.org - 2.38-4 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild - -* Sat Jul 01 2017 Richard W.M. Jones rjones@redhat.com - 2.38-3 -- Rebuild for OCaml 4.04.2. - -* Mon May 15 2017 Richard W.M. Jones rjones@redhat.com - 2.38-2 -- Rebuild for OCaml 4.04.1. - -* Fri Mar 24 2017 Jerry James loganjerry@gmail.com - 2.38-1 -- New upstream release - -* Sat Feb 11 2017 Fedora Release Engineering releng@fedoraproject.org - 2.36-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild - -* Thu Jan 12 2017 Jerry James loganjerry@gmail.com - 2.36-1 -- New upstream release - -* Wed Nov 30 2016 Jerry James loganjerry@gmail.com - 2.35-23 -- Rebuild for gappalib-coq 1.3.2 - -* Sun Nov 06 2016 Richard W.M. Jones rjones@redhat.com - 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 loganjerry@gmail.com - 2.35-20 -- Rebuild for coq 8.5pl3 -- Remove obsolete scriptlets - -* Thu Sep 29 2016 Jerry James loganjerry@gmail.com - 2.35-19 -- Rebuild for flocq 2.5.2 and gappalib-coq 1.3.1 - -* Fri Sep 2 2016 Jerry James loganjerry@gmail.com - 2.35-18 -- Rebuild for why3 0.87.2 - -* Fri Jul 22 2016 Jerry James loganjerry@gmail.com - 2.35-17 -- Rebuild for apron 0.9.11 and gappalib-coq 1.3.0 - -* Wed Jul 13 2016 Jerry James loganjerry@gmail.com - 2.35-16 -- Rebuild for coq 8.5pl2 - -* Wed Jun 1 2016 Jerry James loganjerry@gmail.com - 2.35-15 -- Rebuild for why3 0.87.1 and Frama-C Aluminium - -* Fri Apr 22 2016 Jerry James loganjerry@gmail.com - 2.35-14 -- Rebuild for coq 8.5pl1 - -* Sat Apr 16 2016 Jerry James loganjerry@gmail.com - 2.35-13 -- Rebuild for ocaml-ocamlgraph 1.8.7 - -* Fri Mar 18 2016 Jerry James loganjerry@gmail.com - 2.35-12 -- Rebuild for why3 0.87.0 - -* Fri Feb 12 2016 Jerry James loganjerry@gmail.com - 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 releng@fedoraproject.org - 2.35-10 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild - -* Wed Oct 14 2015 Jerry James loganjerry@gmail.com - 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 rjones@redhat.com - 2.35-8 -- OCaml 4.02.3 rebuild. - -* Mon Jun 22 2015 Jerry James loganjerry@gmail.com - 2.35-7 -- Rebuild for why3 0.86.1 - -* Fri Jun 19 2015 Richard W.M. Jones rjones@redhat.com - 2.35-6 -- Rebuild for ocaml-4.02.2. - -* Fri Jun 19 2015 Fedora Release Engineering rel-eng@lists.fedoraproject.org - 2.35-5 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_23_Mass_Rebuild - -* Sat May 16 2015 Jerry James loganjerry@gmail.com - 2.35-4 -- Rebuild for why3 0.86 - -* Mon Apr 13 2015 Jerry James loganjerry@gmail.com - 2.35-3 -- Rebuild for coq 8.4pl6 - -* Wed Apr 1 2015 Jerry James loganjerry@gmail.com - 2.35-2 -- Adjust requires filter - -* Tue Mar 31 2015 Jerry James loganjerry@gmail.com - 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 loganjerry@gmail.com - 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 rjones@redhat.com - 2.34-17 -- ocaml-4.02.1 rebuild. - -* Sat Nov 15 2014 Jerry James loganjerry@gmail.com - 2.34-16 -- Fix gwhy-2.33.patch (bz 1164470) - -* Thu Nov 13 2014 Richard W.M. Jones rjones@redhat.com - 2.34-15 -- Bump and rebuild for broken dependencies. - -* Thu Oct 30 2014 Jerry James loganjerry@gmail.com - 2.34-14 -- Rebuild for coq 8.4pl5 - -* Thu Sep 18 2014 Jerry James loganjerry@gmail.com - 2.34-13 -- Rebuild for why3 0.85 - -* Mon Sep 8 2014 Jerry James loganjerry@gmail.com - 2.34-12 -- Rebuild for fixed frama-c -- Fix license handling - -* Tue Sep 2 2014 Jerry James loganjerry@gmail.com - 2.34-11 -- Rebuild for the final ocaml 4.02.0 release - -* Mon Aug 25 2014 Jerry James loganjerry@gmail.com - 2.34-10 -- ocaml-4.02.0+rc1 rebuild. - -* Mon Aug 18 2014 Fedora Release Engineering rel-eng@lists.fedoraproject.org - 2.34-9 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild - -* Mon Aug 4 2014 Jerry James loganjerry@gmail.com - 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 loganjerry@gmail.com - 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 rel-eng@lists.fedoraproject.org - 2.34-6 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild - -* Tue May 13 2014 Jerry James loganjerry@gmail.com - 2.34-5 -- Rebuild for coq 8.4pl4 - -* Mon Apr 21 2014 Jerry James loganjerry@gmail.com - 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 rjones@redhat.com - 2.34-3 -- Remove ocaml_arches macro (RHBZ#1087794). - -* Mon Mar 24 2014 Jerry James loganjerry@gmail.com - 2.34-2 -- Remove dropped patches -- Add icons -- Fix the desktop icon entries - -* Tue Mar 18 2014 Jerry James loganjerry@gmail.com - 2.34-1 -- New upstream release -- Drop upstreamed -hashtbl, -flocq, and -or patches -- Add ocaml-findlib BR - -* Wed Feb 26 2014 Jerry James loganjerry@gmail.com - 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 loganjerry@gmail.com - 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 ville.skytta@iki.fi - 2.33-4 -- Install docs to %%{_pkgdocdir} where available. - -* Fri Jun 21 2013 Jerry James loganjerry@gmail.com - 2.33-3 -- Rebuild for frama-c Fluorine 20130601 - -* Thu May 23 2013 Jerry James loganjerry@gmail.com - 2.33-2 -- Rebuild for new frama-c and why3 builds - -* Tue May 14 2013 Jerry James loganjerry@gmail.com - 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 <paragn AT fedoraproject DOT org> - 2.31-7 -- Remove vendor tag from desktop file as per https://fedorahosted.org/fesco/ticket/1077 - -* Mon Jan 14 2013 Jerry James loganjerry@gmail.com - 2.31-6 -- Rebuild for alt-ergo 0.95 - -* Mon Jan 7 2013 Jerry James loganjerry@gmail.com - 2.31-5 -- Rebuild for coq 8.4pl1 - -* Fri Oct 19 2012 Jerry James loganjerry@gmail.com - 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 loganjerry@gmail.com - 2.31-3 -- Rebuild for new frama-c build with altered API. - -* Mon Aug 27 2012 Jerry James loganjerry@gmail.com - 2.31-2 -- Frama-c is fixed; rebuild with the Jessie plugin enabled and functioning - -* Thu Aug 23 2012 Jerry James loganjerry@gmail.com - 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 rjones@redhat.com - 2.30-7 -- Rebuild for OCaml 4.00.0 official. - -* Sun Jul 22 2012 Fedora Release Engineering rel-eng@lists.fedoraproject.org - 2.30-6 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild - -* Wed Jan 11 2012 Jerry James loganjerry@gmail.com - 2.30-5 -- Patch to work with flocq 2.0.0 - -* Tue Dec 27 2011 Jerry James loganjerry@gmail.com - 2.30-4 -- Rebuild for coq 8.3pl3 - -* Tue Dec 6 2011 Jerry James loganjerry@gmail.com - 2.30-3 -- Update alt_ergo and yices "okay" version numbers - -* Wed Nov 23 2011 Jerry James loganjerry@gmail.com - 2.30-2 -- Rebuild with APRON and gappalib-coq support - -* Fri Oct 28 2011 Jerry James loganjerry@gmail.com - 2.30-1 -- New upstream release - -* Thu Jul 14 2011 Jerry James loganjerry@gmail.com - 2.29-2 -- Fix broken conditionals - -* Mon Jul 11 2011 Jerry James loganjerry@gmail.com - 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 karsten@redhat.com 2.28-2.2 -- add ppc to excludearch, too. No pvs-sbcl available there - -* Wed Apr 13 2011 Karsten Hopp karsten@redhat.com 2.28-2.1 -- add ppc64 to excludearch, no sbcl available there - -* Mon Feb 07 2011 Fedora Release Engineering rel-eng@lists.fedoraproject.org - 2.28-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_15_Mass_Rebuild - -* Fri Jan 21 2011 Richard W.M. Jones rjones@gmail.com - 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 rjones@gmail.com - 2.26-2 -- Bump and rebuild for OCaml 3.12. - -* Sat Oct 09 2010 David A. Wheeler + Mark Rader dwheeler@dwheeler.com - 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 rjones@gmail.com - 2.23-2 -- Rebuild to fix dependencies. - -* Fri Jan 08 2010 Alan Dunn amdunn@gmail.com - 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 dennis@ausil.us - 2.17-5 -- Exclude sparc64 s390 s390x there is no ocaml there - -* Fri Aug 07 2009 Alan Dunn amdunn@gmail.com - 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 rel-eng@lists.fedoraproject.org - 2.17-3 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_12_Mass_Rebuild - -* Wed Feb 25 2009 Fedora Release Engineering rel-eng@lists.fedoraproject.org - 2.17-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_11_Mass_Rebuild - -* Wed Dec 24 2008 Alan Dunn amdunn@gmail.com 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 amdunn@gmail.com 2.14-2.1 -- ExcludeArch ppc64 on Fedora 8 due to no ocaml. -* Fri Aug 1 2008 Alan Dunn amdunn@gmail.com 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 amdunn@gmail.com 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 amdunn@gmail.com 2.13-2 -- Added several patches: fixed Zenon output, completed fix of rename - of cpulimit -> why-cpulimit. -* Wed Jul 23 2008 Alan Dunn amdunn@gmail.com 2.13-1 -- Initial Fedora RPM version.
arch-excludes@lists.fedoraproject.org