Skip to content
Snippets Groups Projects
Commit facbbb73 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] add a guard to statically_allocated

parent 5b21f33e
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/wp/share/why3/frama_c_wp/memaddr.mlw
+ 1
− 1
View file @ facbbb73
...@@ -144,7 +144,7 @@ theory MemAddr ...@@ -144,7 +144,7 @@ theory MemAddr
statically allocated uses static_malloc which is abstract. *) statically allocated uses static_malloc which is abstract. *)
lemma valid_pointers_are_statically_allocated: lemma valid_pointers_are_statically_allocated:
forall a: addr, m: malloc, n: int. forall a: addr, m: malloc, n: int.
valid_rd m a n -> statically_allocated (a.base) n > 0 -> valid_rd m a n -> statically_allocated (a.base)
function int_of_addr addr: int function int_of_addr addr: int
function addr_of_int int: addr function addr_of_int int: addr
......
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