From ce57c4d472ae05e135dc78d4156b2ef3dd860af9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 20 Feb 2020 14:20:50 +0100
Subject: [PATCH] [wp] fix documentation
---
src/plugins/wp/Makefile.in | 1 +
src/plugins/wp/MemMemory.ml | 4 ++--
src/plugins/wp/MemVar.ml | 20 ++++++++++----------
src/plugins/wp/TacHavoc.ml | 4 ++--
4 files changed, 15 insertions(+), 14 deletions(-)
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index b9d1954e66c..2d8c1789b5a 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -230,6 +230,7 @@ wp-doc-api:
$(CP) $(Wp_DIR)/doc/ocamldoc.css $(Wp_DIR)/doc/html/style.css
$(OCAMLDOC) \
-package zarith \
+ -package why3 \
-I lib/fc -I lib/plugins -I $(Wp_DIR) -stars \
-html -d $(Wp_DIR)/doc/html -charset utf-8 \
-t "Frama-C/WP API Documentation" \
diff --git a/src/plugins/wp/MemMemory.ml b/src/plugins/wp/MemMemory.ml
index 3297bfdd33e..44c812ddf3f 100644
--- a/src/plugins/wp/MemMemory.ml
+++ b/src/plugins/wp/MemMemory.ml
@@ -292,8 +292,8 @@ let r_havoc = function
| _ -> raise Not_found
(* havoc(undef,m,p,a)[k] =
- - undef[k] WHEN separated (p,a,k,1)
- - m[k] WHEN NOT separated (p,a,k,1)
+ - m[k] WHEN separated (p,a,k,1)
+ - undef[k] WHEN NOT separated (p,a,k,1)
*)
let r_get_havoc = function
| [undef;m;p;a] ->
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index c0148af7dad..814f165a9b9 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -933,16 +933,16 @@ struct
let frame sigma =
let hs = ref [] in
SIGMA.iter
- begin fun x chunk ->
- (if (x.vglob || x.vformal) then
- let t = VAR.typ_of_chunk x in
- let v = e_var chunk in
- let h = forall_pointers (M.global sigma.mem) v t in
- if not (F.eqp h F.p_true) then hs := h :: !hs ) ;
- (if x.vglob then
- let v = e_var chunk in
- hs := Cvalues.has_ctype x.vtype v :: !hs ) ;
- end sigma.vars ;
+ begin fun x chunk ->
+ (if (x.vglob || x.vformal) then
+ let t = VAR.typ_of_chunk x in
+ let v = e_var chunk in
+ let h = forall_pointers (M.global sigma.mem) v t in
+ if not (F.eqp h F.p_true) then hs := h :: !hs ) ;
+ (if x.vglob then
+ let v = e_var chunk in
+ hs := Cvalues.has_ctype x.vtype v :: !hs ) ;
+ end sigma.vars ;
!hs @ M.frame sigma.mem
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/TacHavoc.ml b/src/plugins/wp/TacHavoc.ml
index 9e68996a899..2f70cab4b56 100644
--- a/src/plugins/wp/TacHavoc.ml
+++ b/src/plugins/wp/TacHavoc.ml
@@ -35,8 +35,8 @@ let lookup_havoc e =
| L.Aget( m , p ) ->
begin
match F.repr m with
- | L.Fun( f , [mr;m0;a;n] ) when f == MemMemory.f_havoc ->
- Some( mr , m0 , a , n , p )
+ | L.Fun( f , [m_undef;m_sep;a;n] ) when f == MemMemory.f_havoc ->
+ Some( m_undef , m_sep , a , n , p )
| _ -> None
end
| _ -> None
--
GitLab