Commit 73d7084b authored by François Bobot's avatar François Bobot
Browse files

Remove frama-c specific ressources

parent d58995e3
Pipeline #36695 passed with stage
in 2 minutes and 2 seconds
Require Export Setoid.
Require Export Morphisms.
Open Scope signature_scope.
(* Axiomatization of Hoare logic. *)
Parameter Values: Set. (* Values manipulated by programs. *)
Parameter Locations: Set. (* Memory locations. *)
Definition Store:= Locations -> Values. (* The store maps memory locations to values. *)
Definition Prog:= Store -> Store. (* A program is simply store transformer. *)
Definition PreState:= Store -> Prop. (* A pre-state is a property over stores. *)
Definition PostState:=Store -> Store -> Prop.
(* Due to the \old construct, a post-state is a relation between initial and final store. *)
Parameter Hoare_triple: PreState -> Prog -> PostState -> Prop.
(* Hoare_triple P S Q states that if we start executing S from a store verifying P, we end up in a store verifying Q. *)
Axiom Hoare_def: forall store S P Q, (Hoare_triple P S Q) <-> (P store -> Q store (S store)).
Parameter wp: Prog -> PostState -> PreState.
(* wp computation: if wp S P holds when starting the execution of S, P holds at the end. *)
Axiom wp_def: forall S (P:PostState), Hoare_triple (wp S P) S P.
(* wp S Q is the _weakest_ pre-condition: any P such that Hoare_triple P S Q holds implies wp S Q.*)
Axiom wp_intros: forall S (P:PreState) (Q: PostState),
Hoare_triple P S Q -> (forall store, P store -> (wp S Q) store).
(* Implication is transferred across wp. *)
Lemma wp_implication:
forall (P:PostState) (Q: PostState), forall S: Prog, forall store,
(P store (S store) -> Q store (S store)) -> ((wp S P store) -> (wp S Q store)).
intros P Q S store Himp Hwp.
apply (wp_intros S (wp S P)); trivial.
elim (Hoare_def store S (wp S P) Q); intros _ Hdef.
apply Hdef; clear Hdef; intros _.
apply Himp.
elim (Hoare_def store S (wp S P) P); intros Hdef _.
apply Hdef; trivial.
apply wp_def.
Qed.
(* combination of wp_def and Hoare_def. *)
Lemma wp_transf: forall Q: PostState, forall S: Prog, forall store, (wp S Q) store -> Q store (S store).
intros Q S store Hwp.
elim (Hoare_def store S (wp S Q) Q); intros Hhoare _. apply Hhoare; trivial.
apply wp_def.
Qed.
(* Parameters for thm1*)
Parameter prog: Prog. (* a program. *)
Parameter loc: Store -> Locations. (* the location whose functional dependencies we want to check. *)
Parameter IsFrom: Locations -> Prop.
Definition From:= sig IsFrom. (* Set of dependencies *)
Parameter Pre: PreState. (* Pre condition. *)
(* Now, we define the function space for the higher-order formulation of the proof obligation.
We want to prove that the final value stored in loc is a function of the values stored initially in From.
For that, we consider functions from Store to Values that give the same answer when applied to two stores
that coincide on From and verify Pre.
*)
(* Full functional space. *)
Definition vec_func_space:= (Locations -> Prop) -> Store -> Values.
(* Partial equivalence relation. We're interested only in the functions for which Phi_per IsFrom Phi Phi holds*)
Definition Phi_per (dom: Locations -> Prop):=
fun Phi1 Phi2: vec_func_space =>
forall store1 store2: Store, Pre store1 -> Pre store2 ->
(forall loc: Locations, dom loc -> store1 loc = store2 loc) -> Phi1 dom store1 = Phi2 dom store2.
Definition Phi_space dom:= { x: vec_func_space | Phi_per dom x x }.
Coercion carrier dom := fun Phi: Phi_space dom => proj1_sig Phi.
Lemma Phi_per_refl: forall dom, reflexive (Phi_space dom) (Phi_per dom).
unfold reflexive.
intros dom Phi; elim Phi.
auto.
Qed.
Lemma Phi_per_sym: forall dom, symmetric (Phi_space dom) (Phi_per dom).
unfold symmetric; unfold Phi_per.
intros dom Phi1 Phi2 Hsym store1 store2 Hpre1 Hpre2 Heq.
symmetry; apply Hsym; auto.
intros loc0 Hdom; symmetry; auto.
Qed.
Lemma Phi_per_trans: forall dom, transitive (Phi_space dom) (Phi_per dom).
unfold transitive; unfold Phi_per.
intros dom Phi1 Phi2 Phi3 Ht1 Ht2 store1 store2 Hpre1 Hpre2 Heq.
transitivity (carrier dom Phi2 dom store1).
apply Ht1; auto.
auto.
Qed.
Add Parametric Relation dom: (Phi_space dom) (Phi_per dom)
reflexivity proved by (Phi_per_refl dom)
symmetry proved by (Phi_per_sym dom)
transitivity proved by (Phi_per_trans dom)
as Phi_relation.
Definition app dom store (Phi:Phi_space dom):= carrier dom Phi dom store.
Definition higher_order_formulation:=
exists phi: (Phi_space IsFrom),
forall store, Pre store -> (wp prog (fun store store' => store' (loc store)= (carrier IsFrom phi IsFrom store)) store).
(* The "first-order" formulation uses arbitrary function and predicate symbols, which are universally quantified here. *)
(* Pre_deps is parameterized by the f_deps function that gives arbitrary values to the the locations*)
Definition Pre_deps f_deps: PreState :=
fun store => forall (x:Locations) (H: IsFrom x) ,(store x = f_deps (exist _ x H)).
(* shortcut for the property we want to prove, parameterized by an arbitrary predicate A. *)
Definition proof_obligation A store := wp prog (fun store store' => A (store' (loc store))) store.
(* At our level, the alpha renaming function just rename store into store' as the initial store. *)
Definition first_order_formulation:=
forall A f_deps,
forall store store',
Pre store -> Pre_deps f_deps store -> Pre store' -> Pre_deps f_deps store' ->
(proof_obligation A store <-> proof_obligation A store').
(* In fact, since store and store' play symmetric role, first order formulation can be reduced to
an implication instead of an equivalence. *)
Lemma weaken_first_order:
(forall A f_deps store store',
Pre store -> Pre_deps f_deps store -> Pre store' -> Pre_deps f_deps store' ->
(proof_obligation A store -> proof_obligation A store'))
<-> first_order_formulation.
unfold first_order_formulation; split.
intros A f_deps Hweak store store' Hpre1 Hpre2 Hpre3 Hpre4; split; intros Hpo; eauto.
intros Hfo A f_deps store store' Hpre1 Hpre2 Hpre3 Hpre4;
elim (Hfo A f_deps store store' Hpre1 Hpre2 Hpre3 Hpre4); auto.
Qed.
(* Main theorem: Both formulation are equivalent. *)
Theorem ho_fo_equiv: higher_order_formulation <-> first_order_formulation.
split.
(* Proof of -> *)
intros Hho; elim weaken_first_order; intros Hweak _; apply Hweak; clear Hweak.
unfold higher_order_formulation in Hho.
intros A f_deps store store' Hpre Hpre_deps Hpre' Hpre_deps'.
unfold proof_obligation.
intros Hwp.
elim Hho.
intros Phi Hho_prop.
(* We'll rewrite (prog store' (loc store')) as Phi IsFrom store' *)
generalize (Hho_prop store' Hpre').
apply wp_implication.
intros Heq.
rewrite Heq.
(* We'll rewrite (prog store (loc store)) as Phi IsFrom store *)
generalize (Hho_prop store Hpre).
generalize (wp_transf _ _ _ Hwp).
intros HA Hwp2.
generalize (wp_transf _ _ _ Hwp2).
intros Heq2.
rewrite Heq2 in HA.
(* Since store and store' coincide on From and Phi verifies Phi_per Phi Phi, we can conclude. *)
fold (app IsFrom store' Phi).
setoid_replace (app IsFrom store' Phi) with (app IsFrom store Phi).
unfold app; simpl.
trivial.
unfold app; simpl; simpl.
elim Phi.
clear Hwp Hwp2 HA Heq Heq2 Hho_prop Phi; intros Phi Hphi.
simpl; simpl.
unfold Phi_per in Hphi; simpl in Hphi.
apply Hphi; auto.
intros loc0 Hloc0.
unfold Pre_deps in Hpre_deps; unfold Pre_deps in Hpre_deps'; simpl in Hpre_deps; simpl in Hpre_deps'.
transitivity (f_deps (exist IsFrom loc0 Hloc0)); auto.
(* Proof of <- *)
intros Hfo;
elim weaken_first_order; intros _ H; generalize (H Hfo); clear H Hfo; intros Hfo.
unfold higher_order_formulation;
unfold proof_obligation in Hfo.
pose (Psi:= fun (dom: Locations -> Prop) store => (prog store) (loc store)).
cut (Phi_per IsFrom Psi Psi).
(* prove that prog store (loc store) = Psi store. *)
intros Hpsi.
exists (exist (fun x => Phi_per IsFrom x x) Psi Hpsi: Phi_space IsFrom).
unfold Psi; simpl.
intros store _.
apply (wp_intros prog (fun _ => True) (fun store store' : Store => store' (loc store) = prog store (loc store))); auto.
elim (Hoare_def store prog (fun _ => True) (fun store store' : Store => store' (loc store) = prog store (loc store)));
intros _ Hhoare; apply Hhoare; auto.
(* prove that Phi_per IsFrom Psi Psi. *)
unfold Phi_per; simpl.
intros store1 store2 Hpre1 Hpre2 store_from_eq.
pose (f_deps:= fun (loc: sig IsFrom) => store1 (proj1_sig loc)).
cut (Pre_deps f_deps store1).
cut (Pre_deps f_deps store2).
intros HPre_deps2 HPre_deps1.
generalize (Hfo (fun val => val = Psi IsFrom store1) f_deps store1 store2 Hpre1 HPre_deps1 Hpre2 HPre_deps2).
unfold Psi; intros H1.
generalize (wp_intros prog (fun _ => True) (fun store store' => store' (loc store) = prog store1 (loc store1))).
intros H.
elim (Hoare_def store1 prog (fun _ => True) (fun store store' => store' (loc store) = prog store1 (loc store1))).
intros _ Hhoare.
generalize (Hhoare (fun _ => (refl_equal (prog store1 (loc store1))))).
clear Hhoare. intros Hhoare;
generalize (H Hhoare store1 I).
clear Hhoare H.
intros H.
generalize (H1 H); clear H1 H; intros H.
symmetry.
apply (wp_transf (fun store store' => store' (loc store) = prog store1 (loc store1))); auto.
unfold Pre_deps.
unfold f_deps; simpl.
intros loc0 Hfrom; symmetry; auto.
unfold Pre_deps; unfold f_deps; simpl; reflexivity.
Qed.
\ No newline at end of file
diff -ru frama-c-Beryllium-20090601-beta1/configure frama-c-Beryllium-20090601-beta1.ok/configure
--- frama-c-Beryllium-20090601-beta1/configure 2009-06-23 16:34:44.000000000 +0200
+++ frama-c-Beryllium-20090601-beta1.ok/configure 2009-06-29 09:51:01.000000000 +0200
@@ -686,7 +686,6 @@
JCCMO
WHYDPBIN
WHYBIN
-HAS_LABLGTK_CUSTOM_MODEL
HAS_LEGACY_GTKSOURCEVIEW
EXTERNAL_PLUGINS
LOCAL_MACHDEP
@@ -823,7 +822,6 @@
enable_wp
enable_external
with_whydir
-enable_custommodel
'
ac_precious_vars='build_alias
host_alias
@@ -1482,7 +1480,6 @@
--enable-wp support for wp plugin (default: yes)
--enable-external=plugin allows to compile directly from Frama-C kernel
some external plug-ins.
- --enable-custommodel use a custom tree model in the GUI. Need to have a recent lablgtk2 version
Optional Packages:
--with-PACKAGE[=ARG] use PACKAGE [ARG=yes]
@@ -7546,46 +7543,6 @@
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
#####################################################
# Check for tools/libraries requirements of plugins #
#####################################################
@@ -8697,37 +8654,107 @@
# lablgtk2's custom tree model
-# Check whether --enable-custommodel was given.
-if test "${enable_custommodel+set}" = set; then
- enableval=$enable_custommodel; ENABLE_CUSTOM_MODEL=$enableval; FORCE_CUSTOM_MODEL=yes
-else
- ENABLE_CUSTOM_MODEL=yes
-
-fi
-
-
-HAS_LABLGTK_CUSTOM_MODEL=no
-if test "$ENABLE_CUSTOM_MODEL" == "yes"; then
- { $as_echo "$as_me:$LINENO: checking for lablgtk2's custom tree model" >&5
-$as_echo_n "checking for lablgtk2's custom tree model... " >&6; }
+if test "$HAS_LABLGTK" == "yes"; then
if echo "type ('a,'b,'c,'d) t = ('a,'b,'c,'d) GTree.custom_tree_model" > test_custommodel.ml && ocamlc -c -I +lablgtk2 test_custommodel.ml 2> /dev/null; \
then
- HAS_LABLGTK_CUSTOM_MODEL=yes
+ { $as_echo "$as_me:$LINENO: checking for lablgtk2's custom tree model" >&5
+$as_echo_n "checking for lablgtk2's custom tree model... " >&6; }
{ $as_echo "$as_me:$LINENO: result: yes" >&5
$as_echo "yes" >&6; }
else
- { $as_echo "$as_me:$LINENO: result: no" >&5
-$as_echo "no" >&6; }
- if test "$FORCE_CUSTOM_MODEL" == "yes"; then
- { { $as_echo "$as_me:$LINENO: error: lablgtk2's custom tree model requested but not available." >&5
-$as_echo "$as_me: error: lablgtk2's custom tree model requested but not available." >&2;}
+ # we don't have a good version of lablgtk2:
+ # configure a dummy library "customtree" in order to
+ # configure plug-ins depending on lablgtk2 in a proper way
+
+# No need to check the same thing multiple times.
+
+
+
+
+
+
+
+
+
+
+
+
+
+# [JS 2009/06/02] sh tests and m4 variables do not mix well together.
+# It works by chance but it is not robust enough.
+# Should be rewritten
+ if test -n "$REQUIRE_LABLGTK" -o -n "$USE_LABLGTK" -o "yes" == "yes"; then
+ HAS_LABLGTK=no
+ if test "$HAS_LABLGTK" != "yes"; then
+ { $as_echo "$as_me:$LINENO: checking for custom-tree-model" >&5
+$as_echo_n "checking for custom-tree-model... " >&6; }
+if test "${ac_cv_file_custom_tree_model+set}" = set; then
+ $as_echo_n "(cached) " >&6
+else
+ test "$cross_compiling" = yes &&
+ { { $as_echo "$as_me:$LINENO: error: cannot check for custom-tree-model existence when cross compiling" >&5
+$as_echo "$as_me: error: cannot check for custom-tree-model existence when cross compiling" >&2;}
{ (exit 1); exit 1; }; }
- else
- { { $as_echo "$as_me:$LINENO: error: lablgtk2's custom tree model unavailable. You need at least LablGtk 2.12" >&5
-$as_echo "$as_me: error: lablgtk2's custom tree model unavailable. You need at least LablGtk 2.12" >&2;}
+if test -r "custom-tree-model"; then
+ ac_cv_file_custom_tree_model=yes
+else
+ ac_cv_file_custom_tree_model=no
+fi
+fi
+{ $as_echo "$as_me:$LINENO: result: $ac_cv_file_custom_tree_model" >&5
+$as_echo "$ac_cv_file_custom_tree_model" >&6; }
+if test "x$ac_cv_file_custom_tree_model" = x""yes; then
+ HAS_LABLGTK=yes
+else
+ HAS_LABLGTK=no
+fi
+
+ if test "$HAS_LABLGTK" == "yes"; then SELECTED_LABLGTK=custom-tree-model
+ fi
+ fi
+
+ if test "$HAS_LABLGTK" == "no"; then
+ { $as_echo "$as_me:$LINENO: WARNING: lablgtk2's custom tree model unavailable. You need at least LablGtk 2.12." >&5
+$as_echo "$as_me: WARNING: lablgtk2's custom tree model unavailable. You need at least LablGtk 2.12." >&2;}
+ if test "$REQUIRE_LABLGTK" != ""; then
+ echo "plug-ins disabled:
+ $REQUIRE_LABLGTK"
+ for p in $REQUIRE_LABLGTK; do
+ fp=FORCE_`upper "$p"`
+ if eval test "\$$fp" == "yes"; then
+ { { $as_echo "$as_me:$LINENO: error: $p requested but custom-tree-model missing." >&5
+$as_echo "$as_me: error: $p requested but custom-tree-model missing." >&2;}
{ (exit 1); exit 1; }; }
+ fi
+ ep=ENABLE_`upper "$p"`
+ eval $ep="no\ \(see\ warning\ about\ custom-tree-model\)"
+ done
+ fi
+ if test "$USE_LABLGTK" != ""; then
+ echo "plug-ins not fully functional:
+ $USE_LABLGTK"
+ for p in $USE_LABLGTK; do
+ ep=ENABLE_`upper "$p"`
+ eval eep="\$$ep"
+ if test "`echo $eep | sed -e 's/ .*//' `" != "no"; then
+ eval $ep="partial\ \(see\ warning\ about\ custom-tree-model\)"
+ fi
+ done
+ fi
+ echo
fi
fi
+
+
+
+
+
+
+
+
+
+
+ fi
rm -f test_custommodel.*
fi
@@ -9142,7 +9169,6 @@
-
# m4_foreach_w is not supported in some old autoconf versions.
# Sadly AC_FOREACH is deprecated now...
diff -ru frama-c-Beryllium-20090601-beta1/configure.in frama-c-Beryllium-20090601-beta1.ok/configure.in
--- frama-c-Beryllium-20090601-beta1/configure.in 2009-06-23 15:50:50.000000000 +0200
+++ frama-c-Beryllium-20090601-beta1.ok/configure.in 2009-06-29 09:50:50.000000000 +0200
@@ -804,27 +804,21 @@
# lablgtk2's custom tree model
-AC_ARG_ENABLE(
- [custommodel],
-[ --enable-custommodel use a custom tree model in the GUI. Need to have a recent lablgtk2 version],
- ENABLE_CUSTOM_MODEL=$enableval; FORCE_CUSTOM_MODEL=yes,
- ENABLE_CUSTOM_MODEL=yes
-)
-
-HAS_LABLGTK_CUSTOM_MODEL=no
-if test "$ENABLE_CUSTOM_MODEL" == "yes"; then
- AC_MSG_CHECKING([for lablgtk2's custom tree model])
+if test "$HAS_LABLGTK" == "yes"; then
if echo "type ('a,'b,'c,'d) t = ('a,'b,'c,'d) GTree.custom_tree_model" > test_custommodel.ml && ocamlc -c -I +lablgtk2 test_custommodel.ml 2> /dev/null; \
then
- HAS_LABLGTK_CUSTOM_MODEL=yes
+ AC_MSG_CHECKING([for lablgtk2's custom tree model])
AC_MSG_RESULT([yes])
else
- AC_MSG_RESULT([no])
- if test "$FORCE_CUSTOM_MODEL" == "yes"; then
- AC_MSG_ERROR([lablgtk2's custom tree model requested but not available.])
- else
- AC_MSG_ERROR([lablgtk2's custom tree model unavailable. You need at least LablGtk 2.12])
- fi
+ # we don't have a good version of lablgtk2:
+ # configure a dummy library "customtree" in order to
+ # configure plug-ins depending on lablgtk2 in a proper way
+ configure_library(
+ [LABLGTK],
+ [custom-tree-model],
+ [lablgtk2's custom tree model unavailable. You need at least LablGtk 2.12.],
+ yes)
+ check_frama_c_dependencies()
fi
rm -f test_custommodel.*
fi
@@ -1137,6 +1131,5 @@
AC_SUBST(HAS_USABLE_NATIVE_DYNLINK)
AC_SUBST(HAS_LEGACY_GTKSOURCEVIEW)
-AC_SUBST(HAS_LABLGTK_CUSTOM_MODEL)
AC_SUBST(WHYBIN)
AC_SUBST(WHYDPBIN)
diff -ru frama-c-Beryllium-20090601-beta1/src/kernel/boot.ml frama-c-Beryllium-20090601-beta1.ok/src/kernel/boot.ml
--- frama-c-Beryllium-20090601-beta1/src/kernel/boot.ml 2009-06-23 11:08:08.000000000 +0200
+++ frama-c-Beryllium-20090601-beta1.ok/src/kernel/boot.ml 2009-06-29 08:48:53.000000000 +0200
@@ -69,7 +69,6 @@
(* Main: let's go! *)
let () =
- if Parameters.Debug.get () > 0 then Printexc.record_backtrace true;
Kind.version := Config.version;
boot_cil ();
Sys.catch_break true;
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment