rpms/why
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Compare commits

merge into: rpms:rawhide
Branches Tags
rpms:rawhide
rpms:f31
rpms:main
rpms:f32
rpms:f30
rpms:f29
rpms:f28
rpms:f26
rpms:f27
rpms:f25
rpms:f24
rpms:f23
rpms:f22
rpms:f21
rpms:f20
rpms:f19
rpms:f18
rpms:f16
rpms:f17
rpms:f15
rpms:f13
rpms:f14
rpms:f11
rpms:f9
rpms:f10
rpms:f12
rpms:f8
rpms:why-2_23-2_fc13
rpms:F-13-start
rpms:F-13-split
rpms:why-2_23-1_fc11
rpms:why-2_23-1_fc12
rpms:why-2_23-1_fc13
rpms:why-2_17-5_fc12
rpms:F-12-start
rpms:F-12-split
rpms:why-2_17-4_fc12
rpms:why-2_17-3_fc12
rpms:why-2_17-2_fc11
rpms:F-11-start
rpms:F-11-split
rpms:why-2_17-1_fc9
rpms:why-2_17-1_fc10
rpms:why-2_17-1_fc11
rpms:why-2_14-2_fc8_1
rpms:why-2_14-2_fc9
rpms:why-2_14-2_fc10
rpms:F-10-start
rpms:F-10-split
rpms:F-9-start
rpms:F-9-split
rpms:F-8-start
rpms:F-8-split
...
pull from: rpms:f32
Branches Tags
rpms:f31
rpms:main
rpms:rawhide
rpms:f32
rpms:f30
rpms:f29
rpms:f28
rpms:f26
rpms:f27
rpms:f25
rpms:f24
rpms:f23
rpms:f22
rpms:f21
rpms:f20
rpms:f19
rpms:f18
rpms:f16
rpms:f17
rpms:f15
rpms:f13
rpms:f14
rpms:f11
rpms:f9
rpms:f10
rpms:f12
rpms:f8
rpms:why-2_23-2_fc13
rpms:F-13-start
rpms:F-13-split
rpms:why-2_23-1_fc11
rpms:why-2_23-1_fc12
rpms:why-2_23-1_fc13
rpms:why-2_17-5_fc12
rpms:F-12-start
rpms:F-12-split
rpms:why-2_17-4_fc12
rpms:why-2_17-3_fc12
rpms:why-2_17-2_fc11
rpms:F-11-start
rpms:F-11-split
rpms:why-2_17-1_fc9
rpms:why-2_17-1_fc10
rpms:why-2_17-1_fc11
rpms:why-2_14-2_fc8_1
rpms:why-2_14-2_fc9
rpms:why-2_14-2_fc10
rpms:F-10-start
rpms:F-10-split
rpms:F-9-start
rpms:F-9-split
rpms:F-8-start
rpms:F-8-split
Sign in to create a new pull request.

1 commit
rawhide ... f32

Author SHA1 Message Date
Jerry James
f459c5f17d Abandoned by upstream and fails to build from source 2020-03-30 08:50:55 -06:00
13 changed files with 1 additions and 1669 deletions
Download patch file Download diff file Expand all files Collapse all files

3
.gitignore vendored
View file

@ -1,3 +0,0 @@
/krakatoa.pdf
/why-icons.tar.xz
/why-*.tar.gz

8
README.why
View file

@ -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.

6
README.why-coq.Fedora
View file

@ -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.

1
dead.package Normal file
View file

@ -0,0 +1 @@
Abandoned by upstream and fails to build from source

35
div.pvs
View file

@ -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

43
jessie.appdata.xml
View file

@ -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&amp;group_id=999&amp;func=browse</url>
</component>

7
jessie.desktop
View file

@ -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;

59
patch_jessie_pvs
View file

@ -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

35
rem.pvs
View file

@ -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

3
sources
View file

@ -1,3 +0,0 @@
SHA512 (krakatoa.pdf) = 5d0f4e6b938ddc1eafa48264c02cf99e68f776a7e190b997e35fb2cd154627b5d27369886f570cbcfdfe5f3a1929a97a1fec9457a6f6662f83cbb2e51f65ca04
SHA512 (why-2.41.tar.gz) = 2e31ed2642a29ecbbc05954f2aa5c841befa68959f571bcde134a56639cec49a51351e5c7781a1a50fc531f2111b5649c710fa3e60c0f71f222b192d8c41cc86
SHA512 (why-icons.tar.xz) = d6ca78cf09540f5742564912470fb8c49f7d11ca16cd8bb60c8790af10c1591198f6020bd792cff8e3464f762b7ef0a690d3e4ba1a2cf670c286c8056d266bc3

809
why-frama-c.patch
View file

@ -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 =

27
why.rpmlintrc
View file

@ -1,27 +0,0 @@
# THIS FILE IS FOR WHITELISTING RPMLINT ERRORS AND WARNINGS IN TASKOTRON
# https://fedoraproject.org/wiki/Taskotron/Tasks/dist.rpmlint#Whitelisting_errors
# The dictionary lacks some technical words
addFilter(r'W: spelling-error .* (frama|provers)')
# Caused by ocaml; this package cannot fix it
addFilter(r'why[^:]+: E: missing-call-to-chdir-with-chroot')
# Oh yes, we have no manual page
addFilter(r'W: no-manual-page-for-binary (jessie|krakatoa|patch_jessie_pvs)')
# Indeed there is no documentation
addFilter(r'why.[^:]+: W: no-documentation')
addFilter(r'why-(jessie|pvs-support).[^:]*: W: no-documentation')
# This is a devel package
addFilter(r'why-jessie\.[^:]+: W: devel-file-in-non-devel-package')
# PVS creates, and requires, hidden files
addFilter(r'why-pvs-support\.[^:]+: W: hidden-file-or-dir .*\.pvscontext')
# This package has no binary bits
addFilter(r'why-pvs-support\.[^:]+: W: only-non-binary-in-usr-lib')
# The icons were created by the Fedora packager; there is no URL
addFilter(r'why\.spec: W: invalid-url Source[^:]+: why-icons\.tar\.xz')

634
why.spec
View file

@ -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@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.