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=a8d84c45d49b59....
Change:
-%ifarch %{ocaml_native_compiler}
Thanks.
Full change:
============
commit a8d84c45d49b59c72c1e0161fbb63397ffb01629
Author: Jerry James <loganjerry(a)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(a)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_...
-
-# 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 <releng(a)fedoraproject.org> - 2.41-11
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild
-
-* Thu Jan 23 2020 Jerry James <loganjerry(a)gmail.com> - 2.41-10
-- Rebuild for apron 0.9.12
-
-* Mon Dec 9 2019 Jerry James <loganjerry(a)gmail.com> - 2.41-9
-- OCaml 4.09.0 (final) rebuild.
-
-* Tue Oct 29 2019 Jerry James <loganjerry(a)gmail.com> - 2.41-8
-- Rebuild for why3 1.2.1
-
-* Fri Oct 11 2019 Jerry James <loganjerry(a)gmail.com> - 2.41-7
-- Rebuild for ocaml-mlgmpidl 1.2.11
-
-* Mon Sep 23 2019 Jerry James <loganjerry(a)gmail.com> - 2.41-6
-- Rebuild for frama-c 19.1
-
-* Fri Sep 6 2019 Jerry James <loganjerry(a)gmail.com> - 2.41-5
-- Rebuild for ocaml-zarith 1.9
-
-* Fri Aug 2 2019 Jerry James <loganjerry(a)gmail.com> - 2.41-4
-- Rebuild for frama-c 19.0
-
-* Sat Jul 27 2019 Fedora Release Engineering <releng(a)fedoraproject.org> - 2.41-4
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild
-
-* Wed Jun 5 2019 Jerry James <loganjerry(a)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(a)fedoraproject.org> - 2.41-2
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild
-
-* Sat Jan 26 2019 Jerry James <loganjerry(a)gmail.com> - 2.41-1
-- New upstream release
-- All patches have been upstreamed; drop them all
-
-* Sat Jul 14 2018 Fedora Release Engineering <releng(a)fedoraproject.org> - 2.40-2
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild
-
-* Mon Feb 12 2018 Jerry James <loganjerry(a)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(a)fedoraproject.org> - 2.39-5
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild
-
-* Thu Jan 18 2018 Igor Gnatenko <ignatenkobrain(a)fedoraproject.org> - 2.39-4
-- Remove obsolete scriptlets
-
-* Sat Dec 9 2017 Jerry James <loganjerry(a)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(a)redhat.com> - 2.39-3
-- OCaml 4.06.0 rebuild.
-
-* Sat Oct 7 2017 Jerry James <loganjerry(a)gmail.com> - 2.39-2
-- Rebuild for why3 0.88.0
-
-* Thu Sep 7 2017 Jerry James <loganjerry(a)gmail.com> - 2.39-1
-- New upstream release
-
-* Wed Sep 06 2017 Richard W.M. Jones <rjones(a)redhat.com> - 2.38-6
-- OCaml 4.05.0 rebuild.
-
-* Thu Aug 03 2017 Fedora Release Engineering <releng(a)fedoraproject.org> - 2.38-5
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_27_Binutils_Mass_Rebuild
-
-* Thu Jul 27 2017 Fedora Release Engineering <releng(a)fedoraproject.org> - 2.38-4
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild
-
-* Sat Jul 01 2017 Richard W.M. Jones <rjones(a)redhat.com> - 2.38-3
-- Rebuild for OCaml 4.04.2.
-
-* Mon May 15 2017 Richard W.M. Jones <rjones(a)redhat.com> - 2.38-2
-- Rebuild for OCaml 4.04.1.
-
-* Fri Mar 24 2017 Jerry James <loganjerry(a)gmail.com> - 2.38-1
-- New upstream release
-
-* Sat Feb 11 2017 Fedora Release Engineering <releng(a)fedoraproject.org> - 2.36-2
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild
-
-* Thu Jan 12 2017 Jerry James <loganjerry(a)gmail.com> - 2.36-1
-- New upstream release
-
-* Wed Nov 30 2016 Jerry James <loganjerry(a)gmail.com> - 2.35-23
-- Rebuild for gappalib-coq 1.3.2
-
-* Sun Nov 06 2016 Richard W.M. Jones <rjones(a)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(a)gmail.com> - 2.35-20
-- Rebuild for coq 8.5pl3
-- Remove obsolete scriptlets
-
-* Thu Sep 29 2016 Jerry James <loganjerry(a)gmail.com> - 2.35-19
-- Rebuild for flocq 2.5.2 and gappalib-coq 1.3.1
-
-* Fri Sep 2 2016 Jerry James <loganjerry(a)gmail.com> - 2.35-18
-- Rebuild for why3 0.87.2
-
-* Fri Jul 22 2016 Jerry James <loganjerry(a)gmail.com> - 2.35-17
-- Rebuild for apron 0.9.11 and gappalib-coq 1.3.0
-
-* Wed Jul 13 2016 Jerry James <loganjerry(a)gmail.com> - 2.35-16
-- Rebuild for coq 8.5pl2
-
-* Wed Jun 1 2016 Jerry James <loganjerry(a)gmail.com> - 2.35-15
-- Rebuild for why3 0.87.1 and Frama-C Aluminium
-
-* Fri Apr 22 2016 Jerry James <loganjerry(a)gmail.com> - 2.35-14
-- Rebuild for coq 8.5pl1
-
-* Sat Apr 16 2016 Jerry James <loganjerry(a)gmail.com> - 2.35-13
-- Rebuild for ocaml-ocamlgraph 1.8.7
-
-* Fri Mar 18 2016 Jerry James <loganjerry(a)gmail.com> - 2.35-12
-- Rebuild for why3 0.87.0
-
-* Fri Feb 12 2016 Jerry James <loganjerry(a)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(a)fedoraproject.org> - 2.35-10
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild
-
-* Wed Oct 14 2015 Jerry James <loganjerry(a)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(a)redhat.com> - 2.35-8
-- OCaml 4.02.3 rebuild.
-
-* Mon Jun 22 2015 Jerry James <loganjerry(a)gmail.com> - 2.35-7
-- Rebuild for why3 0.86.1
-
-* Fri Jun 19 2015 Richard W.M. Jones <rjones(a)redhat.com> - 2.35-6
-- Rebuild for ocaml-4.02.2.
-
-* Fri Jun 19 2015 Fedora Release Engineering <rel-eng(a)lists.fedoraproject.org> -
2.35-5
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_23_Mass_Rebuild
-
-* Sat May 16 2015 Jerry James <loganjerry(a)gmail.com> - 2.35-4
-- Rebuild for why3 0.86
-
-* Mon Apr 13 2015 Jerry James <loganjerry(a)gmail.com> - 2.35-3
-- Rebuild for coq 8.4pl6
-
-* Wed Apr 1 2015 Jerry James <loganjerry(a)gmail.com> - 2.35-2
-- Adjust requires filter
-
-* Tue Mar 31 2015 Jerry James <loganjerry(a)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(a)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(a)redhat.com> - 2.34-17
-- ocaml-4.02.1 rebuild.
-
-* Sat Nov 15 2014 Jerry James <loganjerry(a)gmail.com> - 2.34-16
-- Fix gwhy-2.33.patch (bz 1164470)
-
-* Thu Nov 13 2014 Richard W.M. Jones <rjones(a)redhat.com> - 2.34-15
-- Bump and rebuild for broken dependencies.
-
-* Thu Oct 30 2014 Jerry James <loganjerry(a)gmail.com> - 2.34-14
-- Rebuild for coq 8.4pl5
-
-* Thu Sep 18 2014 Jerry James <loganjerry(a)gmail.com> - 2.34-13
-- Rebuild for why3 0.85
-
-* Mon Sep 8 2014 Jerry James <loganjerry(a)gmail.com> - 2.34-12
-- Rebuild for fixed frama-c
-- Fix license handling
-
-* Tue Sep 2 2014 Jerry James <loganjerry(a)gmail.com> - 2.34-11
-- Rebuild for the final ocaml 4.02.0 release
-
-* Mon Aug 25 2014 Jerry James <loganjerry(a)gmail.com> - 2.34-10
-- ocaml-4.02.0+rc1 rebuild.
-
-* Mon Aug 18 2014 Fedora Release Engineering <rel-eng(a)lists.fedoraproject.org> -
2.34-9
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild
-
-* Mon Aug 4 2014 Jerry James <loganjerry(a)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(a)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(a)lists.fedoraproject.org> -
2.34-6
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild
-
-* Tue May 13 2014 Jerry James <loganjerry(a)gmail.com> - 2.34-5
-- Rebuild for coq 8.4pl4
-
-* Mon Apr 21 2014 Jerry James <loganjerry(a)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(a)redhat.com> - 2.34-3
-- Remove ocaml_arches macro (RHBZ#1087794).
-
-* Mon Mar 24 2014 Jerry James <loganjerry(a)gmail.com> - 2.34-2
-- Remove dropped patches
-- Add icons
-- Fix the desktop icon entries
-
-* Tue Mar 18 2014 Jerry James <loganjerry(a)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(a)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(a)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(a)iki.fi> - 2.33-4
-- Install docs to %%{_pkgdocdir} where available.
-
-* Fri Jun 21 2013 Jerry James <loganjerry(a)gmail.com> - 2.33-3
-- Rebuild for frama-c Fluorine 20130601
-
-* Thu May 23 2013 Jerry James <loganjerry(a)gmail.com> - 2.33-2
-- Rebuild for new frama-c and why3 builds
-
-* Tue May 14 2013 Jerry James <loganjerry(a)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(a)gmail.com> - 2.31-6
-- Rebuild for alt-ergo 0.95
-
-* Mon Jan 7 2013 Jerry James <loganjerry(a)gmail.com> - 2.31-5
-- Rebuild for coq 8.4pl1
-
-* Fri Oct 19 2012 Jerry James <loganjerry(a)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(a)gmail.com> - 2.31-3
-- Rebuild for new frama-c build with altered API.
-
-* Mon Aug 27 2012 Jerry James <loganjerry(a)gmail.com> - 2.31-2
-- Frama-c is fixed; rebuild with the Jessie plugin enabled and functioning
-
-* Thu Aug 23 2012 Jerry James <loganjerry(a)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(a)redhat.com> - 2.30-7
-- Rebuild for OCaml 4.00.0 official.
-
-* Sun Jul 22 2012 Fedora Release Engineering <rel-eng(a)lists.fedoraproject.org> -
2.30-6
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild
-
-* Wed Jan 11 2012 Jerry James <loganjerry(a)gmail.com> - 2.30-5
-- Patch to work with flocq 2.0.0
-
-* Tue Dec 27 2011 Jerry James <loganjerry(a)gmail.com> - 2.30-4
-- Rebuild for coq 8.3pl3
-
-* Tue Dec 6 2011 Jerry James <loganjerry(a)gmail.com> - 2.30-3
-- Update alt_ergo and yices "okay" version numbers
-
-* Wed Nov 23 2011 Jerry James <loganjerry(a)gmail.com> - 2.30-2
-- Rebuild with APRON and gappalib-coq support
-
-* Fri Oct 28 2011 Jerry James <loganjerry(a)gmail.com> - 2.30-1
-- New upstream release
-
-* Thu Jul 14 2011 Jerry James <loganjerry(a)gmail.com> - 2.29-2
-- Fix broken conditionals
-
-* Mon Jul 11 2011 Jerry James <loganjerry(a)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(a)redhat.com> 2.28-2.2
-- add ppc to excludearch, too. No pvs-sbcl available there
-
-* Wed Apr 13 2011 Karsten Hopp <karsten(a)redhat.com> 2.28-2.1
-- add ppc64 to excludearch, no sbcl available there
-
-* Mon Feb 07 2011 Fedora Release Engineering <rel-eng(a)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(a)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(a)gmail.com> - 2.26-2
-- Bump and rebuild for OCaml 3.12.
-
-* Sat Oct 09 2010 David A. Wheeler + Mark Rader <dwheeler(a)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(a)gmail.com> - 2.23-2
-- Rebuild to fix dependencies.
-
-* Fri Jan 08 2010 Alan Dunn <amdunn(a)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(a)ausil.us> - 2.17-5
-- Exclude sparc64 s390 s390x there is no ocaml there
-
-* Fri Aug 07 2009 Alan Dunn <amdunn(a)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(a)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(a)lists.fedoraproject.org> -
2.17-2
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_11_Mass_Rebuild
-
-* Wed Dec 24 2008 Alan Dunn <amdunn(a)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(a)gmail.com> 2.14-2.1
-- ExcludeArch ppc64 on Fedora 8 due to no ocaml.
-* Fri Aug 1 2008 Alan Dunn <amdunn(a)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(a)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(a)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(a)gmail.com> 2.13-1
-- Initial Fedora RPM version.