diff --git a/headers/header_spec.txt b/headers/header_spec.txt index 1a83a710a5bb981d01a93e2f5cac9cb58c353743..88e6eb60c47818a2562f0e01ebde0465cbc4a49c 100644 --- a/headers/header_spec.txt +++ b/headers/header_spec.txt @@ -1483,7 +1483,6 @@ src/plugins/wp/LogicSemantics.ml: CEA_WP src/plugins/wp/LogicSemantics.mli: CEA_WP src/plugins/wp/LogicUsage.ml: CEA_WP src/plugins/wp/LogicUsage.mli: CEA_WP -src/plugins/wp/MakeDistrib: .ignore src/plugins/wp/Makefile.in: CEA_WP src/plugins/wp/Matrix.ml: CEA_WP src/plugins/wp/Matrix.mli: CEA_WP @@ -1506,8 +1505,6 @@ src/plugins/wp/MemZeroAlias.mli: CEA_WP src/plugins/wp/Sigs.ml: CEA_WP src/plugins/wp/Mstate.ml: CEA_WP src/plugins/wp/Mstate.mli: CEA_WP -src/plugins/wp/Partitioning.ml: CEA_WP -src/plugins/wp/Partitioning.mli: CEA_WP src/plugins/wp/Passive.ml: CEA_WP src/plugins/wp/Passive.mli: CEA_WP src/plugins/wp/Pcfg.ml: CEA_WP @@ -1516,7 +1513,6 @@ src/plugins/wp/Pcond.ml: CEA_WP src/plugins/wp/Pcond.mli: CEA_WP src/plugins/wp/Plang.ml: CEA_WP src/plugins/wp/Plang.mli: CEA_WP -src/plugins/wp/PrecisionLoss.mli: CEA_WP src/plugins/wp/ProofEngine.ml: CEA_WP src/plugins/wp/ProofEngine.mli: CEA_WP src/plugins/wp/ProofSession.ml: CEA_WP @@ -1535,7 +1531,6 @@ src/plugins/wp/ProverTask.ml: CEA_WP src/plugins/wp/ProverTask.mli: CEA_WP src/plugins/wp/ProverWhy3.mli: CEA_WP src/plugins/wp/ProverWhy3.ml: CEA_WP -src/plugins/wp/REVISION: .ignore src/plugins/wp/RefUsage.ml: CEA_WP src/plugins/wp/RefUsage.mli: CEA_WP src/plugins/wp/Region.ml: CEA_WP @@ -1662,208 +1657,6 @@ src/plugins/wp/doc/manual/wp_runtime.tex: .ignore src/plugins/wp/doc/manual/wp_simplifier.tex: .ignore src/plugins/wp/doc/manual/wp_store.tex: .ignore src/plugins/wp/doc/manual/wp_typed.tex: .ignore -src/plugins/wp/doc/tutorial/.gitignore: .ignore -src/plugins/wp/doc/tutorial/Makefile: .ignore -src/plugins/wp/doc/tutorial/README: .ignore -src/plugins/wp/doc/tutorial/adjacent/adjacent.c: .ignore -src/plugins/wp/doc/tutorial/adjacent/adjacent.h: .ignore -src/plugins/wp/doc/tutorial/adjacent/adjacent.impl: .ignore -src/plugins/wp/doc/tutorial/adjacent/adjacent.spec: .ignore -src/plugins/wp/doc/tutorial/adjacent/adjacent.tex: .ignore -src/plugins/wp/doc/tutorial/adjacent/adjacent_report.tex: .ignore -src/plugins/wp/doc/tutorial/adjacent/neighbors.spec: .ignore -src/plugins/wp/doc/tutorial/binary/binary.h: .ignore -src/plugins/wp/doc/tutorial/binary/division.spec: .ignore -src/plugins/wp/doc/tutorial/binary/sorted.spec: .ignore -src/plugins/wp/doc/tutorial/binarysearch/binarysearch.c: .ignore -src/plugins/wp/doc/tutorial/binarysearch/binarysearch.h: .ignore -src/plugins/wp/doc/tutorial/binarysearch/binarysearch.impl: .ignore -src/plugins/wp/doc/tutorial/binarysearch/binarysearch.spec: .ignore -src/plugins/wp/doc/tutorial/binarysearch/binarysearch.tex: .ignore -src/plugins/wp/doc/tutorial/binarysearch/binarysearch_report.tex: .ignore -src/plugins/wp/doc/tutorial/compare/compare.c: .ignore -src/plugins/wp/doc/tutorial/compare/compare.report: .ignore -src/plugins/wp/doc/tutorial/compare/compare.spec: .ignore -src/plugins/wp/doc/tutorial/compare/compare.tex: .ignore -src/plugins/wp/doc/tutorial/compare/compare_report.tex: .ignore -src/plugins/wp/doc/tutorial/compare/greater.c: .ignore -src/plugins/wp/doc/tutorial/compare/greater.spec: .ignore -src/plugins/wp/doc/tutorial/compare/less.c: .ignore -src/plugins/wp/doc/tutorial/compare/less.spec: .ignore -src/plugins/wp/doc/tutorial/console.report: .ignore -src/plugins/wp/doc/tutorial/copy/copy.c: .ignore -src/plugins/wp/doc/tutorial/copy/copy.h: .ignore -src/plugins/wp/doc/tutorial/copy/copy.impl: .ignore -src/plugins/wp/doc/tutorial/copy/copy.spec: .ignore -src/plugins/wp/doc/tutorial/copy/copy.tex: .ignore -src/plugins/wp/doc/tutorial/copy/copy_report.tex: .ignore -src/plugins/wp/doc/tutorial/count/count.axioms: .ignore -src/plugins/wp/doc/tutorial/count/count.c: .ignore -src/plugins/wp/doc/tutorial/count/count.h: .ignore -src/plugins/wp/doc/tutorial/count/count.impl: .ignore -src/plugins/wp/doc/tutorial/count/count.lemma: .ignore -src/plugins/wp/doc/tutorial/count/count.spec: .ignore -src/plugins/wp/doc/tutorial/count/count.tex: .ignore -src/plugins/wp/doc/tutorial/count/count_report.tex: .ignore -src/plugins/wp/doc/tutorial/count/original.axioms: .ignore -src/plugins/wp/doc/tutorial/equal/equal.c: .ignore -src/plugins/wp/doc/tutorial/equal/equal.h: .ignore -src/plugins/wp/doc/tutorial/equal/equal.impl: .ignore -src/plugins/wp/doc/tutorial/equal/equal.spec: .ignore -src/plugins/wp/doc/tutorial/equal/equal.tex: .ignore -src/plugins/wp/doc/tutorial/equal/equal_report.tex: .ignore -src/plugins/wp/doc/tutorial/equal/equal_rte_report.tex: .ignore -src/plugins/wp/doc/tutorial/fill/fill.c: .ignore -src/plugins/wp/doc/tutorial/fill/fill.h: .ignore -src/plugins/wp/doc/tutorial/fill/fill.impl: .ignore -src/plugins/wp/doc/tutorial/fill/fill.spec: .ignore -src/plugins/wp/doc/tutorial/fill/fill.tex: .ignore -src/plugins/wp/doc/tutorial/fill/fill_report.tex: .ignore -src/plugins/wp/doc/tutorial/find/find.c: .ignore -src/plugins/wp/doc/tutorial/find/find.h: .ignore -src/plugins/wp/doc/tutorial/find/find.impl: .ignore -src/plugins/wp/doc/tutorial/find/find.spec: .ignore -src/plugins/wp/doc/tutorial/find/find.tex: .ignore -src/plugins/wp/doc/tutorial/find/find_report.tex: .ignore -src/plugins/wp/doc/tutorial/find/hasvalue.spec: .ignore -src/plugins/wp/doc/tutorial/findfirst/findfirst.c: .ignore -src/plugins/wp/doc/tutorial/findfirst/findfirst.h: .ignore -src/plugins/wp/doc/tutorial/findfirst/findfirst.impl: .ignore -src/plugins/wp/doc/tutorial/findfirst/findfirst.spec: .ignore -src/plugins/wp/doc/tutorial/findfirst/findfirst.tex: .ignore -src/plugins/wp/doc/tutorial/findfirst/findfirst_report.tex: .ignore -src/plugins/wp/doc/tutorial/findfirst/hasvalueof.spec: .ignore -src/plugins/wp/doc/tutorial/iota/iota.c: .ignore -src/plugins/wp/doc/tutorial/iota/iota.h: .ignore -src/plugins/wp/doc/tutorial/iota/iota.impl: .ignore -src/plugins/wp/doc/tutorial/iota/iota.spec: .ignore -src/plugins/wp/doc/tutorial/iota/iota.tex: .ignore -src/plugins/wp/doc/tutorial/iota/iota_report.tex: .ignore -src/plugins/wp/doc/tutorial/library.h: .ignore -src/plugins/wp/doc/tutorial/library.spec: .ignore -src/plugins/wp/doc/tutorial/lowerbound/lowerbound.c: .ignore -src/plugins/wp/doc/tutorial/lowerbound/lowerbound.h: .ignore -src/plugins/wp/doc/tutorial/lowerbound/lowerbound.impl: .ignore -src/plugins/wp/doc/tutorial/lowerbound/lowerbound.spec: .ignore -src/plugins/wp/doc/tutorial/lowerbound/lowerbound.tex: .ignore -src/plugins/wp/doc/tutorial/lowerbound/lowerbound_report.tex: .ignore -src/plugins/wp/doc/tutorial/maxelt/maxelt.c: .ignore -src/plugins/wp/doc/tutorial/maxelt/maxelt.h: .ignore -src/plugins/wp/doc/tutorial/maxelt/maxelt.impl: .ignore -src/plugins/wp/doc/tutorial/maxelt/maxelt.spec: .ignore -src/plugins/wp/doc/tutorial/maxelt/maxelt.tex: .ignore -src/plugins/wp/doc/tutorial/maxelt/maxelt_report.tex: .ignore -src/plugins/wp/doc/tutorial/maxeltp/maxelt.c: .ignore -src/plugins/wp/doc/tutorial/maxeltp/maxelt.h: .ignore -src/plugins/wp/doc/tutorial/maxeltp/maxelt.impl: .ignore -src/plugins/wp/doc/tutorial/maxeltp/maxelt.report: .ignore -src/plugins/wp/doc/tutorial/maxeltp/maxelt.spec: .ignore -src/plugins/wp/doc/tutorial/maxeltp/maxelt.tex: .ignore -src/plugins/wp/doc/tutorial/maxeltp/maxelt_report.tex: .ignore -src/plugins/wp/doc/tutorial/maxeltp/maximum.spec: .ignore -src/plugins/wp/doc/tutorial/maxseq/maxseq.c: .ignore -src/plugins/wp/doc/tutorial/maxseq/maxseq.h: .ignore -src/plugins/wp/doc/tutorial/maxseq/maxseq.impl: .ignore -src/plugins/wp/doc/tutorial/maxseq/maxseq.spec: .ignore -src/plugins/wp/doc/tutorial/maxseq/maxseq.tex: .ignore -src/plugins/wp/doc/tutorial/maxseq/maxseq_report.tex: .ignore -src/plugins/wp/doc/tutorial/minelt/minelt.c: .ignore -src/plugins/wp/doc/tutorial/minelt/minelt.h: .ignore -src/plugins/wp/doc/tutorial/minelt/minelt.impl: .ignore -src/plugins/wp/doc/tutorial/minelt/minelt.spec: .ignore -src/plugins/wp/doc/tutorial/minelt/minelt.tex: .ignore -src/plugins/wp/doc/tutorial/minelt/minelt_report.tex: .ignore -src/plugins/wp/doc/tutorial/mismatch/eqmismatch.report: .ignore -src/plugins/wp/doc/tutorial/mismatch/eqmismatch_report.tex: .ignore -src/plugins/wp/doc/tutorial/mismatch/equal.c: .ignore -src/plugins/wp/doc/tutorial/mismatch/mismatch.c: .ignore -src/plugins/wp/doc/tutorial/mismatch/mismatch.h: .ignore -src/plugins/wp/doc/tutorial/mismatch/mismatch.impl: .ignore -src/plugins/wp/doc/tutorial/mismatch/mismatch.spec: .ignore -src/plugins/wp/doc/tutorial/mismatch/mismatch.tex: .ignore -src/plugins/wp/doc/tutorial/mismatch/mismatch_report.tex: .ignore -src/plugins/wp/doc/tutorial/ptests_local_config.in: .ignore -src/plugins/wp/doc/tutorial/removecopy/original.axioms: .ignore -src/plugins/wp/doc/tutorial/removecopy/removecopy.axioms: .ignore -src/plugins/wp/doc/tutorial/removecopy/removecopy.c: .ignore -src/plugins/wp/doc/tutorial/removecopy/removecopy.h: .ignore -src/plugins/wp/doc/tutorial/removecopy/removecopy.impl: .ignore -src/plugins/wp/doc/tutorial/removecopy/removecopy.spec: .ignore -src/plugins/wp/doc/tutorial/removecopy/removecopy.tex: .ignore -src/plugins/wp/doc/tutorial/removecopy/removecopy_report.tex: .ignore -src/plugins/wp/doc/tutorial/replacecopy/replacecopy.c: .ignore -src/plugins/wp/doc/tutorial/replacecopy/replacecopy.h: .ignore -src/plugins/wp/doc/tutorial/replacecopy/replacecopy.impl: .ignore -src/plugins/wp/doc/tutorial/replacecopy/replacecopy.spec: .ignore -src/plugins/wp/doc/tutorial/replacecopy/replacecopy.tex: .ignore -src/plugins/wp/doc/tutorial/replacecopy/replacecopy_report.tex: .ignore -src/plugins/wp/doc/tutorial/reversecopy/reverse.c: .ignore -src/plugins/wp/doc/tutorial/reversecopy/reverse.h: .ignore -src/plugins/wp/doc/tutorial/reversecopy/reverse.impl: .ignore -src/plugins/wp/doc/tutorial/reversecopy/reverse.spec: .ignore -src/plugins/wp/doc/tutorial/reversecopy/reverse_report.tex: .ignore -src/plugins/wp/doc/tutorial/reversecopy/reversecopy.c: .ignore -src/plugins/wp/doc/tutorial/reversecopy/reversecopy.h: .ignore -src/plugins/wp/doc/tutorial/reversecopy/reversecopy.impl: .ignore -src/plugins/wp/doc/tutorial/reversecopy/reversecopy.spec: .ignore -src/plugins/wp/doc/tutorial/reversecopy/reversecopy.tex: .ignore -src/plugins/wp/doc/tutorial/reversecopy/reversecopy_report.tex: .ignore -src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy.c: .ignore -src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy.h: .ignore -src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy.impl: .ignore -src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy.spec: .ignore -src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy.tex: .ignore -src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy_report.tex: .ignore -src/plugins/wp/doc/tutorial/search/hasrange.spec: .ignore -src/plugins/wp/doc/tutorial/search/search.c: .ignore -src/plugins/wp/doc/tutorial/search/search.h: .ignore -src/plugins/wp/doc/tutorial/search/search.impl: .ignore -src/plugins/wp/doc/tutorial/search/search.spec: .ignore -src/plugins/wp/doc/tutorial/search/search.tex: .ignore -src/plugins/wp/doc/tutorial/search/search_report.tex: .ignore -src/plugins/wp/doc/tutorial/summary.report: .ignore -src/plugins/wp/doc/tutorial/swap/swap.c: .ignore -src/plugins/wp/doc/tutorial/swap/swap.h: .ignore -src/plugins/wp/doc/tutorial/swap/swap.impl: .ignore -src/plugins/wp/doc/tutorial/swap/swap.spec: .ignore -src/plugins/wp/doc/tutorial/swap/swap.tex: .ignore -src/plugins/wp/doc/tutorial/swap/swap_report.tex: .ignore -src/plugins/wp/doc/tutorial/swapranges/swapranges.c: .ignore -src/plugins/wp/doc/tutorial/swapranges/swapranges.h: .ignore -src/plugins/wp/doc/tutorial/swapranges/swapranges.impl: .ignore -src/plugins/wp/doc/tutorial/swapranges/swapranges.spec: .ignore -src/plugins/wp/doc/tutorial/swapranges/swapranges.tex: .ignore -src/plugins/wp/doc/tutorial/swapranges/swapranges_report.tex: .ignore -src/plugins/wp/doc/tutorial/swapvalues/swapvalues-withassert.c: .ignore -src/plugins/wp/doc/tutorial/swapvalues/swapvalues-withassert.impl: .ignore -src/plugins/wp/doc/tutorial/swapvalues/swapvalues.c: .ignore -src/plugins/wp/doc/tutorial/swapvalues/swapvalues.h: .ignore -src/plugins/wp/doc/tutorial/swapvalues/swapvalues.impl: .ignore -src/plugins/wp/doc/tutorial/swapvalues/swapvalues.spec: .ignore -src/plugins/wp/doc/tutorial/swapvalues/swapvalues.tex: .ignore -src/plugins/wp/doc/tutorial/swapvalues/swapvalues_report.tex: .ignore -src/plugins/wp/doc/tutorial/tut_binary.tex: .ignore -src/plugins/wp/doc/tutorial/tut_function.tex: .ignore -src/plugins/wp/doc/tutorial/tut_intro.tex: .ignore -src/plugins/wp/doc/tutorial/tut_maxmin.tex: .ignore -src/plugins/wp/doc/tutorial/tut_mutating.tex: .ignore -src/plugins/wp/doc/tutorial/tut_rationale.tex: .ignore -src/plugins/wp/doc/tutorial/tutorial.tex: .ignore -src/plugins/wp/doc/tutorial/tutorial.tgz: .ignore -src/plugins/wp/doc/tutorial/uniquecopy/original.axioms: .ignore -src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.axioms: .ignore -src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.c: .ignore -src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.h: .ignore -src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.impl: .ignore -src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.spec: .ignore -src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.tex: .ignore -src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy_report.tex: .ignore -src/plugins/wp/doc/tutorial/upperbound/upperbound.c: .ignore -src/plugins/wp/doc/tutorial/upperbound/upperbound.h: .ignore -src/plugins/wp/doc/tutorial/upperbound/upperbound.impl: .ignore -src/plugins/wp/doc/tutorial/upperbound/upperbound.spec: .ignore -src/plugins/wp/doc/tutorial/upperbound/upperbound.tex: .ignore -src/plugins/wp/doc/tutorial/upperbound/upperbound_report.tex: .ignore src/plugins/wp/driver.mli: CEA_WP src/plugins/wp/driver.mll: CEA_WP src/plugins/wp/dyncall.ml: CEA_WP @@ -1881,17 +1674,6 @@ src/plugins/wp/rformat.mli: CEA_WP src/plugins/wp/rformat.mll: CEA_WP src/plugins/wp/script.mli: CEA_WP src/plugins/wp/script.mll: CEA_WP -src/plugins/wp/semantics/Cil.v: .ignore -src/plugins/wp/semantics/Datatype.v: .ignore -src/plugins/wp/semantics/Layout.v: .ignore -src/plugins/wp/semantics/Machine.v: .ignore -src/plugins/wp/semantics/Makefile: .ignore -src/plugins/wp/semantics/Pointer.v: .ignore -src/plugins/wp/semantics/Primitive.v: .ignore -src/plugins/wp/semantics/Semantics.v: .ignore -src/plugins/wp/semantics/Typing.v: .ignore -src/plugins/wp/semantics/Values.v: .ignore -src/plugins/wp/semantics/coqide.sh: .ignore src/plugins/wp/share/.gitignore: .ignore src/plugins/wp/share/Makefile.coqwp: CEA_WP src/plugins/wp/share/Makefile.resources: CEA_WP @@ -1931,16 +1713,6 @@ src/plugins/wp/share/coqwp/real/Real.v: UNMODIFIED_WHY3 src/plugins/wp/share/coqwp/real/RealInfix.v: UNMODIFIED_WHY3 src/plugins/wp/share/coqwp/real/Square.v: UNMODIFIED_WHY3 src/plugins/wp/share/coqwp/real/Trigonometry.v: UNMODIFIED_WHY3 -src/plugins/wp/share/doc/.gitignore: .ignore -src/plugins/wp/share/doc/coq2html.css: .ignore -src/plugins/wp/share/doc/coq2html.js: .ignore -src/plugins/wp/share/doc/coq2html.mll: .ignore -src/plugins/wp/share/doc/coq2latex.mll: .ignore -src/plugins/wp/share/doc/coq2latex.sty: .ignore -src/plugins/wp/share/doc/foot.html: .ignore -src/plugins/wp/share/doc/frama-c.png: .ignore -src/plugins/wp/share/doc/head.html: .ignore -src/plugins/wp/share/doc/index.png: .ignore src/plugins/wp/share/ergo/ArcTrigo.mlw: CEA_WP src/plugins/wp/share/ergo/Cbits.mlw: CEA_WP src/plugins/wp/share/ergo/Cfloat.mlw: CEA_WP