Skip to content

GitLab

F
frama-c
Commit 434a309e authored by François Bobot's avatar François Bobot
Browse files
Options

Merge branch 'feature/wp/remove-garbage' into 'master' 

[wp] remove garbage files

See merge request frama-c/frama-c!2422
parents fcccfb88 f9bddf3d
Expand all Show whitespace changes
Inline Side-by-side
Showing with 0 additions and 4338 deletions
src/plugins/wp/MakeDistrib deleted 100644 → 0
View file @ fcccfb88
# --------------------------------------------------------------------------
# --- Makefile for WP Distribution ---
# --- Do not distribute this file ---
# --------------------------------------------------------------------------
.PHONY: doc changes headers instructions distrib
TARBALL=wp-$(WP_VERSION)-$(WP_KERNEL)
MANUAL=doc/WP-$(WP_VERSION).pdf
WPINSTALL=install-wp-$(WP_VERSION)-$(WP_KERNEL).prehtml
HEADERS= \
Makefile.in configure.ac \
*.ml *.mll *.mli \
$(MODELS)
DISTRIB_FILES:= \
README INSTALL $(MANUAL) licenses/LGPLv2.1 \
Makefile.in configure.ac configure .depend \
*.ml *.mll *.mli $(MODELS)
distrib: $(DISTRIB_FILES) headers instructions
@echo "Preparing distribution"
@rm -fr tmp.tar $(TARBALL) $(TARBALL).tgz
@tar cf tmp.tar $(DISTRIB_FILES)
@mkdir $(TARBALL)
@tar xf tmp.tar -C $(TARBALL)
@echo "Archive $(TARBALL).tgz"
@tar zcf $(TARBALL).tgz $(TARBALL)
@rm -fr tmp.tar $(TARBALL)
@echo "Distribute '$(TARBALL).tgz' into '<distrib>/download/$(TARBALL).tar.gz'"
@echo "Distribute '$(MANUAL)' into '<distrib>/download/frama-c-wp-manual.pdf'"
@echo "Distribute '$(MANUAL)' into '<distrib>/download/wp-$(WP_VERSION)-$(WP_KERNEL).pdf'"
@echo "Distribute '$(WPINSTALL)' into '<trunk>/doc/www/src/"
@echo "Distribute 'Changelog' into '<trunk>/doc/www/src/wpChangelog'"
instructions:
@echo "Installation instructions"
@ocaml htmlfilter.ml < INSTALL > $(WPINSTALL)
headers::
@echo "Applying Headers"
@headache -c headers/headache_config.txt -h headers/open-source/CEA_LGPL $(HEADERS)
doc/WP-$(WP_VERSION).pdf: doc
doc::
@echo "WP $(WP_VERSION) Manual"
@make -C doc/manual
@cp -f doc/manual/wp.pdf doc/WP-$(WP_VERSION).pdf
changes:
changelog -html /usr/local/shared/changelog -plugin WP -o Changelog.html Changelog
# --------------------------------------------------------------------------
src/plugins/wp/Partitioning.ml deleted 100644 → 0
View file @ fcccfb88
(**************************************************************************)
(* *)
(* This file is part of WP plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2007-2019 *)
(* CEA (Commissariat a l'energie atomique et aux energies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
(* -------------------------------------------------------------------------- *)
(* --- Variables Partitioning --- *)
(* -------------------------------------------------------------------------- *)
open Qed.Logic
open Lang
open Lang.F
type partition = {
mutable color : var Vmap.t ;
mutable depend : Vars.t Vmap.t ;
mutable mem : var Tmap.t ;
}
let zero = Var.dummy
let create () = {
color = Vmap.empty ;
depend = Vmap.empty ;
mem = Tmap.empty ;
}
(* -------------------------------------------------------------------------- *)
(* --- Current Partition --- *)
(* -------------------------------------------------------------------------- *)
let rec color w x =
try
let y = Vmap.find x w.color in
let z = color w y in
if z != y then w.color <- Vmap.add x z w.color ; z
with Not_found -> x
let depend w x =
try Vmap.find (color w x) w.depend
with Not_found -> Vars.empty
(* -------------------------------------------------------------------------- *)
(* --- Unification & Dependencies --- *)
(* -------------------------------------------------------------------------- *)
(* keep x, bind y *)
let merge w x y =
w.color <- Vmap.add y x w.color ;
let xs = depend w x in
let ys = depend w y in
let zs = Vars.union xs ys in
w.depend <- Vmap.add x zs (Vmap.remove y w.depend)
let unify w x y =
if x == zero then y else
if y == zero then x else
let x = color w x in
let y = color w y in
let cmp = Var.compare x y in
if cmp < 0 then (merge w x y ; x) else
if cmp > 0 then (merge w y x ; y) else
x
let add_depend w x xs =
let x = color w x in
let ys = depend w x in
w.depend <- Vmap.add x (Vars.union xs ys) w.depend
(* -------------------------------------------------------------------------- *)
(* --- Segregation --- *)
(* -------------------------------------------------------------------------- *)
let is_varray x = match Var.sort x with Sarray _ -> true | _ -> false
let color_of w c e =
let ms,xs = Vars.partition is_varray (F.vars e) in
let c = Vars.fold (unify w) ms c in
let d = Vars.fold (unify w) xs zero in
if c == zero then d else
(if d != zero then add_depend w c (Vars.singleton d) ; c)
(* -------------------------------------------------------------------------- *)
(* --- Collection --- *)
(* -------------------------------------------------------------------------- *)
let rec collect w p =
match F.repr p with
| Eq(a,b) | Leq(a,b) | Lt(a,b) | Neq(a,b) ->
let ca = color_of w zero a in
let cb = color_of w zero b in
ignore (unify w ca cb)
| Fun(_,es) ->
ignore
(List.fold_left
(fun c e ->
let ce = color_of w zero e in
unify w c ce)
zero es)
| And ps | Or ps -> List.iter (collect w) ps
| Not p -> collect w p
| Imply(hs,p) -> List.iter (collect w) (p::hs)
| Bind(_,_,p) -> collect w (lc_repr p)
| _ -> ignore (color_of w zero p)
let collect w p = collect w (F.e_bool p)
(* -------------------------------------------------------------------------- *)
(* --- Partition --- *)
(* -------------------------------------------------------------------------- *)
type classeq = partition * Vars.t
(* dependencies must be normalized *)
let rec closure w x xs =
let x = color w x in
if Vars.mem x xs then xs else
Vars.fold (closure w) (depend w x) (Vars.add x xs)
let classes w =
w.depend <- Vmap.map (fun _ xs -> Vars.map (color w) xs) w.depend ;
Vars.fold
(fun x cs -> ( w , closure w x Vars.empty ) :: cs)
(Vmap.fold
(fun _ x xs -> Vars.add (color w x) xs)
w.color Vars.empty)
[]
(* Tautologies: False ==> P and P ==> True for all P *)
(* Requires: filter false p ==> p *)
(* Requires: p ==> filter true p *)
let rec filter w positive xs p =
match F.pred p with
| And ps -> F.p_all (filter w positive xs) ps
| Or ps -> F.p_any (filter w positive xs) ps
| Not p -> F.p_not (filter w (not positive) xs p)
| Imply(hs,p) ->
let hs = List.map (filter w (not positive) xs) hs in
F.p_hyps hs (filter w positive xs p)
| Bind(q,x,p) -> F.p_bind q x (filter w positive (Vars.add x xs) p)
| _ ->
if Vars.exists (fun x -> Vars.mem (color w x) xs) (F.varsp p)
then p
else if positive then p_true else p_false
let filter_hyp (w,xs) = filter w true xs
let filter_goal (w,xs) = filter w false xs
src/plugins/wp/Partitioning.mli deleted 100644 → 0
View file @ fcccfb88
(**************************************************************************)
(* *)
(* This file is part of WP plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2007-2019 *)
(* CEA (Commissariat a l'energie atomique et aux energies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
(* -------------------------------------------------------------------------- *)
(* --- Variables Cleaning --- *)
(* -------------------------------------------------------------------------- *)
open Cil_types
open Lang
open Lang.F
type partition
type classeq
val create : unit -> partition
val collect : partition -> F.pred -> unit
val classes : partition -> classeq list
val filter_hyp : classeq -> F.pred -> F.pred
val filter_goal : classeq -> F.pred -> F.pred
src/plugins/wp/PrecisionLoss.mli deleted 100644 → 0
View file @ fcccfb88
(**************************************************************************)
(* *)
(* This file is part of WP plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2007-2019 *)
(* CEA (Commissariat a l'energie atomique et aux energies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
open Qed.Logic
open Lang
open Conditions
open Epsilon
type term = F.term
type system
val fixpoint : system -> int -> int
val assume : system -> term -> unit
val target : system -> term -> unit
val dump : Format.formatter -> system -> unit
class simplifier : Conditions.simplifier
src/plugins/wp/REVISION deleted 100644 → 0
View file @ fcccfb88
# --------------------------------------------------------------------------
# --- REVISION HISTORY ---
# --------------------------------------------------------------------------
R11810 create wp/carbon
R11881 create wp/work-record
R12158 create wp/work/engine
R12896 moveto wp/main
R12978 main development branch (against trunk kernel)
R12975 merged with trunk
R13113 create wp/work/init
R13372 merged with trunk
R13474 merged with trunk
R13504 merged with trunk
R13540 merged with wp/work/init
R13543 plugins/wp/main back into trunk/src/wp
R13553 create wp/work/HoareRef
R14288 merged wp/work/HoareRef into trunk/scr/wp
\ No newline at end of file
src/plugins/wp/doc/tutorial/.gitignore deleted 100644 → 0
View file @ fcccfb88
/tutorial.pdf
/cealistlogo.jpg
/frama-c-book.cls
/frama-c-cover.pdf
/frama-c-left.pdf
/frama-c-right.pdf
/feedback/
/tests/test_config
/tests/ptests_config
/tests/*/result
src/plugins/wp/doc/tutorial/Makefile deleted 100644 → 0
View file @ fcccfb88
# --------------------------------------------------------------------------
# --- WP User & Reference Manual ---
# --------------------------------------------------------------------------
.PHONY: all clean
all: tutorial.pdf
include ../MakeDoc
TEX= \
tutorial.tex \
tut_intro.tex \
tut_function.tex \
tut_maxmin.tex \
tut_binary.tex \
tut_rationale.tex \
tut_mutating.tex \
library.spec \
equal/equal.tex \
equal/equal.spec \
equal/equal.impl \
mismatch/mismatch.tex \
mismatch/mismatch.spec \
mismatch/mismatch.impl \
mismatch/equal.c \
find/find.tex \
find/hasvalue.spec \
find/find.spec \
find/find.impl \
findfirst/findfirst.tex \
findfirst/hasvalueof.spec \
findfirst/findfirst.spec \
findfirst/findfirst.impl \
adjacent/adjacent.tex \
adjacent/neighbors.spec \
adjacent/adjacent.spec \
adjacent/adjacent.impl \
count/count.tex \
count/count.axioms \
count/count.lemma \
count/count.axioms \
count/count.spec \
count/count.impl \
search/search.tex \
search/hasrange.spec \
search/search.spec \
search/search.impl \
compare/compare.tex \
compare/less.spec \
compare/greater.spec \
maxelt/maxelt.tex \
maxelt/maxelt.spec \
maxelt/maxelt.impl \
maxeltp/maxelt.tex \
maxeltp/maximum.spec \
maxeltp/maxelt.spec \
maxeltp/maxelt.impl \
maxseq/maxseq.tex \
maxseq/maxseq.spec \
maxseq/maxseq.impl \
minelt/minelt.tex \
minelt/minelt.spec \
minelt/minelt.impl \
binary/sorted.spec \
binary/division.spec \
lowerbound/lowerbound.tex \
lowerbound/lowerbound.spec \
lowerbound/lowerbound.impl \
upperbound/upperbound.tex \
upperbound/upperbound.spec \
upperbound/upperbound.impl \
binarysearch/binarysearch.tex \
binarysearch/binarysearch.spec \
binarysearch/binarysearch.impl \
fill/fill.tex \
fill/fill.spec \
fill/fill.impl \
swap/swap.tex \
swap/swap.spec \
swap/swap.impl \
swapvalues/swapvalues.tex \
swapvalues/swapvalues.spec \
swapvalues/swapvalues.impl \
swapranges/swapranges.tex \
swapranges/swapranges.spec \
swapranges/swapranges.impl \
copy/copy.tex \
copy/copy.spec \
copy/copy.impl \
reversecopy/reversecopy.tex \
reversecopy/reversecopy.spec \
reversecopy/reversecopy.impl \
reversecopy/reverse.spec \
reversecopy/reverse.impl \
rotatecopy/rotatecopy.tex \
rotatecopy/rotatecopy.spec \
rotatecopy/rotatecopy.impl \
replacecopy/replacecopy.tex \
replacecopy/replacecopy.spec \
replacecopy/replacecopy.impl \
removecopy/removecopy.tex \
removecopy/removecopy.spec \
removecopy/removecopy.impl \
removecopy/removecopy.axioms \
removecopy/original.axioms \
uniquecopy/uniquecopy.tex \
uniquecopy/uniquecopy.spec \
uniquecopy/uniquecopy.impl \
uniquecopy/uniquecopy.axioms \
uniquecopy/original.axioms \
iota/iota.tex \
iota/iota.spec \
iota/iota.impl \
NONMUTATING= \
equal equal_rte mismatch eqmismatch \
find findfirst adjacent \
count search
MAXMIN= compare maxelt maxeltp minelt maxseq
BINARY= lowerbound upperbound binarysearch
MUTATING= \
fill swap
ORACLES= \
$(addprefix tests/nonmutating/oracle/, $(addsuffix .res.oracle, $(NONMUTATING))) \
$(addprefix tests/maxmin/oracle/, $(addsuffix .res.oracle, $(MAXMIN))) \
$(addprefix tests/binary/oracle/, $(addsuffix .res.oracle, $(BINARY))) \
$(addprefix tests/mutating/oracle/, $(addsuffix .res.oracle, $(MUTATING))) \
OLD= \
swapvalues/swapvalues.log \
swapvalues/swapvalues-withassert.log \
swapranges/swapranges.log \
copy/copy.log \
reversecopy/reversecopy.log \
reversecopy/reverse.log \
rotatecopy/rotatecopy.log \
replacecopy/replacecopy.log \
removecopy/removecopy.log \
uniquecopy/uniquecopy.log \
iota/iota.log \
# --------------------------------------------------------------------------
# --- General ---
# --------------------------------------------------------------------------
clean::
@echo "Cleaning Tutorial"
rm -f tutorial.pdf *.cb *.cb2 *.log *.out *.toc *.aux *.blg *.bbl *~
tutorial.pdf: $(FRAMAC_DOC) $(TEX) $(SOURCE) $(ORACLES)
rubber -d tutorial
# --------------------------------------------------------------------------
# --- Generated Logs via ptests ---
# --------------------------------------------------------------------------
.PHONY: config tests kdiff3 update
tests: config
ptests.opt -j 2
kdiff3: config
ptests.opt -j 2 -diff kdiff3