rpms/why/F-12 gwhy-2.23.patch, NONE, 1.1 why-2.23-Makefile.in.patch, NONE, 1.1 .cvsignore, 1.3, 1.4 caduceus.ps, 1.1, 1.2 import.log, 1.3, 1.4 min_why.why.result, 1.1, 1.2 sources, 1.3, 1.4 why.spec, 1.6, 1.7 gwhy-2.17.patch, 1.1, NONE why-2.17-Makefile.in.patch, 1.1, NONE why-config.patch, 1.1, NONE

Alan Dunn amdunn at fedoraproject.org
Fri Jan 8 20:09:45 UTC 2010


Author: amdunn

Update of /cvs/pkgs/rpms/why/F-12
In directory cvs1.fedora.phx.redhat.com:/tmp/cvs-serv18825/F-12

Modified Files:
	.cvsignore caduceus.ps import.log min_why.why.result sources 
	why.spec 
Added Files:
	gwhy-2.23.patch why-2.23-Makefile.in.patch 
Removed Files:
	gwhy-2.17.patch why-2.17-Makefile.in.patch why-config.patch 
Log Message:
- Upgrade to uptream 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
VS: ----------------------------------------------------------------------


gwhy-2.23.patch:
 gwhy.sh |   27 ++++++++++++++++++---------
 1 file changed, 18 insertions(+), 9 deletions(-)

--- NEW FILE gwhy-2.23.patch ---
--- why-2.23-old/bin/gwhy.sh	2010-01-04 21:08:50.401993553 -0500
+++ why-2.23/bin/gwhy.sh	2010-01-05 08:31:05.989807947 -0500
@@ -1,11 +1,17 @@
 #!/bin/sh
 
-case $1 in
+if ! test $1; then
+file=`zenity --file-selection --title="Select the file you want to open with gwhy"`;
+else
+file=$1
+fi
+
+case $file in
   *.java)
-	b=`basename $1 .java`
-	krakatoa $1 || exit 1
+	b=`basename $file .java`
+	krakatoa $file || exit 1
 	echo "krakatoa on $b.java done"
-        d=`dirname $1`
+        d=`dirname $file`
         echo "cd $d"
         cd $d
 	jessie -locs $b.jloc -why-opt -split-user-conj $b.jc || exit 2
@@ -13,20 +19,23 @@
 	make -f $b.makefile gui
 	;;
   *.c)
-	b=`basename $1 .c`
-	caduceus -why-opt -split-user-conj $1 || exit 1
+	b=`basename $file .c`
+	caduceus -why-opt -split-user-conj $b.c || exit 1
 	make -f $b.makefile gui
 	;;
   *.jc)
-	b=`basename $1 .jc`
+	b=`basename $file .jc`
 	jessie -why-opt -split-user-conj $b.jc || exit 1
 	make -f $b.makefile gui
 	;;
   *.mlw|*.why)
-	gwhy-bin -split-user-conj $1
+	gwhy-bin -split-user-conj $file
+	;;
+  ?*)
+	echo "$file does not have file type extension recognized by gwhy"
 	;;
   *)
-	echo "don't know what to do with $1"
+	echo "gwhy needs the name of a file to inspect in order to run"
 esac
 
 

why-2.23-Makefile.in.patch:
 Makefile.in |   29 ++++++++++++++++-------------
 1 file changed, 16 insertions(+), 13 deletions(-)

--- NEW FILE why-2.23-Makefile.in.patch ---
--- why-2.23-old/Makefile.in	2010-01-04 21:08:49.858843630 -0500
+++ why-2.23/Makefile.in	2010-01-05 20:34:20.912391080 -0500
@@ -650,14 +650,23 @@
 bin/cadlog.opt: src/version.cmx c/cversion.cmx tools/cadlog.cmx
 	$(OCAMLOPT) unix.cmxa -o $@ $^
 
+ifeq ($(OCAMLBEST), opt)
+MAKE_FLOAT_MODEL = tools/make_float_model.opt
+else
+MAKE_FLOAT_MODEL = tools/make_float_model.byte
+endif
+
+tools/make_float_model.byte: tools/make_float_model.cmo
+	$(OCAMLC) -o $@ $^
+
 tools/make_float_model.opt: tools/make_float_model.cmx
 	$(OCAMLOPT) -o $@ $^
 
-lib/why/double_model.why lib/why/double_strict.why: tools/make_float_model.opt
-	tools/make_float_model.opt double 53 -1074
+lib/why/double_model.why lib/why/double_strict.why: $(MAKE_FLOAT_MODEL)
+	$(MAKE_FLOAT_MODEL) double 53 -1074
 
-lib/why/single_model.why lib/why/single_strict.why: tools/make_float_model.opt
-	tools/make_float_model.opt single 24 -149
+lib/why/single_model.why lib/why/single_strict.why: $(MAKE_FLOAT_MODEL)
+	$(MAKE_FLOAT_MODEL) single 24 -149
 
 
 static:: $(STATICBINARY)
@@ -842,15 +851,9 @@
 	cp -f $(V7FILES) $(LIBDIR)/why/coq7
 	cp -f $(VO7) $(LIBDIR)/why/coq7
 install-coq-v8 install-coq-v8.1:
-	if test -w $(COQLIB) ; then \
-	 mkdir -p $(COQLIB)/user-contrib ; \
-	 cp -f $(V8FILES) $(COQLIB)/user-contrib ; \
-	 cp -f $(VO8) $(COQLIB)/user-contrib ; \
-	else \
-	echo "Cannot copy to Coq standard library. Add $(LIBDIR)/why/coq to Coq include path." ;\
-	mkdir -p $(LIBDIR)/why/coq ;\
-	cp -f $(VO8) $(V8FILES) $(LIBDIR)/why/coq ;\
-	fi
+	mkdir -p $(COQLIB)/user-contrib
+	cp -f $(V8FILES) $(COQLIB)/user-contrib
+	cp -f $(VO8) $(COQLIB)/user-contrib
 
 install-pvs-no:
 install-pvs-yes: $(PVSFILES)


Index: .cvsignore
===================================================================
RCS file: /cvs/pkgs/rpms/why/F-12/.cvsignore,v
retrieving revision 1.3
retrieving revision 1.4
diff -u -p -r1.3 -r1.4
--- .cvsignore	24 Dec 2008 16:37:05 -0000	1.3
+++ .cvsignore	8 Jan 2010 20:09:42 -0000	1.4
@@ -1,2 +1,2 @@
 krakatoa.pdf
-why-2.17.tar.gz
+why-2.23.tar.gz


Index: caduceus.ps
===================================================================
RCS file: /cvs/pkgs/rpms/why/F-12/caduceus.ps,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -p -r1.1 -r1.2
--- caduceus.ps	5 Aug 2008 16:49:17 -0000	1.1
+++ caduceus.ps	8 Jan 2010 20:09:43 -0000	1.2
@@ -11,7 +11,7 @@
 %DVIPSWebPage: (www.radicaleye.com)
 %DVIPSCommandLine: dvips caduceus.dvi -o caduceus.ps
 %DVIPSParameters: dpi=600
-%DVIPSSource:  TeX output 2008.07.28:1403
+%DVIPSSource:  TeX output 2009.06.23:1409
 %%BeginProcSet: tex.pro 0 0
 %!
 /TeXDict 300 dict def TeXDict begin/N{def}def/B{bind def}N/S{exch}N/X{S
@@ -3561,7 +3561,7 @@ end readonly def
 dup 12 /fi put
 dup 46 /period put
 dup 49 /one put
-dup 52 /four put
+dup 57 /nine put
 dup 65 /A put
 dup 67 /C put
 dup 68 /D put
@@ -3622,91 +3622,94 @@ B4C61B86AD1CF43C0579FEEBBD9CD164CA112769
 27F127BE45FFF7333A812BDCD259788BA0609199672F8672F56E5A6274C17677
 2F73EF9AE57277BE7CFAAE421521CC401C3C6C952D4C884353915FF5C3A61F64
 6544517B95599EAB8E9D757953F44B7A430EA322FA65BF56D944E82F16509880
-3BB6B2C5438F4F709D67B2C6653E22F681D30126A3F7ECC7D7C43EEFEC631704
-5F1635C9B5460A28A5FCB5B6997C19B389C7CB49E95CF08800B9C39523BE4638
-EDC7C6D883F6289EDF8BAE0B2A1A3181F59FD70D1CFEA895E50A6CE64F9611C1
-F7E1EF8C6F8FED4D294E95677B0EFE9F074BD6C4E6EE41B9CD7B18BA56B87CC7
-B868845E4AAA14BC6361B1365D2C3F1BC61C5F5877F2770D9AFBD62E5288CB87
-F6137A8B0995E98775963F03C2B613C6D3DEAFBC2118F490A926C24DE95392E1
-50BC5758499C877BB617D079B46A751D09289751F101277FA98A437BE113AAAD
-026E854140F64E1BA9DDDB38E8B8BB983D057708E569556D73A6E5D5D584F9BD
-FC32DD270AC327B32D7999B3DCF3E3523A41DAE3625B75CED6ABFADBC8271CB0
-8AD9FF084331F04513F11B831D1209BD71A086BE22F27D1206CC830C6FE9276B
-45FB18D69A2C93463A474C84C7C3059384ED9DBF340A147E95BE7FA5DBBD6DDD
-6A12FB399155B5A49940A9F43D858552FA4A509996FE14A268D89F74778726E9
-5D4AAA46907B55BDD228A11729B8B1D6C91152EA9507F46461C4A56E1756A546
-1737DD91C03394BB3BE587C0CCDE8E30904A166B2F7D3D2D616DE9F0D6E07FA4
-5D9B065DF03D5A12476136E2472F9ED5C2062D8E02635C245EFBA217A46AA4FF
-DCC4A53A49C7A3BA6C3E7EDE17EFA611AA46694BED422AD4968A93218EF083BE
-1EEF0801C4998210A2BE952844DF4993B531C220A7607F8EE086823523C94B17
-705B4CF9EC57DCF1E63F6DF828DF58CDA3A9BD34A10B62AEB8E7180BF98EEC2D
-C5168F4CF7891F3FB2E749B358E700713219BD9D4D01A906B96989B71C0C1432
-2885A67F7FAA24993F326BB1CE0A0E0153A2D4FE2E76E87C99509B984B19DAC5
-3D534784A3D44B86C688217D145B9A607298333C5880037165C6B04F0BFCF9B8
-2017E8611A0033FF52A79860C1B2B751DD7AF23FBEDB6E703602D704A9C9B45F
-AF991CF8DFE55FD2E9EDBD6A6E9B47E92645AE9E04F648BD47642502CBBA016E
-6BD15AA2310C75D0C362610FA208D4B686BD90D61C03AA3CD3B95C2E1D8C0CC4
-607A0B9C9046D3BFEC7FACB8A681027EFA1119F2D25DD3EC984366A204A2F52F
-CF66C90150DE1887F3B2A4A82B9094AB2FDB3B7D8C86A385C91C55FDEBB99F19
-B3992ADDD51A1A7AA0FD1813F099FEA7F3A0A1A433D641230BABD75CA805773E
-DE751D69D933754694495264536547F76B06C8099292C6EED3A510F68AB5BA28
-42CC1EAABEAE94D28C5229F6F520DD186BD6805CA260A873A0DE1EEBDBCE1BAB
-C6AE2F64B10444CD7EE6FEE9E1C9B49B0644DF6AC4D2A8E17E4EF584CAE33404
-49A5B385672B90D673F6D040EE2BB1118BD00C86FD97906927E8B4B9CD9086AB
-4D64778EABADBDCA3119D3D3C465AD76D8EAA80EE0833CCC5A002B235C5F1AF6
-4B1AEB4F60C709D5B2076109ABC93E3FB5797A47C981AD94F4CABD9D2430903E
-ACCC450E4F9A17C755416814375DCE4DFE5DD39D059DB06FBDC93F11B7E929A5
-5DF310483288FEDADC33A54CB3DCC8F3131CB7B7D67488DD8293A81A9FA7C006
-8A80D6F9104B260F1AD0F7EDE1CA2CA4FDA96F1314C25A4AC25EEEC0A8581F0F
-06B411DA6967B0DF362774A1C75C57668869D7DBD14F3B3D099B729F7AFA6583
-84B56694701B8031485A2339BE4B4D154E197167C79392EC048172349D0F5CDD
-43FA48472EE589D607C3373DFE53996B79C2C62724B8ED897F1FF11C4CFE7C80
-7284DD4E9E66618CEB3D6855D94D255BF790ED6C8078C0F47790713299BA2B6F
-0BEE5F4A0062E55A8449E382E13AC570024EE4BF897E5BD4EA306A49DD44CB0B
-02A268ACF46F50F02F8EB97293CB249EA507D4FBCD74A8FD2BDFA8C394C62B8C
-86C9D26C352AD4EFA29123A80F8AC2F593F390F79960382D213E14EB94741D68
-781504195EFA13FA680361E84AD1ACF9E47117B1E219CD999820590095B449F1
-587E5E964B532941C28BC3B84945ACAD368E252B55D9B69D94B6AD69933A9EA5
-1D03882F9F78231401CC3A02F4A6732EFE5D3C16C6E821E0E4EF4F542C21C725
-B25D044D5ADAE86C5B15A65D4D80E7CC1B9CB30AA852CD86C5AA7AB32BB79B6D
-08142D2ED3B0E25FB393CDC401AD73B5234F61F3CCDA99A1D111C73197186263
-F43D57FA38AE8E3BC8E48F3BF1C69E1ED553FF0F721BD54480A028FFCB17AD68
-3880C780AB77899078D23CBF7CB00899BC4142140DC904EB684E374B57016980
-958951A5DB9B6536F15EC40E96B6F7B4D29243770B89EFA76B63149352CA595F
-91796DC530BFF2DB37E6CA94F964ECE4DDE172AADB5FAE16D28011840B8A1137
-69C55C83DB3F402AFA97D0FADFC3092F41AD34B2C04E7F87BA360B0AE841E795
-7CFE36B5FFFDA9907D7939B47BB6A9FF408D5DD759CCF13D56403BCC8725C22E
-116ACE67B270C5F34DE0C9DB19BD240F6553BB0C443C201974EC1240EBEAD688
-858ECF4F6CF626E8ACD769007A5929B29932F06F68186EE6F1D010EA5D416AE7
-E7C3621305B655748E8D76526E12FDDA37588EA6C7087F536F2948D06AEB8A92
-CD6AFB34095FC2BDB6169E560F70901E27DE8288DF9E780DC213DF6F6EBA2016
-45158F14BF0F0A5E22BD8862C99C3DB2C69DE89B0DE4725B1244139F922B3606
-86845E99C165CE252126D0E7116F0B108ACF27C202C1CFC60A914C768F6EBA4E
-C21CF0B868764BBABEB54E9146103D59509642743E769C2C079962BDE6047CD0
-328D1309E23AE1B706A5694FA920084AA45F0CC2C69325430B426FE8D76199EB
-6FF1209741FC3E3A4012C7811F5204BA48199DC1BA0F08E015044CCF64F0DF84
-6987B6EF40CCE51290DAEB0EFA5AE6921142E08308C0C1EAFABDFE44D24F77A6
-4918EBA17F946B585E5BE1DC15504D6C67FEF9EB84D7A05081F391B360451415
-615288706E637D8BA10C461708FED33F0A696F8097FA082C2FCB5D6EDAB9B4CE
-5F2896426D0EEB4C4C7166FA6E56CB08C813E40B757F8992533E03B9038843C9
-833B87B4F26684B637E16C8CA8545AC4F7FAB60F2BB25F4902894FE17CC56072
-728BC5F65FF544665918CCC6E083777112E4A3D553AFEF34E9CDD920E4FF2DE1
-0C7E4919B2BB9E25B01E97AF683174A1B872CCE419D6E8BA9D85BAAAA02CA407
-9CEDA5C88BEAB7697AEE323CC8EBD4E471AB5494A8E90036F76FE89083B639AE
-CCC48C14296E9A2330196283585B5739F5D88F0543C2191AF097AA77532C184E
-2D98D82ADAC244CF3FA6FD1537CB0E3EED4F4D09864D578470BFB2D3B56937A0
-277503A5CBF6FED8E3599661E3523FCC4D65029E9DEC2F8CCB15C37F025DC2DC
-D02DD9DEB8DA92B754B0F7364C277B0DB39E8226CF95FF235CD46D70DD2CAA8D
-86E49816F09D405791B7520FABC8B432FB5911ED70F717B1FF7E269CCD19920B
-7A1C5816B0EB76E96BD36BE2CCF97E609C5099F26A52548E60D3962064C14D8B
-4D908570950969EA0377B04620420A78E55FCE7E9EF0427071C08D82C6038888
-5FD337F59E6CC803909FC41A376D25FE8637918D94595D346E2127E9E9D30E6D
-D8E468FDCFDCED8F1B8C2DEBA9C02290C5C6F0A39E53A2BB7DAC0FBAC9044BD6
-FE1798EACA7612C46B6B08504274FD654488C8AAE8077F0E7041046CB4388F53
-03793A52D0F9DAF130FAFBE852C0BDBC69CD797DC89B4824F6E833ADA458D539
-445B95B3C2DC66E636ED334A30CF13F8E6DF451C3F9E834ECEE385FF0DEEA3F8
-D83F156ED482F1A8116BA5B5BC8A1BDBA22AF895BF29CFD87512E0BF6FC4503C
-42AA3607B602A009EBF5DD5756DC01000681B0F6EF1961B43D232D909C5D
+3BB6B2C5438F4F709D67B2C6653E22F681D3012E56515D0E1F01633A70B156D7
+163343AFE48E64ECEB5E8371D89A2DE8AD0A0ED2C424DCFAC827DD58DE0F486B
+22B7CC010188AFA33F9F6D0DC067B0B104CB169824843C41AE7F9EA60ECA380B
+8422FB6F445AD6D9F82B0A6E48FB1C809C0EBED48B750A18FBC23DBC8CB1FEF6
+56C1D4958F611E5F3BE7F90797D99A980518220D081A9308FA43B4A0AF0AA692
+187DE853449C9FD2D9908EAF7800C37A257BEF6DE606DDB3D061B6E9C58FE211
+5EA4896F2D5AC595597BCA18251B9EB5D05899F1435718D7489AE74321EE4232
+749AA4F7BE22AA99EC392B8173D600E5B5C187FCD41049C5492CD9944F42F49C
+D434F66F747EA27306C2EFDF9D0A705CA721EEB94447AC5029983F1D407E1EDF
+2D19A7ADF22678486BB6DF7D4626013761D1A8375A5C9229FFE3C49E6B815FF4
+5B9704BBE03A7055A0487C5989D7CBB888B2D9D75D31A7D305183F4D31C4F76D
+773A95672EDCB63D0A8971C4162B47F7DDBA7245C14AC7DF36E77A99EA36D875
+79786F8DD335EB980F775F788AA3B1A2EA93C6D90A37DA71AD64BEE092AC8A6B
+89B6C1BDCABF8237B3E6E3FE4819CC818315FDCEB2F1F296DA03B8B5124825DD
+30570C8FD6F2EBC3BF5EA83D5D1B9AF41ECBEC37719AEE1F0B6B1868BA2724F7
+75D85134350FD4B86C579A98D092D655DE9E4330D6AD7E7C37C52DFD5B8D72AF
+DEF13D26C2242410582BFB5887C523B7DA0D117F42DD35F79AF6ED7BB820A483
+E3B4DB9CEFA96210EA84F13E1E1207A44FA402CD224D2DEF2E5340B532977A4F
+5C51B390DCC59157F6766DD137302C8F40880736C108ADB1A7059E259CD265B2
+803A6BF769D92666E64CD8A002C038DE90080EC900E50E81D533AB1DCA38FA7C
+15506843732CEC5954D5BCC5774D04DE8FDE8F41DDD33E2C31C957A545C9EFF6
+2252A618475A8D5E653841056489BF82CCA74D4AC7325A54A2F23B5FE76480DC
+7DEB30F25ECC2AE38294DF3C6E4281D2501A8BEC923311CADAC6882231BCE42C
+F9C515052D7DE839850FF900CA3C88572099B6E6BE2B3AC063FC34446772462C
+08C8F11F7CACAAE7BA023EAE9237FB5DD6544A3321DF3EFC047FA89EF0E77F00
+8975CED1E50F61BF083E652D8F9E322D2B4F75AF5D022C238A23573FA658DA85
+79C12DD3473DB18A2EDA21CBF0BA3C574FEB6FDE80365499A13B19489086FA35
+DC3C4046C181DFFB707921E71DB38261F2A7F4373A106021B17A469B058C8F92
+99A0D245CA208BA76546A248F23A1519347875D0D7D6E6A8BD720468367EE867
+967FF6A4728215316BA2146D75436694F5733140A13681F5E37658736AEA2CC9
+7D0E8F31494BAA74A7AC8C8FAA069C76873DED134CC6C1955B1DDA47BD620121
+52518CB3DE9FEF8606FD4946A135F932D0D2254D7C063DED1F37BBA76C085C58
+91C688B5ACFCEE89EA980E3474301A3CF333F2639DD38ACE03E12051DDA8D980
+F3DD48E088FE1517F1E86F56FB6B57F2CC133483344E26E69D406CC13D962C66
+ABA321EFA3A0D60759E7853087194C4FF18215ED32913570F42EA08C5E96EAEA
+0953A943FFB290440C55F81EF8DAD2184475F7570FD8904CF0A60D34ED089D2B
+B3238773CDF9EA4CEDE868BFC6AA5DEF73C445D32493C62265E2866AF2871EA4
+0AB89CA1E12CB25B3E8331BE45341C4B14A109C0956E495BF55A0DDE831D117C
+2BDB9B19B30BB670CD462B2F3761AD9887E8FF1C328EF74DE38AE03867320C8A
+E6A5F643C37BB6EAC4EEB628EE6A0A56EE1C1BA99BCCC2E53DDAA2DD55E552CB
+00A01EE509936282E8EEB193B6C751E4C22FA9DB5FA1101E1BFC021AF4E1EDAD
+3D0688960BA2438EF75DE5C9F9575DE69B1E38547CF90A49FB7456F1D9C55E0F
+0072DABDA18031CA89556ACC1FB6049993ACD0B97FA85CCBBC4B3BD1D9C25033
+EADAAA65F292E0E3C6FA83BF16295CB1EE9E7A1CF2D97334B811DF4BCE5B2D8B
+5D6A16DDCA0573879F074C92B330AC92D73300081BB444069EB53E59E5D59070
+A1FB5E1E6C8BB8D17B1055DEDF5DB4211FD6F07027AD9222C994F4EA13D51946
+AC24584FE64435EA163DEA7191429A0F84445EB82177BC3C915450E6C9BD5962
+F2D8E30A901AAB7DA4179B377E05832E68F8FF333138943C0FF74982681907AC
+50B6214B45A7F5C3611409CCAE3FF462B669DC136C4D3084F81C7E61910D7B57
+EAD936693587B8E50C55BC20FA7C5C49C7FCF7E13702A84EE9798AF80A88A155
+5ACF7481DBFF8F9878CCE9CD49F160C66A2B021E3720F4AF52975F735E84BD50
+5FBE819A10B6FCE54B2EA1762A68240EA6EFB4438D4EDF605605E62C667FAD76
+8FAEA664CD45FD570B64CFB7C09B9CC636CA374364BD0D729AFF1C18879D6811
+9F13997D9A0A04CBEF04D03FD460DB50AF4D245EE0B6923C037B352A065271EA
+833E8A7CB8E40CBE9B937B4F18D4F4809B0CB5C10D262E1B5E99EF67F8F8DD8E
+23BA5F1B6D18B458ADA0AA5F121AF7C9D9EE3C5BFB3F0AADFF5293BA43BFD810
+6CE4FB2E8521AB6BEBE68754C253374B802F187DEAD3F01364A9E7A0337EE59D
+B99E0A80A3192853131FA21D116BF30610C3962C757D058E5FDF9CE34F44E8B8
+57C8CFF155D8447C1A1D3D9651D6ADBD636700FEAA55161D4C3CB11DA36A5D64
+EF557369F25DA939E094DA00E94AD253C78B3EAA427CE4AFFA6DD2E3251AF25B
+754730B072FEA24B5002CC3014A2FEFACC1594443DBA833A20440E7B784F122B
+FBA817B5D243A01FF2511010565C07DCC24CA098321F85884BB51FC8EF8C0354
+C7DFC011D3172389CA464963C39F3071ECEBC8E1C3FBC2071E30F8D989BEC51A
+908BEC59B59DE12E1BE7D2430A3EACC6899263F315C02871FFB1B0EEF4FC6603
+67CBBC243E9F32FF9EF6045080F8545C86E6134F3B3F27AEC86E0DB4320DEE59
+0A0DC84B6B67574BF33BF30F291E1E89502DDD34408DBF61F1FF6F03FCB2BD67
+F9D81EAE3EF51F6467E264E78C40E9C2D5CCA37122F5990A9ED2DC3EFA9C24AE
+802B3BD19050AFE2F847BC06EB195D8770ED6DEC5927B89FAD44A3F979055C03
+A2CB8D685F90EB5B1564B4E2649B2FAD76897EB52C3DF4C1B7830147CD03864A
+E324B9887DC341864704CC86DC98159C59A7FF5F1EF940F3223A6328735265B8
+0601D05DDF2AFFDCD2D097D49333A99CB9F3344FE36B5F546BBE50F0D4A47A4D
+FA97B76BF1BC1DD26B5E53FDC5260BEAD099C80D91202F650888634AEA138E0B
+6EC85A2EDF5B9296B328F14F1A97FFACD21C346FD0E5DC5BF8BBD582B1A2DC7D
+4D6EBC0B87C04C0C6B7E35A78ADEE0C85076FED117475D880D8D7EABBD7B9E2A
+E62939EB2E70B96915551C358658C64EF09472BD37A81D955A1EF45AC59151B6
+54EA2D5562ECA5B2D6C2951684CC52F7B6A696C39577DA5C25CE97B4B6E5864D
+668777C8D50472FF34A2B855EB730E0495A87FEE1CB31041B946AADD7528740E
+E1D56957395314C1BAE6AE7033A588FBFA1A05827CC2992970F0E58AF26172C4
+57AD52413366F206198BA7C0647C28772B5FC6E6320A22DB75E5F6B72EC87304
+056583EE24325B0AC4E5FC3E9C88F3630F22565C8654D92FB9309E58464A04D1
+2D9DC261A91A22603798576DBBFB3096E1C33A37271D39BFABF28D0147BBC69B
+F798BEEC7A3B6947691659B5796F08D15944BB0A01B2B38B751FDC351C2B26BA
+440C177A7A6220D37E15D310330022B835EF5BB9AFF527458F90317901B900FE
+B66A00184CFE29970AED7E03AA383389D3D50FF29996054916CE85E9483EA4CF
+D690BE40371344C92AD2875E42C06093700FD6ACB12EC00C7EBE332879154B14
+64BEC0601F102149A7FA1CA7ABD2BB44803A0A7F252FC4DF03C4A11D65C1E4DB
+F37C0FCB21F4281F41DE1382698B70721ADF8B85C939B60595DFDBB12A6943A9
+15AF9454779D0D906898719F54ABB3E20CD903
 0000000000000000000000000000000000000000000000000000000000000000
 0000000000000000000000000000000000000000000000000000000000000000
 0000000000000000000000000000000000000000000000000000000000000000
@@ -3766,7 +3769,7 @@ rf /Fj 152[45 45 102[{}2 90.9091 /CMSY10
 54 72 76 66 76 73 89 61 76 50 35 73 77 64 66 75 70 69
 73 1[46 1[76 1[27 27 49 49 49 49 49 49 49 49 49 49 49
 27 33 27 76 1[38 38 27 76 2[81 49 14[49 5[54 54 57 11[{}84
-99.6264 /CMR12 rf /Fu 203[67 2[67 2[37 46[{}3 143.462
+99.6264 /CMR12 rf /Fu 198[67 7[67 2[37 46[{}3 143.462
 /CMSS17 rf /Fv 137[89 1[70 74 66 1[100 97 100 154 46
 2[46 100 97 59 86 1[86 1[93 11[133 132 108 13[116 140
 124 1[129 52[104 12[{}24 206.559 /CMSS17 rf end
@@ -3780,10 +3783,10 @@ TeXDict begin
 %%Page: 1 1
 TeXDict begin 1 0 bop 0 1411 3761 24 v 520 1778 a Fv(The)66
 b(CADUCEUS)e(veri\014cation)i(to)5 b(ol)1274 2179 y(fo)-5
-b(r)65 b(C)f(p)-5 b(rograms)1760 2558 y Fu(1.14)p 0 2702
+b(r)65 b(C)f(p)-5 b(rograms)1760 2558 y Fu(1.19)p 0 2702
 V 380 3058 a Ft(V)d(ersion)33 b(Jean-Christophe)h(Filli^)-49
 b(atre,)33 b(Thierry)h(Hub)s(ert)f(and)g(Claude)g(Marc)m(h)m(\023)-46
-b(e)1596 5078 y(July)34 b(28,)e(2008)743 5199 y(INRIA)h(T)-8
+b(e)1587 5078 y(June)33 b(23,)g(2009)743 5199 y(INRIA)g(T)-8
 b(eam-Pro)5 b(ject)34 b Fs(Pr)-5 b(oval)42 b Fr(http://proval.lri.fr)
 694 5319 y Ft(INRIA)33 b(Sacla)m(y)g(-)1376 5294 y(^)1383
 5319 y(Ile-de-F)-8 b(rance)33 b(&)f(LRI,)h(CNRS)g(UMR)g(8623)814
@@ -4644,49 +4647,47 @@ b(a)e(default)h(Co)s(q)g(tactic)g(to)f F
 end
 %%Page: 23 23
 TeXDict begin 23 22 bop 0 100 a Fm(2.2)161 b(Input)52
-b(Files)h(Syn)l(tax)0 321 y Ft(C)37 b(\014les)g(conform)g(to)f(the)h
+b(Files)h(Syn)l(tax)0 328 y Ft(C)37 b(\014les)g(conform)g(to)f(the)h
 (usual)g(ANSI)g(C)g(syn)m(tax)h(and)f(annotations)f(are)h(inserted)h
-(in)f(the)g(source)0 441 y(as)c(commen)m(ts.)0 737 y
-Fo(2.2.1)136 b(Lexical)46 b(con)l(v)l(en)l(tions)0 924
-y Fh(Co)s(de)0 1110 y Ft(The)34 b(lexical)f(con)m(v)m(en)m(tions)j
+(in)f(the)g(source)0 448 y(as)c(commen)m(ts.)0 764 y
+Fo(2.2.1)136 b(Lexical)46 b(con)l(v)l(en)l(tions)0 957
+y Fh(Co)s(de)0 1151 y Ft(The)34 b(lexical)f(con)m(v)m(en)m(tions)j
 (conform)c(to)g(the)h(ANSI)h(C)f(standard)g(\(see)g(for)f(instance)i
-([18]\).)0 1377 y Fh(Annotations)0 1564 y Ft(Within)f(annotations)g
+([18]\).)0 1438 y Fh(Annotations)0 1631 y Ft(Within)f(annotations)g
 (the)g(lexical)h(con)m(v)m(en)m(tions)h(are)d(the)i(same)f(as)g(C)g
-(ones,)g(except)h(that:)145 1773 y Fn(\017)49 b Ft(commen)m(ts)36
-b(are)f(enclosed)h(b)m(y)h Fr(\(*)e Ft(and)g Fr(*\))g
-Ft(\(so)g(that)g(y)m(ou)g(can)g(put)g(commen)m(ts)h(inside)g(anno-)244
-1893 y(tations)d(without)g(messing)h(traditional)e(C)h(compilers\))145
-2102 y Fn(\017)49 b Ft(the)33 b(set)g(of)f(k)m(eyw)m(ords)k(is)d
-(di\013eren)m(t:)294 2473 y Fr(\\forall)350 b(\\exists)249
-b(int)657 b(float)607 b(decreases)294 2594 y(\\true)452
-b(\\false)300 b(if)708 b(then)658 b(else)294 2714 y(invariant)248
-b(variant)h(for)657 b(label)607 b(assert)294 2834 y(requires)299
-b(ensures)249 b(assigns)453 b(logic)607 b(axiom)294 2955
-y(predicate)248 b(\\result)h(\\old)606 b(\\block_length)199
-b(\\null)294 3075 y(reads)452 b(\\valid)300 b(\\valid_index)198
-b(\\valid_range)250 b(\\fresh)294 3196 y(\\base_addr)197
-b(\\nothing)0 3481 y Fo(2.2.2)136 b(Syn)l(tax)0 3667
-y Ft(Annotations)26 b(are)f(inserted)i(in)m(to)f(programs)f(as)h(sp)s
-(ecial)g(commen)m(ts)i(of)d(the)h(shap)s(e)g Fr(/*@)52
-b(...)103 b(*/)26 b Ft(or)0 3788 y(one-line)j(commen)m(ts)i(of)e(the)g
-(shap)s(e)h Fr(//@)52 b(...)43 b Ft(Figure)29 b(2.1)f(giv)m(es)j(the)e
-(syn)m(tax)h(for)f(the)g(additional)g(C)0 3908 y(constructs)35
-b(con)m(taining)e(annotations;)g(some)h(are)f(C)h(declarations)g
-(\(non-terminal)f Fn(h)p Fd(declaration)p Fn(i)p Ft(\))0
-4029 y(and)j(some)g(are)g(C)g(statemen)m(ts)h(\(non-terminal)f
-Fn(h)p Fd(statemen)m(t)r Fn(i)p Ft(\).)54 b(Figure)36
-b(2.2)f(giv)m(es)i(the)f(syn)m(tax)h(for)0 4149 y(the)c(annotations.)0
-4488 y Fm(2.3)161 b(Arithmetic)0 4739 y Fo(2.3.1)136
-b(In)l(teger)46 b(arithmetic)0 4926 y Ft(The)38 b(mo)s(del)f(used)h
-(for)e(in)m(teger)h(arithmetic)h(is)f(con)m(trolled)h(through)e(the)h
-Fr(-int-model)j Ft(option.)56 b(It)0 5046 y(tak)m(es)34
-b(one)f(of)f(the)h(follo)m(wing)g(v)-5 b(alues:)0 5282
-y Fr(-int-model)54 b(exact)244 5446 y Ft(This)33 b(is)f(the)g(default)g
-(mo)s(del.)43 b(All)32 b(C)g(in)m(tegers)h(are)e(mapp)s(ed)i(to)e
-(mathematical)h(in)m(tegers)h Fs(i.e.)244 5567 y Ft(arbitrary)i
-(precision)h(in)m(tegers.)51 b(It)35 b(is)g(th)m(us)g(a)g(mo)s(del)g
-(where)h(all)e(in)m(teger)i(computations)g(are)1832 5816
-y(23)p eop end
+(ones,)g(except)h(that:)145 1856 y Fn(\017)49 b Ft(the)33
+b(set)g(of)f(k)m(eyw)m(ords)k(is)d(di\013eren)m(t:)294
+2256 y Fr(\\forall)350 b(\\exists)249 b(int)657 b(float)607
+b(decreases)294 2376 y(\\true)452 b(\\false)300 b(if)708
+b(then)658 b(else)294 2497 y(invariant)248 b(variant)h(for)657
+b(label)607 b(assert)294 2617 y(requires)299 b(ensures)249
+b(assigns)453 b(logic)607 b(axiom)294 2738 y(predicate)248
+b(\\result)h(\\old)606 b(\\block_length)199 b(\\null)294
+2858 y(reads)452 b(\\valid)300 b(\\valid_index)198 b(\\valid_range)250
+b(\\fresh)294 2978 y(\\base_addr)197 b(\\nothing)145
+3284 y Fn(\017)49 b Ft(single-line)42 b(commen)m(ts)i(\(i.e.)70
+b(using)42 b Fr(//)p Ft(\))g(are)f(allo)m(w)m(ed)h(in)g(annotations,)i
+(so)d(that)g(y)m(ou)h(can)244 3404 y(put)e(commen)m(ts)i(inside)g
+(annotations)e(without)h(messing)g(traditional)f(C)h(compilers.)67
+b(Note)244 3525 y(that)38 b(former)g(syn)m(tax)i(for)d(commen)m(ts)j
+(in)f(annotations)f(using)i Fr(\(*)f Ft(and)f Fr(*\))g
+Ft(is)h(not)f(a)m(v)-5 b(ailable)244 3645 y(an)m(ymore.)0
+3961 y Fo(2.2.2)136 b(Syn)l(tax)0 4154 y Ft(Annotations)26
+b(are)f(inserted)i(in)m(to)f(programs)f(as)h(sp)s(ecial)g(commen)m(ts)i
+(of)d(the)h(shap)s(e)g Fr(/*@)52 b(...)103 b(*/)26 b
+Ft(or)0 4275 y(one-line)j(commen)m(ts)i(of)e(the)g(shap)s(e)h
+Fr(//@)52 b(...)43 b Ft(Figure)29 b(2.1)f(giv)m(es)j(the)e(syn)m(tax)h
+(for)f(the)g(additional)g(C)0 4395 y(constructs)35 b(con)m(taining)e
+(annotations;)g(some)h(are)f(C)h(declarations)g(\(non-terminal)f
+Fn(h)p Fd(declaration)p Fn(i)p Ft(\))0 4516 y(and)j(some)g(are)g(C)g
+(statemen)m(ts)h(\(non-terminal)f Fn(h)p Fd(statemen)m(t)r
+Fn(i)p Ft(\).)54 b(Figure)36 b(2.2)f(giv)m(es)i(the)f(syn)m(tax)h(for)0
+4636 y(the)c(annotations.)0 4996 y Fm(2.3)161 b(Arithmetic)0
+5253 y Fo(2.3.1)136 b(In)l(teger)46 b(arithmetic)0 5446
+y Ft(The)38 b(mo)s(del)f(used)h(for)e(in)m(teger)h(arithmetic)h(is)f
+(con)m(trolled)h(through)e(the)h Fr(-int-model)j Ft(option.)56
+b(It)0 5567 y(tak)m(es)34 b(one)f(of)f(the)h(follo)m(wing)g(v)-5
+b(alues:)1832 5816 y(23)p eop end
 %%Page: 24 24
 TeXDict begin 24 23 bop 0 3 3761 4 v 50 96 a Fn(h)p Fd(c)p
 138 96 30 4 v 35 w(\014le)5 b Fn(i)563 b Ft(::=)100 b
@@ -4858,72 +4859,77 @@ Fr(>)h Fn(j)f Fr(>=)p 0 5378 3761 4 v 11
 b(Syn)m(tax)33 b(of)g(annotations)1832 5816 y(25)p eop
 end
 %%Page: 26 26
-TeXDict begin 26 25 bop 244 100 a Ft(assumed)44 b(to)f(b)s(e)f
+TeXDict begin 26 25 bop 0 100 a Fr(-int-model)54 b(exact)244
+257 y Ft(This)33 b(is)f(the)g(default)g(mo)s(del.)43
+b(All)32 b(C)g(in)m(tegers)h(are)e(mapp)s(ed)i(to)e(mathematical)h(in)m
+(tegers)h Fs(i.e.)244 377 y Ft(arbitrary)i(precision)h(in)m(tegers.)51
+b(It)35 b(is)g(th)m(us)g(a)g(mo)s(del)g(where)h(all)e(in)m(teger)i
+(computations)g(are)244 497 y(assumed)44 b(to)f(b)s(e)f
 Fs(exact)p Ft(.)74 b(As)43 b(a)f(consequence,)49 b(a)42
 b(C)h(program)f(pro)m(v)m(ed)i(correct)g(using)f(this)244
-220 y(mo)s(del)33 b(is)g(indeed)h(correct)f Fs(only)i(if)f(no)h(inte)-5
+618 y(mo)s(del)33 b(is)g(indeed)h(correct)f Fs(only)i(if)f(no)h(inte)-5
 b(ger)34 b(over\015ow)h(o)-5 b(c)g(curs)34 b(during)h(the)g(exe)-5
-b(cution)p Ft(.)244 392 y(Note)26 b(that)g(in)g(this)h(mo)s(del)f
+b(cution)p Ft(.)244 775 y(Note)26 b(that)g(in)g(this)h(mo)s(del)f
 (there)h(is)g(no)f(range)g(of)f(v)-5 b(alues)27 b(asso)s(ciated)g(to)f
-(the)h(C)f(in)m(teger)h(t)m(yp)s(es.)244 512 y(F)-8 b(or)32
+(the)h(C)f(in)m(teger)h(t)m(yp)s(es.)244 895 y(F)-8 b(or)32
 b(instance,)i(if)e Fg(x)h Ft(has)g(t)m(yp)s(e)g Fr(char)p
 Ft(,)h(y)m(ou)f(are)g(not)f(able)h(to)g(pro)m(v)m(e)g(that)g
 Fn(\000)p Ft(128)27 b Fn(\024)h Fg(x)h(<)e Ft(127.)0
-736 y Fr(-int-model)54 b(bounded)244 908 y Ft(In)33 b(this)h(mo)s(del)f
-(the)g(user)h Fs(pr)-5 b(oves)40 b Ft(that)33 b(there)g(is)g(no)g(in)m
-(teger)h(o)m(v)m(er\015o)m(w)h(during)e(the)g(program)244
-1028 y(execution.)44 b(This)30 b(means)g(that)f(eac)m(h)h(op)s
-(eration,)f(including)i(the)e(implicit)h(con)m(v)m(ersions)i(from)244
-1149 y(one)k(in)m(teger)g(t)m(yp)s(e)h(to)e(another,)i(is)f(giv)m(en)h
-(a)e(precondition)i(to)e(establish)i(that)e(the)h(result)h(of)244
-1269 y(the)31 b(computation)h(\014ts)f(in)m(to)g(the)h(target)f(t)m(yp)
-s(e.)43 b(As)32 b(a)f(coun)m(terpart,)h(information)f(ab)s(out)f(the)
-244 1389 y(range)i(of)h(eac)m(h)g(in)m(teger)g(v)-5 b(ariable)33
-b(is)g(pro)m(vided.)244 1561 y(The)h(sizes)g(of)f(the)g(v)-5
-b(arious)33 b(in)m(teger)h(t)m(yp)s(es)g(can)g(b)s(e)f(set)g(using)h
-(the)f(follo)m(wing)g(command-line)244 1682 y(options:)p
-964 1863 2077 4 v 962 1984 4 121 v 1014 1948 a(t)m(yp)s(e)p
-1523 1984 V 375 w(option)p 2392 1984 V 597 w(default)g(v)-5
-b(alue)p 3039 1984 V 964 1987 2077 4 v 962 2107 4 121
-v 1014 2071 a Fr(char)p 1523 2107 V 357 w(-char-size)p
-2392 2107 V 358 w Ft(8)p 3039 2107 V 964 2111 2077 4
-v 962 2231 4 121 v 1014 2195 a Fr(short)p 1523 2231 V
-306 w(-short-size)p 2392 2231 V 307 w Ft(16)p 3039 2231
-V 964 2234 2077 4 v 962 2355 4 121 v 1014 2319 a Fr(int)p
-1523 2355 V 408 w(-int-size)p 2392 2355 V 409 w Ft(32)p
-3039 2355 V 964 2358 2077 4 v 962 2479 4 121 v 1014 2442
-a Fr(long)p 1523 2479 V 357 w(-long-size)p 2392 2479
-V 358 w Ft(32)p 3039 2479 V 964 2482 2077 4 v 962 2602
-4 121 v 1014 2566 a Fr(long)52 b(long)p 1523 2602 V 101
-w(-long-long-size)p 2392 2602 V 103 w Ft(64)p 3039 2602
-V 964 2606 2077 4 v 244 2834 a(Within)33 b(sp)s(eci\014cations,)i(the)e
-(minimal)h(and)f(maximal)g(v)-5 b(alue)33 b(of)f(an)m(y)i(C)f(in)m
-(teger)h(t)m(yp)s(e)f Fg(\034)44 b Ft(can)244 2954 y(b)s(e)33
-b(referred)g(to)f(using)i(the)f(notation)f Fr(\\min)p
-1880 2954 31 4 v 38 w(range\()p Fg(\034)11 b Fr(\))35
-b Ft(and)d Fr(\\max)p 2756 2954 V 38 w(range\()p Fg(\034)11
-b Fr(\))35 b Ft(resp)s(ectiv)m(ely)-8 b(.)0 3178 y Fr(-int-model)54
-b(modulo)244 3350 y Ft(This)29 b(is)f(the)g(mo)s(del)g(whic)m(h)h(is)f
-(faithful)g(to)f(the)h(program)f(execution)j Fs(i.e.)41
-b Ft(mo)s(dulo)28 b(arithmetic)244 3470 y(is)33 b(p)s(erformed)g(as)g
-(so)s(on)f(as)h(an)g(o)m(v)m(er\015o)m(w)h(o)s(ccurs.)244
-3642 y(Sizes)46 b(of)e(in)m(teger)h(t)m(yp)s(es)h(can)e(b)s(e)h(sp)s
-(eci\014ed)h(on)e(the)h(command-line)h(as)e(for)g(the)h
-Fr(bounded)244 3762 y Ft(mo)s(del)33 b(ab)s(o)m(v)m(e.)0
-4076 y Fo(2.3.2)136 b(En)l(umeration)46 b(t)l(yp)t(es)0
-4269 y Ft(The)38 b(default)f(b)s(eha)m(vior)h(regarding)f(en)m
+1089 y Fr(-int-model)54 b(bounded)244 1246 y Ft(In)33
+b(this)h(mo)s(del)f(the)g(user)h Fs(pr)-5 b(oves)40 b
+Ft(that)33 b(there)g(is)g(no)g(in)m(teger)h(o)m(v)m(er\015o)m(w)h
+(during)e(the)g(program)244 1367 y(execution.)44 b(This)30
+b(means)g(that)f(eac)m(h)h(op)s(eration,)f(including)i(the)e(implicit)h
+(con)m(v)m(ersions)i(from)244 1487 y(one)k(in)m(teger)g(t)m(yp)s(e)h
+(to)e(another,)i(is)f(giv)m(en)h(a)e(precondition)i(to)e(establish)i
+(that)e(the)h(result)h(of)244 1607 y(the)31 b(computation)h(\014ts)f
+(in)m(to)g(the)h(target)f(t)m(yp)s(e.)43 b(As)32 b(a)f(coun)m(terpart,)
+h(information)f(ab)s(out)f(the)244 1728 y(range)i(of)h(eac)m(h)g(in)m
+(teger)g(v)-5 b(ariable)33 b(is)g(pro)m(vided.)244 1885
+y(The)h(sizes)g(of)f(the)g(v)-5 b(arious)33 b(in)m(teger)h(t)m(yp)s(es)
+g(can)g(b)s(e)f(set)g(using)h(the)f(follo)m(wing)g(command-line)244
+2005 y(options:)p 964 2127 2077 4 v 962 2247 4 121 v
+1014 2211 a(t)m(yp)s(e)p 1523 2247 V 375 w(option)p 2392
+2247 V 597 w(default)g(v)-5 b(alue)p 3039 2247 V 964
+2251 2077 4 v 962 2371 4 121 v 1014 2335 a Fr(char)p
+1523 2371 V 357 w(-char-size)p 2392 2371 V 358 w Ft(8)p
+3039 2371 V 964 2374 2077 4 v 962 2495 4 121 v 1014 2459
+a Fr(short)p 1523 2495 V 306 w(-short-size)p 2392 2495
+V 307 w Ft(16)p 3039 2495 V 964 2498 2077 4 v 962 2618
+4 121 v 1014 2582 a Fr(int)p 1523 2618 V 408 w(-int-size)p
+2392 2618 V 409 w Ft(32)p 3039 2618 V 964 2622 2077 4
+v 962 2742 4 121 v 1014 2706 a Fr(long)p 1523 2742 V
+357 w(-long-size)p 2392 2742 V 358 w Ft(32)p 3039 2742
+V 964 2745 2077 4 v 962 2866 4 121 v 1014 2830 a Fr(long)52
+b(long)p 1523 2866 V 101 w(-long-long-size)p 2392 2866
+V 103 w Ft(64)p 3039 2866 V 964 2869 2077 4 v 244 3037
+a(Within)33 b(sp)s(eci\014cations,)i(the)e(minimal)h(and)f(maximal)g(v)
+-5 b(alue)33 b(of)f(an)m(y)i(C)f(in)m(teger)h(t)m(yp)s(e)f
+Fg(\034)44 b Ft(can)244 3158 y(b)s(e)33 b(referred)g(to)f(using)i(the)f
+(notation)f Fr(\\min)p 1880 3158 31 4 v 38 w(range\()p
+Fg(\034)11 b Fr(\))35 b Ft(and)d Fr(\\max)p 2756 3158
+V 38 w(range\()p Fg(\034)11 b Fr(\))35 b Ft(resp)s(ectiv)m(ely)-8
+b(.)0 3352 y Fr(-int-model)54 b(modulo)244 3509 y Ft(This)29
+b(is)f(the)g(mo)s(del)g(whic)m(h)h(is)f(faithful)g(to)f(the)h(program)f
+(execution)j Fs(i.e.)41 b Ft(mo)s(dulo)28 b(arithmetic)244
+3629 y(is)33 b(p)s(erformed)g(as)g(so)s(on)f(as)h(an)g(o)m(v)m(er\015o)
+m(w)h(o)s(ccurs.)244 3786 y(Sizes)46 b(of)e(in)m(teger)h(t)m(yp)s(es)h
+(can)e(b)s(e)h(sp)s(eci\014ed)h(on)e(the)h(command-line)h(as)e(for)g
+(the)h Fr(bounded)244 3906 y Ft(mo)s(del)33 b(ab)s(o)m(v)m(e.)0
+4190 y Fo(2.3.2)136 b(En)l(umeration)46 b(t)l(yp)t(es)0
+4375 y Ft(The)38 b(default)f(b)s(eha)m(vior)h(regarding)f(en)m
 (umeration)h(t)m(yp)s(es)g(is)g(to)f(map)g(them)g(to)g(mathematical)h
-(in-)0 4389 y(tegers)h(and)g(to)f(in)m(tro)s(duce)i(one)e(in)m(teger)i
+(in-)0 4495 y(tegers)h(and)g(to)f(in)m(tro)s(duce)i(one)e(in)m(teger)i
 (constan)m(t)f(for)f(eac)m(h)i(elemen)m(t)g(in)f(the)g(en)m(umeration.)
-62 b(F)-8 b(or)0 4510 y(instance,)34 b(the)f(declaration)103
-4737 y Fr(enum)52 b(E)f({)h(A)f(=)h(0,)g(B,)g(C)f(};)0
-4961 y Ft(in)m(tro)s(duces)26 b(three)f(in)m(teger)g(constan)m(t)g
+62 b(F)-8 b(or)0 4616 y(instance,)34 b(the)f(declaration)103
+4790 y Fr(enum)52 b(E)f({)h(A)f(=)h(0,)g(B,)g(C)f(};)0
+4965 y Ft(in)m(tro)s(duces)26 b(three)f(in)m(teger)g(constan)m(t)g
 Fr(A)p Ft(,)g Fr(B)p Ft(,)f Fr(C)h Ft(with)g(v)-5 b(alues)25
 b(0,)h(1)e(and)g(2)g(resp)s(ectiv)m(ely)-8 b(.)44 b(But)24
-b(a)g(v)-5 b(ariable)0 5081 y(of)36 b(t)m(yp)s(e)i Fr(enum)52
+b(a)g(v)-5 b(ariable)0 5085 y(of)36 b(t)m(yp)s(e)i Fr(enum)52
 b(E)37 b Ft(will)g(not)g(b)s(e)g(guaran)m(teed)g(to)g(ha)m(v)m(e)h(one)
 f(of)f(the)h(en)m(umeration)h(v)-5 b(alues:)53 b(it)37
-b(is)g(not)0 5202 y(pro)m(vided)d(as)f(input)g(and)g(it)f(is)h(not)g
+b(is)g(not)0 5206 y(pro)m(vided)d(as)f(input)g(and)g(it)f(is)h(not)g
 (required)h(when)f(assigned)h(the)f(v)-5 b(ariable.)146
 5326 y(Option)26 b Fr(-check-enum)j Ft(enforces)e(the)g(in)m(v)-5
 b(arian)m(t)26 b(that)g(an)g(expression)i(of)e(an)f(en)m(umeration)j(t)


Index: import.log
===================================================================
RCS file: /cvs/pkgs/rpms/why/F-12/import.log,v
retrieving revision 1.3
retrieving revision 1.4
diff -u -p -r1.3 -r1.4
--- import.log	8 Aug 2009 02:35:30 -0000	1.3
+++ import.log	8 Jan 2010 20:09:44 -0000	1.4
@@ -1,3 +1,4 @@
 why-2_14-2_fc9:HEAD:why-2.14-2.fc9.src.rpm:1217954050
 why-2_17-1_fc11:HEAD:why-2.17-1.fc11.src.rpm:1230136029
 why-2_17-4_fc10:HEAD:why-2.17-4.fc10.src.rpm:1249698515
+why-2_23-1_fc12:F-12:why-2.23-1.fc12.src.rpm:1262981231


Index: min_why.why.result
===================================================================
RCS file: /cvs/pkgs/rpms/why/F-12/min_why.why.result,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -p -r1.1 -r1.2
--- min_why.why.result	5 Aug 2008 16:49:17 -0000	1.1
+++ min_why.why.result	8 Jan 2010 20:09:44 -0000	1.2
@@ -6,46 +6,6 @@ logic eq_bool : bool, bool -> prop
 
 logic neq_bool : bool, bool -> prop
 
-logic bool_and : bool, bool -> bool
-
-logic bool_or : bool, bool -> bool
-
-logic bool_xor : bool, bool -> bool
-
-logic bool_not : bool -> bool
-
-axiom bool_and_def:
-  (forall a:bool.
-    (forall b:bool.
-      ((bool_and(a, b) = true) <-> ((a = true) and (b = true)))))
-
-axiom bool_or_def:
-  (forall a:bool.
-    (forall b:bool. ((bool_or(a, b) = true) <-> ((a = true) or (b = true)))))
-
-axiom bool_xor_def:
-  (forall a:bool. (forall b:bool. ((bool_xor(a, b) = true) <-> (a <> b))))
-
-axiom bool_not_def: (forall a:bool. ((bool_not(a) = true) <-> (a = false)))
-
-logic ite : bool, 'a1, 'a1 -> 'a1
-
-axiom ite_true: (forall x:'a1. (forall y:'a1. (ite(true, x, y) = x)))
-
-axiom ite_false: (forall x:'a1. (forall y:'a1. (ite(false, x, y) = y)))
-
-logic add_int : int, int -> int
-
-logic sub_int : int, int -> int
-
-logic mul_int : int, int -> int
-
-logic div_int : int, int -> int
-
-logic mod_int : int, int -> int
-
-logic neg_int : int -> int
-
 logic lt_int : int, int -> prop
 
 logic le_int : int, int -> prop
@@ -58,215 +18,20 @@ logic eq_int : int, int -> prop
 
 logic neq_int : int, int -> prop
 
-logic lt_int_bool : int, int -> bool
-
-logic le_int_bool : int, int -> bool
-
-logic gt_int_bool : int, int -> bool
-
-logic ge_int_bool : int, int -> bool
-
-logic eq_int_bool : int, int -> bool
-
-logic neq_int_bool : int, int -> bool
-
-axiom lt_int_bool_axiom:
-  (forall x:int. (forall y:int. ((lt_int_bool(x, y) = true) <-> (x < y))))
-
-axiom le_int_bool_axiom:
-  (forall x:int. (forall y:int. ((le_int_bool(x, y) = true) <-> (x <= y))))
-
-axiom gt_int_bool_axiom:
-  (forall x:int. (forall y:int. ((gt_int_bool(x, y) = true) <-> (x > y))))
-
-axiom ge_int_bool_axiom:
-  (forall x:int. (forall y:int. ((ge_int_bool(x, y) = true) <-> (x >= y))))
-
-axiom eq_int_bool_axiom:
-  (forall x:int. (forall y:int. ((eq_int_bool(x, y) = true) <-> (x = y))))
-
-axiom neq_int_bool_axiom:
-  (forall x:int. (forall y:int. ((neq_int_bool(x, y) = true) <-> (x <> y))))
-
-logic add_real : real, real -> real
-
-logic sub_real : real, real -> real
-
-logic mul_real : real, real -> real
-
-logic div_real : real, real -> real
-
-logic pow_real : real, real -> real
-
-logic neg_real : real -> real
-
-logic abs_real : real -> real
-
-logic sqrt_real : real -> real
-
-logic real_of_int : int -> real
-
-logic int_of_real : real -> int
-
-logic lt_real : real, real -> prop
-
-logic le_real : real, real -> prop
-
-logic gt_real : real, real -> prop
-
-logic ge_real : real, real -> prop
-
-logic eq_real : real, real -> prop
-
-logic neq_real : real, real -> prop
-
-logic lt_real_bool : real, real -> bool
-
-logic le_real_bool : real, real -> bool
-
-logic gt_real_bool : real, real -> bool
-
-logic ge_real_bool : real, real -> bool
-
-logic eq_real_bool : real, real -> bool
-
-logic neq_real_bool : real, real -> bool
-
-axiom lt_real_bool_axiom:
-  (forall x:real. (forall y:real. ((lt_real_bool(x, y) = true) <-> (x < y))))
-
-axiom le_real_bool_axiom:
-  (forall x:real.
-    (forall y:real. ((le_real_bool(x, y) = true) <-> (x <= y))))
-
-axiom gt_real_bool_axiom:
-  (forall x:real. (forall y:real. ((gt_real_bool(x, y) = true) <-> (x > y))))
-
-axiom ge_real_bool_axiom:
-  (forall x:real.
-    (forall y:real. ((ge_real_bool(x, y) = true) <-> (x >= y))))
-
-axiom eq_real_bool_axiom:
-  (forall x:real. (forall y:real. ((eq_real_bool(x, y) = true) <-> (x = y))))
+logic add_int : int, int -> int
 
-axiom neq_real_bool_axiom:
-  (forall x:real.
-    (forall y:real. ((neq_real_bool(x, y) = true) <-> (x <> y))))
+logic sub_int : int, int -> int
 
-logic int_max : int, int -> int
+logic mul_int : int, int -> int
 
-logic int_min : int, int -> int
+logic div_int : int, int -> int
 
-logic real_max : real, real -> real
+logic mod_int : int, int -> int
 
-logic real_min : real, real -> real
+logic neg_int : int -> int
 
 predicate zwf_zero(a: int, b: int) = ((0 <= b) and (a < b))
 
-type 'a farray
-
-logic access : 'a1 farray, int -> 'a1
-
-logic update : 'a1 farray, int, 'a1 -> 'a1 farray
-
-axiom access_update:
-  (forall a:'a1 farray.
-    (forall i:int. (forall v:'a1. (access(update(a, i, v), i) = v))))
-
-axiom access_update_neq:
-  (forall a:'a1 farray.
-    (forall i:int.
-      (forall j:int.
-        (forall v:'a1.
-          ((i <> j) -> (access(update(a, i, v), j) = access(a, j)))))))
-
-logic array_length : 'a1 farray -> int
-
-predicate sorted_array(t: int farray, i: int, j: int) =
-  (forall k1:int.
-    (forall k2:int.
-      ((((i <= k1) and (k1 <= k2)) and (k2 <= j)) -> (access(t,
-       k1) <= access(t, k2)))))
-
-predicate exchange(a1: 'a1 farray, a2: 'a1 farray, i: int, j: int) =
-  ((array_length(a1) = array_length(a2)) and
-   ((access(a1, i) = access(a2, j)) and
-    ((access(a2, i) = access(a1, j)) and
-     (forall k:int.
-       (((k <> i) and (k <> j)) -> (access(a1, k) = access(a2, k)))))))
-
-logic permut : 'a1 farray, 'a1 farray, int, int -> prop
-
-axiom permut_refl:
-  (forall t:'a1 farray. (forall l:int. (forall u:int. permut(t, t, l, u))))
-
-axiom permut_sym:
-  (forall t1:'a1 farray.
-    (forall t2:'a1 farray.
-      (forall l:int.
-        (forall u:int. (permut(t1, t2, l, u) -> permut(t2, t1, l, u))))))
-
-axiom permut_trans:
-  (forall t1:'a1 farray.
-    (forall t2:'a1 farray.
-      (forall t3:'a1 farray.
-        (forall l:int.
-          (forall u:int.
-            (permut(t1, t2, l, u) ->
-             (permut(t2, t3, l, u) -> permut(t1, t3, l, u))))))))
-
-axiom permut_exchange:
-  (forall a1:'a1 farray.
-    (forall a2:'a1 farray.
-      (forall l:int.
-        (forall u:int.
-          (forall i:int.
-            (forall j:int.
-              (((l <= i) and (i <= u)) ->
-               (((l <= j) and (j <= u)) ->
-                (exchange(a1, a2, i, j) -> permut(a1, a2, l, u))))))))))
-
-axiom exchange_upd:
-  (forall a:'a1 farray.
-    (forall i:int.
-      (forall j:int. exchange(a, update(update(a, i, access(a, j)), j,
-        access(a, i)), i, j))))
-
-axiom permut_weakening:
-  (forall a1:'a1 farray.
-    (forall a2:'a1 farray.
-      (forall l1:int.
-        (forall r1:int.
-          (forall l2:int.
-            (forall r2:int.
-              ((((l1 <= l2) and (l2 <= r2)) and (r2 <= r1)) ->
-               (permut(a1, a2, l2, r2) -> permut(a1, a2, l1, r1)))))))))
-
-axiom permut_eq:
-  (forall a1:'a1 farray.
-    (forall a2:'a1 farray.
-      (forall l:int.
-        (forall u:int.
-          ((l <= u) ->
-           (permut(a1, a2, l, u) ->
-            (forall i:int.
-              (((i < l) or (u < i)) -> (access(a2, i) = access(a1, i))))))))))
-
-predicate permutation(a1: 'a1 farray, a2: 'a1 farray) = permut(a1, a2, 0,
-  (array_length(a1) - 1))
-
-axiom array_length_update:
-  (forall a:'a1 farray.
-    (forall i:int.
-      (forall v:'a1. (array_length(update(a, i, v)) = array_length(a)))))
-
-axiom permut_array_length:
-  (forall a1:'a1 farray.
-    (forall a2:'a1 farray.
-      (forall l:int.
-        (forall u:int.
-          (permut(a1, a2, l, u) -> (array_length(a1) = array_length(a2)))))))
-
 logic min : int, int -> int
 
 axiom min_ax: (forall x:int. (forall y:int. (min(x, y) <= x)))


Index: sources
===================================================================
RCS file: /cvs/pkgs/rpms/why/F-12/sources,v
retrieving revision 1.3
retrieving revision 1.4
diff -u -p -r1.3 -r1.4
--- sources	24 Dec 2008 16:37:05 -0000	1.3
+++ sources	8 Jan 2010 20:09:44 -0000	1.4
@@ -1,2 +1,2 @@
-56c2e53b7ef4dae8afe4e8264ac44419  krakatoa.pdf
-8508024cf174f03c463d5560318ce6b5  why-2.17.tar.gz
+14563361a9427e58115825b4e782d23e  krakatoa.pdf
+8b8d8f6376e42c688521abf5d9f21a9c  why-2.23.tar.gz


Index: why.spec
===================================================================
RCS file: /cvs/pkgs/rpms/why/F-12/why.spec,v
retrieving revision 1.6
retrieving revision 1.7
diff -u -p -r1.6 -r1.7
--- why.spec	22 Sep 2009 19:36:16 -0000	1.6
+++ why.spec	8 Jan 2010 20:09:45 -0000	1.7
@@ -1,6 +1,6 @@
 Name:           why
-Version:        2.17
-Release:        5%{?dist}
+Version:        2.23
+Release:        1%{?dist}
 Summary:        Why software verification platform
 
 Group:          Applications/Engineering
@@ -15,13 +15,27 @@ Source5:        gwhy-icon.png
 Source6:        min.mlw
 Source7:        min_why.why.result
 Source8:        http://caduceus.lri.fr/manual/caduceus.ps
-Source9:        http://gforge.inria.fr/docman/view.php/999/5097/krakatoa.pdf
+Source9:        http://krakatoa.lri.fr/manual/krakatoa.pdf
+
+# The gwhy execution shell script is not particularly informative
+# about when bad parameters are passed to it - this patch fixes that
+# Upstream has been informed about this issue and a better fix is on
+# their todo list
 Patch0:         gwhy-%{version}.patch
+
+# This patch makes a Fedora-specific fix to eliminate checking for the
+# location of Coq - since we're using the coq package, we know where
+# it is and their checking causes the rpm building to fail
+
+# It also makes a fix necessary to correctly build the bytecode only
+# version of why by building the make_float_model tool correctly in
+# this case.
 Patch1:         why-%{version}-Makefile.in.patch
-Patch2:         why-config.patch
+
 BuildRoot:      %{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)
 BuildRequires:  ocaml >= 3.09, ocaml-camlp4-devel, gtk2-devel, ocaml-lablgtk-devel, desktop-file-utils, dos2unix, prelink
-BuildRequires:  ocaml-ocamlgraph
+BuildRequires:  ocaml-ocamlgraph-devel
+BuildRequires:  cvc3
 
 ExcludeArch:    sparc64 s390 s390x
 %if 0%{?fedora} >= 11
@@ -82,21 +96,8 @@ manipulation of why Coq-formatted output
 %prep
 %setup -q
 
-# The gwhy execution shell script is not particularly informative
-# about when bad parameters are passed to it - this patch fixes that
-# Upstream has been informed about this issue and a better fix is on
-# their todo list, perhaps for 2.15
-%patch0
-
-# This patch makes a Fedora-specific fix to eliminate checking for the
-# location of Coq - since we're using the coq package, we know where
-# it is and their checking causes the rpm building to fail
-%patch1
-
-# This patch fixes the creation of a default configuration file in Why
-# to use more sensible values for default provers chosen to appear in
-# the lefthand GUI window
-%patch2
+%patch0 -p1
+%patch1 -p1
 
 cp %SOURCE1 %SOURCE2 %SOURCE3 %SOURCE4 %SOURCE5 %SOURCE6 %SOURCE7 %SOURCE8 %SOURCE9 .
 
@@ -109,12 +110,15 @@ cp %SOURCE1 %SOURCE2 %SOURCE3 %SOURCE4 %
 %global opt 0
 %endif
 
-# If not building opt, disable the debug info creation as this would otherwise destroy the bytecode executables
+# It seems that we should not be creating debuginfo regardless of
+# whether we have opt or not, as debuginfo is not particularly useful
+# for OCaml programs
+
 # If we have opt, as this has a dependency on ocaml, we should have ocamlopt.opt
-%if ! %{opt}
-%global __os_install_post /usr/lib/rpm/brp-compress %{nil}
-%global _enable_debug_package 0
+
 %global debug_package %{nil}
+
+%if ! %{opt}
 %global opt_option OCAMLBEST=byte OCAMLC=ocamlc OCAMLDEP=ocamldep OCAMLYACC=ocamlyacc OCAMLLEX=ocamllex
 %else
 %global opt_option OCAMLBEST=opt OCAMLOPT=ocamlopt.opt
@@ -122,9 +126,22 @@ cp %SOURCE1 %SOURCE2 %SOURCE3 %SOURCE4 %
 
 # We actually want to install library files into a non /usr/lib
 # directory as they aren't architecture dependent
-./configure --prefix=%{_prefix} --bindir=%{_bindir} --libdir=%{_datadir} --mandir=%{_mandir} %{!?has_coq: COQC=no}
+
+./configure --prefix=%{_prefix} --bindir=%{_bindir} --libdir=%{_datadir} --mandir=%{_mandir} \
+            %{!?has_coq: COQC=no}
 make %{opt_option}
 
+# Remove unnecessary execstack permissions
+%if %opt
+execstack -c bin/*.opt bin/why-cpulimit
+%endif
+
+# Strip binaries (Makefile misses some of them, and don't want to add an extra patch)
+strip bin/why-cpulimit
+%if %opt
+strip bin/*.opt
+%endif
+
 %check
 %if %opt
 %global why bin/why.opt
@@ -139,7 +156,8 @@ diff min_why.why min_why.why.result > /d
 %install
 rm -rf %{buildroot}
 
-make %{opt_option} BINDIR=%{buildroot}%{_bindir} LIBDIR=%{buildroot}%{_datadir} MANDIR=%{buildroot}%{_mandir} %{?has_coq: COQLIB=%{buildroot}%{_datadir}/coq} install
+make %{opt_option} BINDIR=%{buildroot}%{_bindir} LIBDIR=%{buildroot}%{_datadir} MANDIR=%{buildroot}%{_mandir} \
+     %{?has_coq: COQLIB=%{buildroot}%{_datadir}/coq} install
 
 # Fix a small bug in their Makefile: if no Coq, NO .v files should be installed
 %if 0%{?has_coq} != 1
@@ -206,12 +224,13 @@ rm -rf %{buildroot}
 %{why_data_dir}
 %exclude %{why_data_dir}/gwhy-icon.png
 %{_datadir}/caduceus
-# % {_datadir}/jessie
+%{_datadir}/jessie
 # % {_datadir}/krakatoa
-# % exclude % {_datadir}/jessie/jc.cmo
-# % if % opt
-# % exclude % {_datadir}/jessie/jc.cmx
-# % endif
+%exclude %{_datadir}/jessie/jc.cmo
+%if %opt
+%exclude %{_datadir}/jessie/jc.cmx
+%exclude %{_datadir}/jessie/jc.o
+%endif
 # Man page
 %{_mandir}/man1/why.1.gz
 # Documentation and examples
@@ -239,7 +258,7 @@ rm -rf %{buildroot}
 %{_datadir}/coq/user-contrib/caduceus*
 # % exclude % {_datadir}/coq/user-contrib/caduceus*.v
 %{_datadir}/coq/user-contrib/Caduceus.v*
-# %exclude % {_datadir}/coq/user-contrib/Caduceus.v
+# % exclude % {_datadir}/coq/user-contrib/Caduceus.v
 %{_datadir}/coq/user-contrib/jessie_why.v*
 # % exclude % {_datadir}/coq/user-contrib/jessie_why.v
 %{_datadir}/coq/jessie_why.v*
@@ -248,6 +267,16 @@ rm -rf %{buildroot}
 %endif
 
 %changelog
+* Fri Jan 08 2010 Alan Dunn <amdunn at 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 at ausil.us> - 2.17-5
 - Exclude sparc64 s390 s390x  there is no ocaml there
 


--- gwhy-2.17.patch DELETED ---


--- why-2.17-Makefile.in.patch DELETED ---


--- why-config.patch DELETED ---




More information about the fedora-extras-commits mailing list