Compare commits
16 commits
| Author | SHA1 | Date | |
|---|---|---|---|
|
a8d84c45d4 | ||
|
4ea920bebe | ||
|
|
4d6840f782 | ||
|
|
a55ef6338d | ||
|
|
219f4f021b | ||
|
|
ee09cbc085 | ||
|
|
81014a5a53 | ||
|
|
2ff5e9754d | ||
|
|
d626ea5898 | ||
|
|
d4041358df | ||
|
|
6aa1f91c4b | ||
|
|
01dc32708f | ||
|
|
26b175fd32 | ||
|
|
1341b9c9ef | ||
|
|
6472c2a08f | ||
|
|
e3863b543f |
15 changed files with 1 additions and 1548 deletions
6
.gitignore
vendored
6
.gitignore
vendored
|
|
@ -1,6 +0,0 @@
|
|||
/krakatoa.pdf
|
||||
/why-icons.tar.xz
|
||||
/why-2.36.tar.gz
|
||||
/why-2.38.tar.gz
|
||||
/why-2.39.tar.gz
|
||||
/why-2.40.tar.gz
|
||||
|
|
@ -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.
|
||||
|
|
@ -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
1
dead.package
Normal file
|
|
@ -0,0 +1 @@
|
|||
Abandoned by upstream and fails to build from source
|
||||
35
div.pvs
35
div.pvs
|
|
@ -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
|
||||
|
||||
|
|
@ -1,43 +0,0 @@
|
|||
<?xml version="1.0" encoding="UTF-8"?>
|
||||
<component type="desktop">
|
||||
<id>jessie.desktop</id>
|
||||
<metadata_license>CC0-1.0</metadata_license>
|
||||
<project_license>LGPL-2.1</project_license>
|
||||
<name>jessie</name>
|
||||
<summary>Interface between why and Frama-C</summary>
|
||||
<description>
|
||||
<p>
|
||||
Jessie is an interface between why and Frama-C.
|
||||
</p>
|
||||
<p>
|
||||
Why is a software verification platform that applies formal proving tools to
|
||||
annotated programs. The Jessie plugin provide the ability to analyze C
|
||||
programs by invoking Frama-C.
|
||||
</p>
|
||||
</description>
|
||||
<screenshots>
|
||||
<screenshot type="default">
|
||||
<image>http://krakatoa.lri.fr/jessie/max_why3ide.png</image>
|
||||
<caption>Interactive proof session</caption>
|
||||
</screenshot>
|
||||
<screenshot>
|
||||
<image>http://krakatoa.lri.fr/jessie/max_ptr_why3ide.png</image>
|
||||
<caption>Max function proof</caption>
|
||||
</screenshot>
|
||||
<screenshot>
|
||||
<image>http://krakatoa.lri.fr/jessie/binary_search_raw.png</image>
|
||||
<caption>Binary search function proof</caption>
|
||||
</screenshot>
|
||||
<screenshot>
|
||||
<image>http://krakatoa.lri.fr/jessie/binary_search_ovfl.png</image>
|
||||
<caption>Binary search arithmetic overflow</caption>
|
||||
</screenshot>
|
||||
<screenshot>
|
||||
<image>http://krakatoa.lri.fr/jessie/binary_search_behav.png</image>
|
||||
<caption>Binar search function behavior</caption>
|
||||
</screenshot>
|
||||
</screenshots>
|
||||
<update_contact>loganjerry@gmail.com</update_contact>
|
||||
<url type="homepage">http://krakatoa.lri.fr/</url>
|
||||
<url type="bugtracker">https://gforge.inria.fr/tracker/?atid=4012&group_id=999&func=browse</url>
|
||||
</component>
|
||||
|
|
@ -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;
|
||||
|
|
@ -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
35
rem.pvs
|
|
@ -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
3
sources
|
|
@ -1,3 +0,0 @@
|
|||
SHA512 (krakatoa.pdf) = 5d0f4e6b938ddc1eafa48264c02cf99e68f776a7e190b997e35fb2cd154627b5d27369886f570cbcfdfe5f3a1929a97a1fec9457a6f6662f83cbb2e51f65ca04
|
||||
SHA512 (why-2.40.tar.gz) = e99f528ab2a3030c5ed8509ec45e75dc2f3dc2ed92fe1213c2b92a2dc700e2d9c32bc765751b2660cc1f3a6e110b4687a4262779fdae52faaaf144c411712972
|
||||
SHA512 (why-icons.tar.xz) = d6ca78cf09540f5742564912470fb8c49f7d11ca16cd8bb60c8790af10c1591198f6020bd792cff8e3464f762b7ef0a690d3e4ba1a2cf670c286c8056d266bc3
|
||||
596
why-num.patch
596
why-num.patch
|
|
@ -1,596 +0,0 @@
|
|||
--- atp/cooper.ml.orig 2018-01-23 03:07:35.000000000 -0700
|
||||
+++ atp/cooper.ml 2018-02-11 20:48:48.754907226 -0700
|
||||
@@ -38,10 +38,10 @@
|
||||
(* Lift operations up to numerals. *)
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
|
||||
-let mk_numeral n = Fn(string_of_num n,[]);;
|
||||
+let mk_numeral n = Fn(Z.to_string n,[]);;
|
||||
|
||||
let dest_numeral =
|
||||
- function (Fn(ns,[])) -> num_of_string ns
|
||||
+ function (Fn(ns,[])) -> Z.of_string ns
|
||||
| _ -> failwith "dest_numeral";;
|
||||
|
||||
let is_numeral = can dest_numeral;;
|
||||
@@ -59,12 +59,12 @@ let numeral2 fn m n = mk_numeral(fn (des
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
|
||||
let rec linear_cmul n tm =
|
||||
- if n =/ Int 0 then Fn("0",[]) else
|
||||
+ if Z.equal n Z.zero then Fn("0",[]) else
|
||||
match tm with
|
||||
Fn("+",[Fn("*",[c1; x1]); rest]) ->
|
||||
- Fn("+",[Fn("*",[numeral1 (( */ ) n) c1; x1]);
|
||||
+ Fn("+",[Fn("*",[numeral1 (Z.mul n) c1; x1]);
|
||||
linear_cmul n rest])
|
||||
- | k -> numeral1 (( */ ) n) k;;
|
||||
+ | k -> numeral1 (Z.mul n) k;;
|
||||
|
||||
let earlierv vars (Var x) (Var y) = earlier vars x y;;
|
||||
|
||||
@@ -73,7 +73,7 @@ let rec linear_add vars tm1 tm2 =
|
||||
(Fn("+",[Fn("*",[c1; x1]); rest1]),
|
||||
Fn("+",[Fn("*",[c2; x2]); rest2])) ->
|
||||
if x1 = x2 then
|
||||
- let c = numeral2 (+/) c1 c2 in
|
||||
+ let c = numeral2 Z.add c1 c2 in
|
||||
if c = Fn("0",[]) then linear_add vars rest1 rest2
|
||||
else Fn("+",[Fn("*",[c; x1]); linear_add vars rest1 rest2])
|
||||
else if earlierv vars x1 x2 then
|
||||
@@ -84,9 +84,9 @@ let rec linear_add vars tm1 tm2 =
|
||||
Fn("+",[Fn("*",[c1; x1]); linear_add vars rest1 tm2])
|
||||
| (_,Fn("+",[Fn("*",[c2; x2]); rest2])) ->
|
||||
Fn("+",[Fn("*",[c2; x2]); linear_add vars tm1 rest2])
|
||||
- | _ -> numeral2 (+/) tm1 tm2;;
|
||||
+ | _ -> numeral2 Z.add tm1 tm2;;
|
||||
|
||||
-let linear_neg tm = linear_cmul (Int(-1)) tm;;
|
||||
+let linear_neg tm = linear_cmul Z.minus_one tm;;
|
||||
|
||||
let linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2);;
|
||||
|
||||
@@ -116,7 +116,7 @@ let mkatom vars p t = Atom(R(p,[Fn("0",[
|
||||
let linform vars fm =
|
||||
match fm with
|
||||
Atom(R("divides",[c;t])) ->
|
||||
- let c' = mk_numeral(abs_num(dest_numeral c)) in
|
||||
+ let c' = mk_numeral(Z.abs(dest_numeral c)) in
|
||||
Atom(R("divides",[c';lint vars t]))
|
||||
| Atom(R("=",[s;t])) -> mkatom vars "=" (Fn("-",[t;s]))
|
||||
| Atom(R("<",[s;t])) -> mkatom vars "<" (Fn("-",[t;s]))
|
||||
@@ -144,11 +144,11 @@ let rec posineq fm =
|
||||
let rec formlcm x fm =
|
||||
match fm with
|
||||
Atom(R(p,[_;Fn("+",[Fn("*",[c;y]);z])])) when y = x ->
|
||||
- abs_num(dest_numeral c)
|
||||
+ Z.abs(dest_numeral c)
|
||||
| Not(p) -> formlcm x p
|
||||
| And(p,q) -> lcm_num (formlcm x p) (formlcm x q)
|
||||
| Or(p,q) -> lcm_num (formlcm x p) (formlcm x q)
|
||||
- | _ -> Int 1;;
|
||||
+ | _ -> Z.one;;
|
||||
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
(* Adjust all coefficients of x in formula; fold in reduction to +/- 1. *)
|
||||
@@ -157,10 +157,10 @@ let rec formlcm x fm =
|
||||
let rec adjustcoeff x l fm =
|
||||
match fm with
|
||||
Atom(R(p,[d; Fn("+",[Fn("*",[c;y]);z])])) when y = x ->
|
||||
- let m = l // dest_numeral c in
|
||||
- let n = if p = "<" then abs_num(m) else m in
|
||||
- let xtm = Fn("*",[mk_numeral(m // n); x]) in
|
||||
- Atom(R(p,[linear_cmul (abs_num m) d;
|
||||
+ let m = Z.div l (dest_numeral c) in
|
||||
+ let n = if p = "<" then Z.abs(m) else m in
|
||||
+ let xtm = Fn("*",[mk_numeral(Z.div m n); x]) in
|
||||
+ Atom(R(p,[linear_cmul (Z.abs m) d;
|
||||
Fn("+",[xtm; linear_cmul n z])]))
|
||||
| Not(p) -> Not(adjustcoeff x l p)
|
||||
| And(p,q) -> And(adjustcoeff x l p,adjustcoeff x l q)
|
||||
@@ -174,7 +174,7 @@ let rec adjustcoeff x l fm =
|
||||
let unitycoeff x fm =
|
||||
let l = formlcm x fm in
|
||||
let fm' = adjustcoeff x l fm in
|
||||
- if l =/ Int 1 then fm' else
|
||||
+ if Z.equal l Z.one then fm' else
|
||||
let xp = Fn("+",[Fn("*",[Fn("1",[]);x]); Fn("0",[])]) in
|
||||
And(Atom(R("divides",[mk_numeral l; xp])),adjustcoeff x l fm);;
|
||||
|
||||
@@ -204,7 +204,7 @@ let rec divlcm x fm =
|
||||
| Not(p) -> divlcm x p
|
||||
| And(p,q) -> lcm_num (divlcm x p) (divlcm x q)
|
||||
| Or(p,q) -> lcm_num (divlcm x p) (divlcm x q)
|
||||
- | _ -> Int 1;;
|
||||
+ | _ -> Z.one;;
|
||||
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
(* Construct the B-set. *)
|
||||
@@ -242,8 +242,8 @@ let rec linrep vars x t fm =
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
|
||||
let operations =
|
||||
- ["=",(=/); "<",(</); ">",(>/); "<=",(<=/); ">=",(>=/);
|
||||
- "divides",(fun x y -> mod_num y x =/ Int 0)];;
|
||||
+ ["=",(Z.equal); "<",(Z.lt); ">",(Z.gt); "<=",(Z.leq); ">=",(Z.geq);
|
||||
+ "divides",(fun x y -> Z.equal (Z.rem y x) Z.zero)];;
|
||||
|
||||
let evalc_atom at =
|
||||
match at with
|
||||
@@ -265,7 +265,7 @@ let cooper vars fm =
|
||||
let x = Var x0 in
|
||||
let p = unitycoeff x p0 in
|
||||
let p_inf = simplify(minusinf x p) and bs = bset x p
|
||||
- and js = Int 1 --- divlcm x p in
|
||||
+ and js = Z.one --- divlcm x p in
|
||||
let p_element j b =
|
||||
linrep vars x (linear_add vars b (mk_numeral j)) p in
|
||||
let stage j = list_disj
|
||||
--- atp/defcnf.ml.orig 2018-01-23 03:07:35.000000000 -0700
|
||||
+++ atp/defcnf.ml 2018-02-11 14:00:03.159892859 -0700
|
||||
@@ -55,7 +55,7 @@ let rec nenf fm =
|
||||
(* Make a stylized variable and update the index. *)
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
|
||||
-let mkprop n = Atom(P("p_"^(string_of_num n))),n +/ Int 1;;
|
||||
+let mkprop n = Atom(P("p_"^(Z.to_string n))),Z.succ n;;
|
||||
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
(* Make n large enough that "v_m" won't clash with s for any m >= n *)
|
||||
@@ -67,7 +67,7 @@ let max_varindex pfx =
|
||||
let l = String.length s in
|
||||
if l <= m or String.sub s 0 m <> pfx then n else
|
||||
let s' = String.sub s m (l - m) in
|
||||
- if forall numeric (explode s') then max_num n (num_of_string s')
|
||||
+ if forall numeric (explode s') then Z.max n (Z.of_string s')
|
||||
else n;;
|
||||
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
@@ -90,7 +90,7 @@ and defstep op (p,q) (fm,defs,n) =
|
||||
|
||||
let defcnf fm =
|
||||
let fm' = nenf(psimplify fm) in
|
||||
- let n = Int 1 +/ overatoms (max_varindex "p_" ** pname) fm' (Int 0) in
|
||||
+ let n = Z.succ (overatoms (max_varindex "p_" ** pname) fm' Z.zero) in
|
||||
let (fm'',defs,_) = maincnf (fm',undefined,n) in
|
||||
let deflist = map (snd ** snd) (funset defs) in
|
||||
let subcnfs = itlist ((@) ** simpcnf) deflist (simpcnf fm'') in
|
||||
@@ -130,7 +130,7 @@ let rec andcnf (fm,defs,n as trip) =
|
||||
|
||||
let defcnfs fm =
|
||||
let fm' = nenf(psimplify fm) in
|
||||
- let n = Int 1 +/ overatoms (max_varindex "p_" ** pname) fm' (Int 0) in
|
||||
+ let n = Z.succ (overatoms (max_varindex "p_" ** pname) fm' Z.zero) in
|
||||
let (fm'',defs,_) = andcnf (fm',undefined,n) in
|
||||
let deflist = map (snd ** snd) (funset defs) in
|
||||
setify(itlist ((@) ** simpcnf) deflist (simpcnf fm''));;
|
||||
@@ -181,7 +181,7 @@ let rec andcnf pos (fm,defs,n as trip) =
|
||||
|
||||
let defcnfs imps fm =
|
||||
let fm' = nenf(psimplify fm) in
|
||||
- let n = Int 1 +/ overatoms (max_varindex "p_" ** pname) fm' (Int 0) in
|
||||
+ let n = Z.succ (overatoms (max_varindex "p_" ** pname) fm' Z.zero) in
|
||||
let (fm'',defs,_) = andcnf imps (fm',undefined,n) in
|
||||
let deflist = map (snd ** snd) (funset defs) in
|
||||
setify(itlist ((@) ** simpcnf) deflist (simpcnf fm''));;
|
||||
@@ -209,7 +209,7 @@ let rec andcnf3 pos (fm,defs,n as trip)
|
||||
|
||||
let defcnf3s imps fm =
|
||||
let fm' = nenf(psimplify fm) in
|
||||
- let n = Int 1 +/ overatoms (max_varindex "p_" ** pname) fm' (Int 0) in
|
||||
+ let n = Z.succ (overatoms (max_varindex "p_" ** pname) fm' Z.zero) in
|
||||
let (fm'',defs,_) = andcnf3 imps (fm',undefined,n) in
|
||||
let deflist = map (snd ** snd) (funset defs) in
|
||||
setify(itlist ((@) ** simpcnf) deflist (simpcnf fm''));;
|
||||
--- atp/fourier_motzkin.ml.orig 2018-01-23 03:07:35.000000000 -0700
|
||||
+++ atp/fourier_motzkin.ml 2018-02-11 20:34:13.822886848 -0700
|
||||
@@ -71,10 +71,10 @@ let rec posineq fm =
|
||||
let rec adjustcoeff x l fm =
|
||||
match fm with
|
||||
Atom(R(p,[d; Fn("+",[Fn("*",[c;y]);z])])) when y = x ->
|
||||
- let m = l // dest_numeral c in
|
||||
- let n = if p = "<=" then abs_num(m) else m in
|
||||
- let xtm = Fn("*",[mk_numeral(m // n); x]) in
|
||||
- Atom(R(p,[linear_cmul (abs_num m) d;
|
||||
+ let m = Z.div l (dest_numeral c) in
|
||||
+ let n = if p = "<=" then Z.abs(m) else m in
|
||||
+ let xtm = Fn("*",[mk_numeral(Z.div m n); x]) in
|
||||
+ Atom(R(p,[linear_cmul (Z.abs m) d;
|
||||
Fn("+",[xtm; linear_cmul n z])]))
|
||||
| Not(p) -> Not(adjustcoeff x l p)
|
||||
| And(p,q) -> And(adjustcoeff x l p,adjustcoeff x l q)
|
||||
@@ -88,7 +88,7 @@ let rec adjustcoeff x l fm =
|
||||
let unitycoeff x fm =
|
||||
let l = formlcm x fm in
|
||||
let fm' = adjustcoeff x l fm in
|
||||
- if l =/ Int 1 then fm' else
|
||||
+ if Z.equal l Z.one then fm' else
|
||||
adjustcoeff x l fm;;
|
||||
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
@@ -98,10 +98,10 @@ let unitycoeff x fm =
|
||||
let isolate x fm =
|
||||
match fm with
|
||||
Atom(R(p,[_;Fn("+",[Fn("*",[c;y]);z])])) when y = x ->
|
||||
- let c = mk_numeral (Int 0 -/ dest_numeral c) in
|
||||
+ let c = mk_numeral (Z.sub Z.zero (dest_numeral c)) in
|
||||
Atom(R(p,[Fn("*",[c;y]);z]))
|
||||
| Atom(R(p,[zero;Fn("*",[c;y])])) when y = x ->
|
||||
- let c = mk_numeral (Int 0 -/ dest_numeral c) in
|
||||
+ let c = mk_numeral (Z.sub Z.zero (dest_numeral c)) in
|
||||
Atom(R(p,[Fn("*",[c;y]);zero]))
|
||||
| _ ->
|
||||
printer fm;
|
||||
@@ -110,7 +110,7 @@ let isolate x fm =
|
||||
let replace vars x t fm =
|
||||
match fm with
|
||||
Atom(R(p,[Fn("*",[c;y]);z])) when y = x ->
|
||||
- let t = if dest_numeral c >/ Int 0 then t else linear_neg t in
|
||||
+ let t = if Z.gt (dest_numeral c) Z.zero then t else linear_neg t in
|
||||
linform vars (Atom(R(p,[t;z])))
|
||||
| _ -> assert false
|
||||
|
||||
@@ -128,13 +128,13 @@ let fourier vars fm =
|
||||
(function (Atom(R("=",_))) -> true | _ -> false) cjs in
|
||||
let (Atom(R("=",[s;t]))) = eqn in
|
||||
let (Fn("*",[c;_])) = s in
|
||||
- let y = if dest_numeral c =/ Int 1 then t else linear_neg t in
|
||||
+ let y = if Z.equal (dest_numeral c) Z.one then t else linear_neg t in
|
||||
list_conj(map (replace vars x y) (subtract cjs [eqn]))
|
||||
with Failure _ ->
|
||||
let l,r =
|
||||
partition
|
||||
(fun (Atom(R("<=",[Fn("*",[c;_]);t]))) ->
|
||||
- dest_numeral c =/ Int (-1)) cjs
|
||||
+ Z.equal (dest_numeral c) Z.minus_one) cjs
|
||||
in
|
||||
let lefts = map (fun (Atom(R("<=",[_;l]))) -> linear_neg l) l
|
||||
and rights = map (fun (Atom(R("<=",[_;r]))) -> r) r in
|
||||
--- atp/lib.ml.orig 2018-01-23 03:07:35.000000000 -0700
|
||||
+++ atp/lib.ml 2018-02-11 13:26:57.020559495 -0700
|
||||
@@ -46,11 +46,9 @@ let ( ** ) = fun f g x -> f(g x);;
|
||||
(* GCD and LCM on arbitrary-precision numbers. *)
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
|
||||
-let gcd_num n1 n2 =
|
||||
- abs_num(num_of_big_int
|
||||
- (Big_int.gcd_big_int (big_int_of_num n1) (big_int_of_num n2)));;
|
||||
+let gcd_num n1 n2 = Z.gcd n1 n2;;
|
||||
|
||||
-let lcm_num n1 n2 = abs_num(n1 */ n2) // gcd_num n1 n2;;
|
||||
+let lcm_num n1 n2 = Z.lcm n1 n2;;
|
||||
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
(* A useful idiom for "non contradictory" etc. *)
|
||||
@@ -73,7 +71,7 @@ let can f x = try f x; true with Failure
|
||||
|
||||
let rec (--) = fun m n -> if m > n then [] else m::((m + 1) -- n);;
|
||||
|
||||
-let rec (---) = fun m n -> if m >/ n then [] else m::((m +/ Int 1) --- n);;
|
||||
+let rec (---) = fun m n -> if Z.gt m n then [] else m::((Z.succ m) --- n);;
|
||||
|
||||
let rec map2 f l1 l2 =
|
||||
match (l1,l2) with
|
||||
@@ -596,4 +594,4 @@ let equated (Partition f) = dom f;;
|
||||
(* First number starting at n for which p succeeds. *)
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
|
||||
-let rec first n p = if p(n) then n else first (n +/ Int 1) p;;
|
||||
+let rec first n p = if p(n) then n else first (Z.succ n) p;;
|
||||
--- atp/Makefile.orig 2018-01-23 03:07:35.000000000 -0700
|
||||
+++ atp/Makefile 2018-02-11 13:14:15.311777144 -0700
|
||||
@@ -8,6 +8,8 @@
|
||||
# many.ml (Example relevant to many-sorted logic)
|
||||
# hol.ml (Simple higher order logic setup)
|
||||
|
||||
+ZARITHLIB=$(shell ocamlfind query zarith)
|
||||
+
|
||||
#MLFILES = lib.ml intro.ml formulas.ml prop.ml propexamples.ml \
|
||||
defcnf.ml dp.ml stal.ml bdd.ml fol.ml skolem.ml \
|
||||
herbrand.ml unif.ml tableaux.ml resolution.ml prolog.ml \
|
||||
@@ -33,9 +35,9 @@ compiled: example.ml atp.cmx; ocamlopt -
|
||||
|
||||
# Make the appropriate object for the main body of code
|
||||
|
||||
-atp.cmx: atp.ml; ocamlopt -w ax -c atp.ml
|
||||
+atp.cmx: atp.ml; ocamlopt -I $(ZARITHLIB) -w ax -c atp.ml
|
||||
|
||||
-atp.cmo: atp.ml; ocamlc -w ax -c atp.ml
|
||||
+atp.cmo: atp.ml; ocamlc -I $(ZARITHLIB) -w ax -c atp.ml
|
||||
|
||||
# Make the camlp4 quotation expander
|
||||
|
||||
--- atp/make.ml.orig 2018-01-23 03:07:35.000000000 -0700
|
||||
+++ atp/make.ml 2018-02-11 14:37:48.178019612 -0700
|
||||
@@ -44,10 +44,9 @@
|
||||
Gc.set { (Gc.get()) with Gc.stack_limit = 16777216 };; (* Up the stack size *)
|
||||
Format.set_margin 72;; (* Reduce margins *)
|
||||
open Format;; (* Open formatting *)
|
||||
-open Num;; (* Open bignums *)
|
||||
let imperative_assign = (:=);; (* Preserve this *)
|
||||
|
||||
-let print_num n = print_string(string_of_num n);; (* Avoid range limit *)
|
||||
+let print_num n = print_string(Z.to_string n);; (* Avoid range limit *)
|
||||
#install_printer print_num;; (* when printing nums *)
|
||||
|
||||
(* ------------------------------------------------------------------------- *)
|
||||
--- atp/Mk_ml_file.orig 2018-01-23 03:07:35.000000000 -0700
|
||||
+++ atp/Mk_ml_file 2018-02-10 22:01:01.925304810 -0700
|
||||
@@ -1,4 +1,3 @@
|
||||
-echo "open Num;;"
|
||||
echo "open Format;;"
|
||||
|
||||
cat $@ | sed 's/START_INTERACTIVE;;/(\*/' | sed 's/END_INTERACTIVE;;/\*)/'
|
||||
--- jc/jc_annot_inference.ml.orig 2018-02-10 16:03:04.338379961 -0700
|
||||
+++ jc/jc_annot_inference.ml 2018-02-11 13:13:48.313855743 -0700
|
||||
@@ -49,7 +49,6 @@ open Apron
|
||||
open Coeff
|
||||
open Interval
|
||||
open Lincons1
|
||||
-open Num
|
||||
|
||||
|
||||
(*****************************************************************************)
|
||||
@@ -1120,7 +1119,7 @@ let linearize t =
|
||||
try match t#node with
|
||||
| JCTconst c ->
|
||||
begin match c with
|
||||
- | JCCinteger s -> (TermMap.empty, num_of_string s)
|
||||
+ | JCCinteger s -> (TermMap.empty, Z.of_string s)
|
||||
| JCCboolean _ | JCCvoid | JCCnull | JCCreal _ | JCCstring _ ->
|
||||
err ()
|
||||
end
|
||||
@@ -1133,7 +1132,7 @@ let linearize t =
|
||||
(fun vt1 c1 acc ->
|
||||
try
|
||||
let c2 = TermMap.find vt1 coeffs2 in
|
||||
- TermMap.add vt1 (c1 +/ c2) acc
|
||||
+ TermMap.add vt1 (Z.add c1 c2) acc
|
||||
with Not_found -> TermMap.add vt1 c1 acc
|
||||
) coeffs1 TermMap.empty
|
||||
in
|
||||
@@ -1143,55 +1142,55 @@ let linearize t =
|
||||
else TermMap.add vt2 c2 acc
|
||||
) coeffs2 coeffs
|
||||
in
|
||||
- (coeffs, cst1 +/ cst2)
|
||||
+ (coeffs, (Z.add cst1 cst2))
|
||||
| `Bsub ->
|
||||
let coeffs = TermMap.fold
|
||||
(fun vt1 c1 acc ->
|
||||
try
|
||||
let c2 = TermMap.find vt1 coeffs2 in
|
||||
- TermMap.add vt1 (c1 -/ c2) acc
|
||||
+ TermMap.add vt1 (Z.sub c1 c2) acc
|
||||
with Not_found -> TermMap.add vt1 c1 acc
|
||||
) coeffs1 TermMap.empty
|
||||
in
|
||||
let coeffs = TermMap.fold
|
||||
(fun vt2 c2 acc ->
|
||||
if TermMap.mem vt2 coeffs then acc
|
||||
- else TermMap.add vt2 (minus_num c2) acc
|
||||
+ else TermMap.add vt2 (Z.neg c2) acc
|
||||
) coeffs2 coeffs
|
||||
in
|
||||
- (coeffs, cst1 -/ cst2)
|
||||
+ (coeffs, (Z.sub cst1 cst2))
|
||||
| `Bmul when TermMap.is_empty coeffs1 || TermMap.is_empty coeffs2 ->
|
||||
let coeffs =
|
||||
if TermMap.is_empty coeffs1 then
|
||||
- TermMap.map (fun c -> c */ cst1) coeffs2
|
||||
+ TermMap.map (fun c -> Z.mul c cst1) coeffs2
|
||||
else
|
||||
- TermMap.map (fun c -> c */ cst2) coeffs1
|
||||
+ TermMap.map (fun c -> Z.mul c cst2) coeffs1
|
||||
in
|
||||
- (coeffs, cst1 */ cst2)
|
||||
+ (coeffs, (Z.mul cst1 cst2))
|
||||
| `Bmul
|
||||
| `Bdiv
|
||||
| `Bmod -> err ()
|
||||
end
|
||||
| JCTbinary(t1,(#bitwise_op as bop,`Integer),t2) ->
|
||||
let coeffs1, cst1 = aux t1 in
|
||||
- if coeffs1 = TermMap.empty && cst1 =/ Int 0 then
|
||||
+ if coeffs1 = TermMap.empty && Z.equal cst1 Z.zero then
|
||||
match bop with
|
||||
| `Bbw_and
|
||||
| `Bshift_left
|
||||
| `Blogical_shift_right
|
||||
- | `Barith_shift_right -> TermMap.empty, Int 0
|
||||
+ | `Barith_shift_right -> TermMap.empty, Z.zero
|
||||
| `Bbw_or
|
||||
| `Bbw_xor -> aux t2
|
||||
| _ -> err ()
|
||||
else
|
||||
(* Consider non-linear term as abstract variable. *)
|
||||
- (TermMap.add t (Int 1) TermMap.empty, Int 0)
|
||||
+ (TermMap.add t Z.one TermMap.empty, Z.zero)
|
||||
| JCTunary((uop,`Integer),t1) ->
|
||||
let coeffs1,cst1 = aux t1 in
|
||||
begin match uop with
|
||||
| `Uminus ->
|
||||
- let coeffs = TermMap.map (fun c -> minus_num c) coeffs1 in
|
||||
- (coeffs, minus_num cst1)
|
||||
+ let coeffs = TermMap.map (fun c -> Z.neg c) coeffs1 in
|
||||
+ (coeffs, Z.neg cst1)
|
||||
| _ -> err ()
|
||||
end
|
||||
| JCTvar _ | JCTderef _ | JCToffset _ | JCTapp _ | JCTbinary _
|
||||
@@ -1201,13 +1200,16 @@ let linearize t =
|
||||
| JCTrange _ | JCTif _ | JCTlet _ ->
|
||||
err ()
|
||||
with Failure "linearize" ->
|
||||
- (TermMap.add t (Int 1) TermMap.empty, Int 0)
|
||||
+ (TermMap.add t Z.one TermMap.empty, Z.zero)
|
||||
in aux t
|
||||
|
||||
let linstr_of_term env t =
|
||||
+(*
|
||||
let mkmulstr = function
|
||||
- | (_va, Int 0) -> ""
|
||||
- | (va, c) -> string_of_num c ^ " * " ^ va
|
||||
+ | (_va, Z.zero) -> ""
|
||||
+ | (va, c) -> (Z.to_string c) ^ " * " ^ va
|
||||
+*)
|
||||
+ let mkmulstr = (fun (va,c) -> if Z.equal Z.zero c then "" else (Z.to_string c) ^ " * " ^ va)
|
||||
in
|
||||
let rec mkaddstr = function
|
||||
| [] -> ""
|
||||
@@ -1286,33 +1288,33 @@ let rec linstr_of_assertion env a =
|
||||
in
|
||||
let env,str,cst = linstr_of_term env subt in
|
||||
if str = "" then
|
||||
- let ncst = minus_num cst in
|
||||
+ let ncst = Z.neg cst in
|
||||
let is_true = match bop with
|
||||
- | `Blt -> Int 0 </ ncst
|
||||
- | `Bgt -> Int 0 >/ ncst
|
||||
- | `Ble -> Int 0 <=/ ncst
|
||||
- | `Bge -> Int 0 >=/ ncst
|
||||
- | `Beq -> Int 0 =/ ncst
|
||||
- | `Bneq -> Int 0 <>/ ncst
|
||||
+ | `Blt -> Z.lt Z.zero ncst
|
||||
+ | `Bgt -> Z.gt Z.zero ncst
|
||||
+ | `Ble -> Z.leq Z.zero ncst
|
||||
+ | `Bge -> Z.geq Z.zero ncst
|
||||
+ | `Beq -> Z.equal Z.zero ncst
|
||||
+ | `Bneq -> not (Z.equal Z.zero ncst)
|
||||
in
|
||||
env, if is_true then Dnf.true_ else Dnf.false_
|
||||
else
|
||||
- let cstr = string_of_num (minus_num cst) in
|
||||
+ let cstr = Z.to_string (Z.neg cst) in
|
||||
(* Do not use < and > with APRON, due to bugs in some versions.
|
||||
Convert to equivalent non-strict. *)
|
||||
let str = match bop with
|
||||
| `Blt -> [[str ^ " <= " ^
|
||||
- (string_of_num (pred_num (minus_num cst)))]]
|
||||
+ (Z.to_string (Z.pred (Z.neg cst)))]]
|
||||
| `Bgt -> [[str ^ " >= " ^
|
||||
- (string_of_num (succ_num (minus_num cst)))]]
|
||||
+ (Z.to_string (Z.succ (Z.neg cst)))]]
|
||||
| `Ble -> [[str ^ " <= " ^ cstr]]
|
||||
| `Bge -> [[str ^ " >= " ^ cstr]]
|
||||
| `Beq -> [[str ^ " = " ^ cstr]]
|
||||
| `Bneq ->
|
||||
[[str ^ " <= " ^
|
||||
- (string_of_num (pred_num (minus_num cst)))];
|
||||
+ (Z.to_string (Z.pred (Z.neg cst)))];
|
||||
[str ^ " >= " ^
|
||||
- (string_of_num (succ_num (minus_num cst)))]]
|
||||
+ (Z.to_string (Z.succ (Z.neg cst)))]]
|
||||
in
|
||||
env, str
|
||||
| JCAnot a ->
|
||||
@@ -1330,8 +1332,8 @@ let rec linstr_of_assertion env a =
|
||||
let linstr_of_expr env e =
|
||||
match Jc_effect.term_of_expr e with None -> None | Some t ->
|
||||
let env,str,cst = linstr_of_term env t in
|
||||
- if str = "" then Some (env, string_of_num cst)
|
||||
- else Some (env, str ^ " + " ^ (string_of_num cst))
|
||||
+ if str = "" then Some (env, Z.to_string cst)
|
||||
+ else Some (env, str ^ " + " ^ (Z.to_string cst))
|
||||
|
||||
let offset_linstr_of_expr env ok e =
|
||||
match e#node with
|
||||
@@ -1340,15 +1342,15 @@ let offset_linstr_of_expr env ok e =
|
||||
else
|
||||
begin match Jc_effect.term_of_expr e with None -> None | Some t ->
|
||||
let env,str,cst = linstr_of_term env t in
|
||||
- if str = "" then Some (env,string_of_num cst)
|
||||
- else Some (env,str ^ " + " ^ (string_of_num cst))
|
||||
+ if str = "" then Some (env,Z.to_string cst)
|
||||
+ else Some (env,str ^ " + " ^ (Z.to_string cst))
|
||||
end
|
||||
| _ ->
|
||||
if is_nonnull_pointer_type e#typ then
|
||||
match Jc_effect.term_of_expr e with None -> None | Some t ->
|
||||
let env,str,cst = offset_linstr_of_term env ok t in
|
||||
- if str = "" then Some (env,string_of_num cst)
|
||||
- else Some (env,str ^ " + " ^ (string_of_num cst))
|
||||
+ if str = "" then Some (env,Z.to_string cst)
|
||||
+ else Some (env,str ^ " + " ^ (Z.to_string cst))
|
||||
else None
|
||||
|
||||
|
||||
@@ -1419,13 +1421,13 @@ let mkassertion lincons =
|
||||
|
||||
let rec linterms_of_term t =
|
||||
let mkmulterm (t,c) =
|
||||
- if c =/ Int 0 then None
|
||||
- else if c =/ Int 1 then Some t
|
||||
- else if c =/ Int (-1) then
|
||||
+ if Z.equal c Z.zero then None
|
||||
+ else if Z.equal c Z.one then Some t
|
||||
+ else if Z.equal c Z.minus_one then
|
||||
Some(new term ~typ:integer_type (JCTunary((`Uminus,`Integer),t)))
|
||||
else
|
||||
let c =
|
||||
- new term ~typ:integer_type (JCTconst(JCCinteger(string_of_num c)))
|
||||
+ new term ~typ:integer_type (JCTconst(JCCinteger(Z.to_string c)))
|
||||
in
|
||||
Some(new term ~typ:integer_type (JCTbinary(c,(`Bmul,`Integer),t)))
|
||||
in
|
||||
@@ -1443,30 +1445,30 @@ let rec linterms_of_term t =
|
||||
let coeffs,cst = linearize t in
|
||||
let posl,negl =
|
||||
TermMap.fold (fun t c (pl,nl) ->
|
||||
- if c >/ Int 0 then (t,c) :: pl, nl
|
||||
- else if c </ Int 0 then pl, (t,minus_num c) :: nl
|
||||
+ if Z.gt c Z.zero then (t,c) :: pl, nl
|
||||
+ else if Z.lt c Z.zero then pl, (t,Z.neg c) :: nl
|
||||
else pl, nl
|
||||
) coeffs ([],[])
|
||||
in
|
||||
let cstt =
|
||||
new term ~typ:integer_type
|
||||
- (JCTconst(JCCinteger(string_of_num(abs_num cst))))
|
||||
+ (JCTconst(JCCinteger(Z.to_string(Z.abs cst))))
|
||||
in
|
||||
let post = match mkaddterm posl with
|
||||
| None ->
|
||||
- if cst >/ Int 0 then cstt
|
||||
+ if Z.gt cst Z.zero then cstt
|
||||
else new term ~typ:integer_type (JCTconst(JCCinteger "0"))
|
||||
| Some t ->
|
||||
- if cst >/ Int 0 then
|
||||
+ if Z.gt cst Z.zero then
|
||||
new term ~typ:integer_type (JCTbinary(t,(`Badd,`Integer),cstt))
|
||||
else t
|
||||
in
|
||||
let negt = match mkaddterm negl with
|
||||
| None ->
|
||||
- if cst </ Int 0 then cstt
|
||||
+ if Z.lt cst Z.zero then cstt
|
||||
else new term ~typ:integer_type (JCTconst(JCCinteger "0"))
|
||||
| Some t ->
|
||||
- if cst </ Int 0 then
|
||||
+ if Z.lt cst Z.zero then
|
||||
new term ~typ:integer_type (JCTbinary(t,(`Badd,`Integer),cstt))
|
||||
else t
|
||||
in
|
||||
@@ -1518,8 +1520,8 @@ let mkconsistent a =
|
||||
let posl,negl =
|
||||
TermMap.fold
|
||||
(fun t c (pl,nl) ->
|
||||
- if c >/ Int 0 then t :: pl, nl
|
||||
- else if c </ Int 0 then pl, t :: nl
|
||||
+ if Z.gt c Z.zero then t :: pl, nl
|
||||
+ else if Z.lt c Z.zero then pl, t :: nl
|
||||
else pl, nl
|
||||
) coeffs ([],[])
|
||||
in
|
||||
@@ -2497,10 +2499,10 @@ let collect_expr_targets e =
|
||||
let collect_integer_overflow ei e1 =
|
||||
match Jc_effect.term_of_expr e1 with None -> [] | Some t1 ->
|
||||
let mint = new term ~typ:integer_type
|
||||
- (JCTconst (JCCinteger (Num.string_of_num ei.jc_enum_info_min)))
|
||||
+ (JCTconst (JCCinteger (Z.to_string ei.jc_enum_info_min)))
|
||||
in
|
||||
let maxt = new term ~typ:integer_type
|
||||
- (JCTconst(JCCinteger (Num.string_of_num ei.jc_enum_info_max)))
|
||||
+ (JCTconst(JCCinteger (Z.to_string ei.jc_enum_info_max)))
|
||||
in
|
||||
let mina = new assertion (JCArelation (mint, (`Ble,`Integer), t1)) in
|
||||
let maxa = new assertion (JCArelation (t1, (`Ble,`Integer), maxt)) in
|
||||
|
|
@ -1,11 +0,0 @@
|
|||
--- Makefile.in.orig 2018-02-10 15:44:26.226883183 -0700
|
||||
+++ Makefile.in 2018-02-12 19:34:20.930490137 -0700
|
||||
@@ -214,7 +214,7 @@ jc/jc.cmx jc/jc.o: $(JCCMX_EXPORT)
|
||||
# ppc: jc/jc.cmi jc/jc.cmo jc/jc.cmx
|
||||
|
||||
bin/jessie.opt: $(JCCMX)
|
||||
- $(if $(QUIET),@echo 'Linking $@' &&) $(OCAMLOPT) $(OFLAGS) $(APRONLIB) $(APRONLIBS) $(ATPLIB) -o $@ \
|
||||
+ $(if $(QUIET),@echo 'Linking $@' &&) $(OCAMLOPT) -runtime-variant _pic $(OFLAGS) $(APRONLIB) $(APRONLIBS) $(ATPLIB) -o $@ \
|
||||
unix.cmxa str.cmxa zarith.cmxa graph.cmxa $^
|
||||
$(STRIP) $@
|
||||
|
||||
|
|
@ -1,115 +0,0 @@
|
|||
--- Makefile.in.orig 2018-01-23 03:07:35.000000000 -0700
|
||||
+++ Makefile.in 2018-02-10 15:44:26.226883183 -0700
|
||||
@@ -155,7 +155,7 @@ CMO_EXPORT = src/lib.cmo src/rc.cmo src
|
||||
src/effect.cmo src/pp.cmo src/option_misc.cmo \
|
||||
src/report.cmo \
|
||||
src/explain.cmo \
|
||||
- src/xml.cmo src/project.cmo
|
||||
+ src/xml.cmo src/whyproject.cmo
|
||||
|
||||
# jessie
|
||||
JCCML_EXPORT = src/why3_kw.ml jc/output.ml \
|
||||
--- src/options.mli.orig 2018-01-23 03:07:35.000000000 -0700
|
||||
+++ src/options.mli 2018-02-10 15:44:26.258883112 -0700
|
||||
@@ -184,7 +184,7 @@ val files : string list
|
||||
(*s GUI? *)
|
||||
|
||||
val gui : bool ref
|
||||
-val gui_project : Project.t option ref
|
||||
+val gui_project : Whyproject.t option ref
|
||||
val lib_files_to_load : string list
|
||||
|
||||
(*
|
||||
--- src/pretty.ml.orig 2018-01-23 03:07:35.000000000 -0700
|
||||
+++ src/pretty.ml 2018-02-10 15:44:26.259883110 -0700
|
||||
@@ -416,12 +416,12 @@ let output_project f =
|
||||
with Not_found ->
|
||||
functions := SMap.add fn SMap.empty !functions)
|
||||
Util.program_locs ;
|
||||
- let p = Project.create (Filename.basename f) in
|
||||
- Project.set_project_context_file p (f ^ "_ctx.why");
|
||||
+ let p = Whyproject.create (Filename.basename f) in
|
||||
+ Whyproject.set_project_context_file p (f ^ "_ctx.why");
|
||||
List.iter
|
||||
(fun (expl,fpo) ->
|
||||
let n = expl.lemma_or_fun_name in
|
||||
- let _ = Project.add_lemma p n expl fpo in ())
|
||||
+ let _ = Whyproject.add_lemma p n expl fpo in ())
|
||||
!lemmas;
|
||||
SMap.iter
|
||||
(fun fname behs ->
|
||||
@@ -431,15 +431,15 @@ let output_project f =
|
||||
floc
|
||||
with Not_found -> Loc.dummy_floc
|
||||
in
|
||||
- let f = Project.add_function p fname floc in
|
||||
+ let f = Whyproject.add_function p fname floc in
|
||||
SMap.iter
|
||||
(fun beh vcs ->
|
||||
- let be = Project.add_behavior f beh floc in
|
||||
+ let be = Whyproject.add_behavior f beh floc in
|
||||
List.iter
|
||||
(fun (expl,fpo) ->
|
||||
- let _ = Project.add_goal be expl fpo in ())
|
||||
+ let _ = Whyproject.add_goal be expl fpo in ())
|
||||
vcs)
|
||||
behs)
|
||||
!functions;
|
||||
- Project.save p f;
|
||||
+ Whyproject.save p f;
|
||||
p
|
||||
--- src/pretty.mli.orig 2018-01-23 03:07:35.000000000 -0700
|
||||
+++ src/pretty.mli 2018-02-10 15:44:26.259883110 -0700
|
||||
@@ -50,4 +50,4 @@ val output_files : string -> unit
|
||||
(* [output_project f] produces a whole project description, in a file
|
||||
[f.wpr], together with other needed files [f_ctx.why], [f_lemmas.why],
|
||||
and each goal in a separate file [f_po<i>.why] for i=1,2,... *)
|
||||
-val output_project : string -> Project.t
|
||||
+val output_project : string -> Whyproject.t
|
||||
--- src/whyweb.ml.orig 2018-01-23 03:07:35.000000000 -0700
|
||||
+++ src/whyweb.ml 2018-02-10 15:44:26.259883110 -0700
|
||||
@@ -29,7 +29,7 @@
|
||||
(**************************************************************************)
|
||||
|
||||
open Format
|
||||
-open Project
|
||||
+open Whyproject
|
||||
|
||||
(*prover*)
|
||||
let provers = [Ergo ; Simplify ; Z3 ; Yices ; Cvc3]
|
||||
@@ -168,7 +168,7 @@ let file = match !file with
|
||||
| None -> ()
|
||||
| Some f -> Arg.usage spec usage; exit 1
|
||||
|
||||
-let proj = ref (Project.create "")
|
||||
+let proj = ref (Whyproject.create "")
|
||||
|
||||
let proj_file = ref ""
|
||||
|
||||
@@ -260,7 +260,7 @@ let interp_com c =
|
||||
let _ = Thread.create (launch_behavior Cvc3) b in ()
|
||||
| `LaunchCvc3Function f ->
|
||||
let _ = Thread.create (launch_function Cvc3) f in ()
|
||||
- | `Save -> Project.save !proj !proj.project_name
|
||||
+ | `Save -> Whyproject.save !proj !proj.project_name
|
||||
end;
|
||||
loc
|
||||
with Not_found -> ("",0,0,0)
|
||||
@@ -343,7 +343,7 @@ let main_page msg =
|
||||
let load_prj file =
|
||||
eprintf "Reading file %s@." file;
|
||||
try
|
||||
- proj := Project.load file;
|
||||
+ proj := Whyproject.load file;
|
||||
proj_file := file;
|
||||
with
|
||||
Sys_error _ ->
|
||||
@@ -526,7 +526,7 @@ wprint "<center><a href=\"%s\">Save Proj
|
||||
<table border=\"1\" cellpadding=\"0\" cellspacing=\"0\">" ns;
|
||||
wprint "<tr><th></th>";
|
||||
List.iter (fun prover ->
|
||||
- wprint "<th>%s</th>" (Project.provers_name prover))
|
||||
+ wprint "<th>%s</th>" (Whyproject.provers_name prover))
|
||||
provers;
|
||||
wprint "</tr>
|
||||
";
|
||||
|
|
@ -1,19 +0,0 @@
|
|||
--- jc/jc_annot_inference.ml.orig 2018-01-23 03:07:35.000000000 -0700
|
||||
+++ jc/jc_annot_inference.ml 2018-02-10 16:03:04.338379961 -0700
|
||||
@@ -212,14 +212,14 @@ let name_of_term t =
|
||||
Format.fprintf str_formatter "%a" Jc_output.term t;
|
||||
let s = Format.flush_str_formatter () in
|
||||
let s = filter_alphanumeric s in
|
||||
- "T" ^ unique_term_name t s
|
||||
+ "T" ^ unique_term_name t (Bytes.to_string s)
|
||||
|
||||
let name_of_assertion a =
|
||||
ignore (Format.flush_str_formatter ());
|
||||
Format.fprintf str_formatter "%a" Jc_output.assertion a;
|
||||
let s = Format.flush_str_formatter () in
|
||||
let s = filter_alphanumeric s in
|
||||
- "A" ^ unique_assertion_name a s
|
||||
+ "A" ^ unique_assertion_name a (Bytes.to_string s)
|
||||
|
||||
(* support of <new> (Nicolas) *)
|
||||
let rec destruct_alloc t =
|
||||
605
why.spec
605
why.spec
|
|
@ -1,605 +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.40
|
||||
Release: 2%{?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
|
||||
# Avoid a clash between Frama-C and why modules both named "Project".
|
||||
# Sent upstream 26 Jun 2014.
|
||||
Patch0: %{name}-project.patch
|
||||
# Adapt to the safe string feature of ocaml 4.06
|
||||
Patch1: %{name}-safe-string.patch
|
||||
# Adapt to ocaml 4.06 in general
|
||||
Patch2: %{name}-ocaml-4.06.patch
|
||||
# Finish an incomplete Num to zarith conversion
|
||||
Patch3: %{name}-num.patch
|
||||
|
||||
BuildRequires: auto-destdir
|
||||
BuildRequires: desktop-file-utils
|
||||
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
|
||||
%patch1
|
||||
%patch2
|
||||
%patch3
|
||||
|
||||
# The other part of avoiding the "Project" module name clash
|
||||
mv src/project.ml src/whyproject.ml
|
||||
mv src/project.mli src/whyproject.mli
|
||||
|
||||
cp -p %SOURCE2 ./
|
||||
|
||||
# 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|" \
|
||||
-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
|
||||
|
||||
%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/
|
||||
cp -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} %{SOURCE3} CHANGES README Version %{buildroot}%{why_doc_dir}
|
||||
|
||||
%check
|
||||
make check
|
||||
|
||||
%files
|
||||
%doc README.why-coq.Fedora
|
||||
%license COPYING LICENSE
|
||||
%{_bindir}/*
|
||||
%{_libdir}/why/
|
||||
%{_datadir}/icons/hicolor/*/apps/%{name}.png
|
||||
%{why_doc_dir}/
|
||||
# why-jessie
|
||||
%exclude %{_bindir}/jessie
|
||||
# why-pvs-support:
|
||||
%exclude %{_bindir}/patch_jessie_pvs
|
||||
|
||||
%files jessie
|
||||
%{_bindir}/jessie
|
||||
%{_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
|
||||
* 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.
|
||||
Loading…
Add table
Add a link
Reference in a new issue