--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on May 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Unable to ensure null



Hello,

I have come across a situation where I cannot ensure that a pointer will 
be null, and I am unsure what I am doing incorrectly. I have a simple 
example below, along with the proof obligations generated. I have also 
attached the full files.

Thank you for your time,
Ian

int *var_ptr;
/*@
assigns var_ptr;// Valid
ensures var_ptr == NULL;// Unknown
ensures var_ptr == \null;// Unknown
ensures !\valid(var_ptr);// Unknown
*/
void function(){
var_ptr = NULL;
}

Running with wp generates the output :

[wp] [Alt-Ergo] Goal typed_function_post : Unknown (Degenerated)
[wp] [Alt-Ergo] Goal typed_function_post_2 : Unknown (Stronger)
[wp] [Alt-Ergo] Goal typed_function_post_3 : Unknown (Stronger)
[wp] [Qed] Goal typed_function_assign : Valid

And the following proof obligations are generated:

goal function_post: forall Malloc_0 : int farray. not linked(Malloc_0)
goal function_post_2:
   forall Malloc_0 : int farray.
   forall var_ptr_0 : addr.
   linked(Malloc_0) ->
   (var_ptr_0 = null)
goal function_post_3:
   forall Malloc_0 : int farray.
   forall var_ptr_0 : addr.
   linked(Malloc_0) ->
   (not valid_rw(Malloc_0, var_ptr_0, 1))

-------------- next part --------------
(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat ?? l'??nergie atomique et aux        *)
(*                        ??nergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(* this is a prelude for Alt-Ergo integer arithmetic *)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat ?? l'??nergie atomique et aux        *)
(*                        ??nergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
logic abs_int : int -> int

axiom abs_def : (forall x:int. ((0 <= x) -> (abs_int(x) = x)))

axiom abs_def1 : (forall x:int. ((not (0 <= x)) -> (abs_int(x) = (-x))))

axiom Abs_le :
  (forall x:int. forall y:int. ((abs_int(x) <= y) -> ((-y) <= x)))

axiom Abs_le1 : (forall x:int. forall y:int. ((abs_int(x) <= y) -> (x <= y)))

axiom Abs_le2 :
  (forall x:int. forall y:int. ((((-y) <= x) and (x <= y)) ->
  (abs_int(x) <= y)))

axiom Abs_pos : (forall x:int. (0 <= abs_int(x)))

(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat ?? l'??nergie atomique et aux        *)
(*                        ??nergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
logic safe_comp_div: int, int -> int
axiom safe_comp_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_div(x,y) = x / y
logic safe_comp_mod: int, int -> int
axiom safe_comp_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_mod(x,y) = x % y
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
(** The theory int_Abs_ must be appended to this file*)
axiom Div_bound :
  (forall x:int. forall y:int. (((0 <= x) and (0 <  y)) ->
  (0 <= safe_comp_div(x,y))))

axiom Div_bound1 :
  (forall x:int. forall y:int. (((0 <= x) and (0 <  y)) ->
  (safe_comp_div(x,y) <= x)))

axiom Div_1 : (forall x:int. (safe_comp_div(x,1) = x))

axiom Mod_1 : (forall x:int. (safe_comp_mod(x,1) = 0))

axiom Div_inf :
  (forall x:int. forall y:int. (((0 <= x) and (x <  y)) ->
  (safe_comp_div(x,y) = 0)))

axiom Mod_inf :
  (forall x:int. forall y:int. (((0 <= x) and (x <  y)) ->
  (safe_comp_mod(x,y) = x)))

axiom Div_mult :
  (forall x:int. forall y:int. forall z:int [safe_comp_div(((x * y) + z),x)].
  (((0 <  x) and ((0 <= y) and (0 <= z))) ->
  (safe_comp_div(((x * y) + z),x) = (y + safe_comp_div(z,x)))))

axiom Mod_mult :
  (forall x:int. forall y:int. forall z:int [safe_comp_mod(((x * y) + z),x)].
  (((0 <  x) and ((0 <= y) and (0 <= z))) ->
  (safe_comp_mod(((x * y) + z),x) = safe_comp_mod(z,x))))

(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat ?? l'??nergie atomique et aux        *)
(*                        ??nergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(* this is a prelude for Alt-Ergo real arithmetic *)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
axiom add_div :
  (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) ->
  (((x + y) / z) = ((x / z) + (y / z)))))

axiom sub_div :
  (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) ->
  (((x - y) / z) = ((x / z) - (y / z)))))

axiom neg_div :
  (forall x:real. forall y:real. ((not (y = 0.0)) ->
  (((-x) / y) = (-(x / y)))))

axiom assoc_mul_div :
  (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) ->
  (((x * y) / z) = (x * (y / z)))))

axiom assoc_div_mul :
  (forall x:real. forall y:real. forall z:real. (((not (y = 0.0)) and
  (not (z = 0.0))) -> (((x / y) / z) = (x / (y * z)))))

axiom assoc_div_div :
  (forall x:real. forall y:real. forall z:real. (((not (y = 0.0)) and
  (not (z = 0.0))) -> ((x / (y / z)) = ((x * z) / y))))

(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat ?? l'??nergie atomique et aux        *)
(*                        ??nergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory real_Real_ must be appended to this file*)
(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat ?? l'??nergie atomique et aux        *)
(*                        ??nergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
(** The theory real_Real_ must be appended to this file*)
logic from_int : int -> real

axiom Zero : (from_int(0) = 0.0)

axiom One : (from_int(1) = 1.0)

axiom Add :
  (forall x:int. forall y:int.
  (from_int((x + y)) = (from_int(x) + from_int(y))))

axiom Sub :
  (forall x:int. forall y:int.
  (from_int((x - y)) = (from_int(x) - from_int(y))))

axiom Mul :
  (forall x:int. forall y:int.
  (from_int((x * y)) = (from_int(x) * from_int(y))))

axiom Neg : (forall x:int. (from_int((-x)) = (-from_int(x))))

(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2014                                               *)
(*    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).            *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory bool_Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
(** The theory int_Abs_ must be appended to this file*)
(** The theory int_ComputerDivision_ must be appended to this file*)
(** The theory real_Real_ must be appended to this file*)
(** The theory real_RealInfix_ must be appended to this file*)
(** The theory real_FromInt_ must be appended to this file*)
logic ite : bool, 'a, 'a -> 'a

axiom ite1 :
  (forall p:bool. forall x:'a. forall y:'a [ite(p, x, y)]. (((p = true) and
  (ite(p, x, y) = x)) or ((p = false) and (ite(p, x, y) = y))))

logic eqb : 'a, 'a -> bool

axiom eqb1 : (forall x:'a. forall y:'a. ((eqb(x, y) = true) -> (x = y)))

axiom eqb2 : (forall x:'a. forall y:'a. ((x = y) -> (eqb(x, y) = true)))

logic neqb : 'a, 'a -> bool

axiom neqb1 :
  (forall x:'a. forall y:'a. ((neqb(x, y) = true) -> (not (x = y))))

axiom neqb2 :
  (forall x:'a. forall y:'a. ((not (x = y)) -> (neqb(x, y) = true)))

logic zlt : int, int -> bool

logic zleq : int, int -> bool

axiom zlt1 : (forall x:int. forall y:int. ((zlt(x, y) = true) -> (x <  y)))

axiom zlt2 : (forall x:int. forall y:int. ((x <  y) -> (zlt(x, y) = true)))

axiom zleq1 : (forall x:int. forall y:int. ((zleq(x, y) = true) -> (x <= y)))

axiom zleq2 : (forall x:int. forall y:int. ((x <= y) -> (zleq(x, y) = true)))

logic rlt : real, real -> bool

logic rleq : real, real -> bool

axiom rlt1 : (forall x:real. forall y:real. ((rlt(x, y) = true) -> (x <  y)))

axiom rlt2 : (forall x:real. forall y:real. ((x <  y) -> (rlt(x, y) = true)))

axiom rleq1 :
  (forall x:real. forall y:real. ((rleq(x, y) = true) -> (x <= y)))

axiom rleq2 :
  (forall x:real. forall y:real. ((x <= y) -> (rleq(x, y) = true)))

logic truncate : real -> int

function real_of_int(x: int) : real = from_int(x)

axiom truncate_of_int : (forall x:int. (truncate(real_of_int(x)) = x))

axiom c_euclidian :
  (forall n:int. forall d:int [safe_comp_div(n,d), safe_comp_mod(n,d)].
  ((not (d = 0)) -> (n = ((safe_comp_div(n,d) * d) + safe_comp_mod(n,d)))))

axiom cdiv_cases :
  (forall n:int. forall d:int [safe_comp_div(n,d)]. ((0 <= n) -> ((0 <  d) ->
  (safe_comp_div(n,d) = (n / d)))))

axiom cdiv_cases1 :
  (forall n:int. forall d:int [safe_comp_div(n,d)]. ((n <= 0) -> ((0 <  d) ->
  (safe_comp_div(n,d) = (-((-n) / d))))))

axiom cdiv_cases2 :
  (forall n:int. forall d:int [safe_comp_div(n,d)]. ((0 <= n) -> ((d <  0) ->
  (safe_comp_div(n,d) = (-(n / (-d)))))))

axiom cdiv_cases3 :
  (forall n:int. forall d:int [safe_comp_div(n,d)]. ((n <= 0) -> ((d <  0) ->
  (safe_comp_div(n,d) = ((-n) / (-d))))))

axiom cmod_cases :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((0 <  d) ->
  (safe_comp_mod(n,d) = (n % d)))))

axiom cmod_cases1 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((0 <  d) ->
  (safe_comp_mod(n,d) = (-((-n) % d))))))

axiom cmod_cases2 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((d <  0) ->
  (safe_comp_mod(n,d) = (n % (-d))))))

axiom cmod_cases3 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((d <  0) ->
  (safe_comp_mod(n,d) = (-((-n) % (-d)))))))

axiom cmod_remainder :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((0 <  d) ->
  (0 <= safe_comp_mod(n,d)))))

axiom cmod_remainder1 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((0 <  d) ->
  (safe_comp_mod(n,d) <  d))))

axiom cmod_remainder2 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((0 <  d) ->
  ((-d) <  safe_comp_mod(n,d)))))

axiom cmod_remainder3 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((0 <  d) ->
  (safe_comp_mod(n,d) <= 0))))

axiom cmod_remainder4 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((d <  0) ->
  (0 <= safe_comp_mod(n,d)))))

axiom cmod_remainder5 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((d <  0) ->
  (safe_comp_mod(n,d) <  (-d)))))

axiom cmod_remainder6 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((d <  0) ->
  (d <  safe_comp_mod(n,d)))))

axiom cmod_remainder7 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((d <  0) ->
  (safe_comp_mod(n,d) <= 0))))

axiom cdiv_neutral :
  (forall a:int [safe_comp_div(a,1)]. (safe_comp_div(a,1) = a))

axiom cdiv_inv :
  (forall a:int [safe_comp_div(a,a)]. ((not (a = 0)) ->
  (safe_comp_div(a,a) = 1)))

(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2014                                               *)
(*    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).            *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory bool_Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
(** The theory map_Map_ must be appended to this file*)
type addr = { base : int; offset : int
}

logic addr_le : addr, addr -> prop

logic addr_lt : addr, addr -> prop

logic addr_le_bool : addr, addr -> bool

logic addr_lt_bool : addr, addr -> bool

axiom addr_le_def :
  (forall p:addr. forall q:addr [addr_le(p, q)]. (((p).base = (q).base) ->
  (addr_le(p, q) -> ((p).offset <= (q).offset))))

axiom addr_le_def1 :
  (forall p:addr. forall q:addr [addr_le(p, q)]. (((p).base = (q).base) ->
  (((p).offset <= (q).offset) -> addr_le(p, q))))

axiom addr_lt_def :
  (forall p:addr. forall q:addr [addr_lt(p, q)]. (((p).base = (q).base) ->
  (addr_lt(p, q) -> ((p).offset <  (q).offset))))

axiom addr_lt_def1 :
  (forall p:addr. forall q:addr [addr_lt(p, q)]. (((p).base = (q).base) ->
  (((p).offset <  (q).offset) -> addr_lt(p, q))))

axiom addr_le_bool_def :
  (forall p:addr. forall q:addr [addr_le_bool(p, q)]. (addr_le(p, q) ->
  (addr_le_bool(p, q) = true)))

axiom addr_le_bool_def1 :
  (forall p:addr. forall q:addr [addr_le_bool(p, q)]. ((addr_le_bool(p,
  q) = true) -> addr_le(p, q)))

axiom addr_lt_bool_def :
  (forall p:addr. forall q:addr [addr_lt_bool(p, q)]. (addr_lt(p, q) ->
  (addr_lt_bool(p, q) = true)))

axiom addr_lt_bool_def1 :
  (forall p:addr. forall q:addr [addr_lt_bool(p, q)]. ((addr_lt_bool(p,
  q) = true) -> addr_lt(p, q)))

function null() : addr = { base = 0; offset = 0 }

function global(b: int) : addr = { base = b; offset = 0 }

function shift(p: addr, k: int) : addr = { base = (p).base; offset =
  ((p).offset + k) }

predicate included(p: addr, a: int, q: addr, b: int) = ((0 <  a) ->
  ((0 <= b) and (((p).base = (q).base) and (((q).offset <= (p).offset) and
  (((p).offset + a) <= ((q).offset + b))))))

predicate separated(p: addr, a: int, q: addr, b: int) = ((a <= 0) or
  ((b <= 0) or ((not ((p).base = (q).base)) or
  ((((q).offset + b) <= (p).offset) or (((p).offset + a) <= (q).offset)))))

predicate eqmem(m1: (addr,'a) farray, m2: (addr,'a) farray, p: addr,
  a1: int) =
  (forall q:addr [(m1[p])| (m2[q])]. (included(q, 1, p, a1) ->
  ((m1[q]) = (m2[q]))))

predicate havoc(m1: (addr,'a) farray, m2: (addr,'a) farray, p: addr,
  a1: int) =
  (forall q:addr [(m1[p])| (m2[q])]. (separated(q, 1, p, a1) ->
  ((m1[q]) = (m2[q]))))

predicate valid_rd(m: (int,int) farray, p: addr, n: int) = ((0 <  n) ->
  ((0 <= (p).offset) and (((p).offset + n) <= (m[(p).base]))))

predicate valid_rw(m: (int,int) farray, p: addr, n: int) = ((0 <  n) ->
  ((0 <  (p).base) and ((0 <= (p).offset) and
  (((p).offset + n) <= (m[(p).base])))))

axiom valid_rw_rd :
  (forall m:(int,int) farray.
  (forall p:addr. (forall n:int. (valid_rw(m, p, n) -> valid_rd(m, p, n)))))

axiom valid_string :
  (forall m:(int,int) farray.
  (forall p:addr. (((p).base <  0) -> (((0 <= (p).offset) and
  ((p).offset <  (m[(p).base]))) -> valid_rd(m, p, 1)))))

axiom valid_string1 :
  (forall m:(int,int) farray.
  (forall p:addr. (((p).base <  0) -> (((0 <= (p).offset) and
  ((p).offset <  (m[(p).base]))) -> (not valid_rw(m, p, 1))))))

axiom separated_1 :
  (forall p:addr. forall q:addr.
  (forall a:int. forall b:int. forall i:int. forall j:int [separated(p, a, q,
  b), { base = (p).base; offset = i }, { base = (q).base; offset = j }].
  (separated(p, a, q, b) -> ((((p).offset <= i) and
  (i <  ((p).offset + a))) -> ((((q).offset <= j) and
  (j <  ((q).offset + b))) -> (not ({ base = (p).base; offset = i } = {
  base = (q).base; offset = j })))))))

logic region : int -> int

logic linked : (int,int) farray -> prop

logic sconst : (addr,int) farray -> prop

predicate framed(m: (addr,addr) farray) =
  (forall p:addr [(m[p])]. (region(((m[p])).base) <= 0))

axiom separated_included :
  (forall p:addr. forall q:addr.
  (forall a:int. forall b:int [separated(p, a, q, b), included(p, a, q, b)].
  ((0 <  a) -> ((0 <  b) -> (separated(p, a, q, b) -> (not included(p, a, q,
  b)))))))

axiom included_trans :
  (forall p:addr. forall q:addr. forall r:addr.
  (forall a:int. forall b:int. forall c:int [included(p, a, q, b),
  included(q, b, r, c)]. (included(p, a, q, b) -> (included(q, b, r, c) ->
  included(p, a, r, c)))))

axiom separated_trans :
  (forall p:addr. forall q:addr. forall r:addr.
  (forall a:int. forall b:int. forall c:int [included(p, a, q, b),
  separated(q, b, r, c)]. (included(p, a, q, b) -> (separated(q, b, r, c) ->
  separated(p, a, r, c)))))

axiom separated_sym :
  (forall p:addr. forall q:addr.
  (forall a:int. forall b:int [separated(p, a, q, b)]. (separated(p, a, q,
  b) -> separated(q, b, p, a))))

axiom separated_sym1 :
  (forall p:addr. forall q:addr.
  (forall a:int. forall b:int [separated(p, a, q, b)]. (separated(q, b, p,
  a) -> separated(p, a, q, b))))

axiom eqmem_included :
  (forall m1:(addr,'a) farray. forall m2:(addr,'a) farray.
  (forall p:addr. forall q:addr.
  (forall a1:int. forall b:int [eqmem(m1, m2, p, a1), eqmem(m1, m2, q, b)].
  (included(p, a1, q, b) -> (eqmem(m1, m2, q, b) -> eqmem(m1, m2, p, a1))))))

axiom eqmem_sym :
  (forall m1:(addr,'a) farray. forall m2:(addr,'a) farray.
  (forall p:addr.
  (forall a1:int. (eqmem(m1, m2, p, a1) -> eqmem(m2, m1, p, a1)))))

axiom havoc_sym :
  (forall m1:(addr,'a) farray. forall m2:(addr,'a) farray.
  (forall p:addr.
  (forall a1:int. (havoc(m1, m2, p, a1) -> havoc(m2, m1, p, a1)))))

logic cast : addr -> int

axiom cast_injective :
  (forall p:addr. forall q:addr [cast(p), cast(q)]. ((cast(p) = cast(q)) ->
  (p = q)))

logic hardware : int -> int

axiom hardnull : (hardware(0) = 0)

(* ---------------------------------------------------------- *)
(* --- Post-condition (file null_pointer.c, line 11) in 'function' --- *)
(* ---------------------------------------------------------- *)

goal function_post_2:
  forall Malloc_0 : int farray.
  forall var_ptr_0 : addr.
  linked(Malloc_0) ->
  (var_ptr_0 = null)

-------------- next part --------------
(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat ?? l'??nergie atomique et aux        *)
(*                        ??nergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(* this is a prelude for Alt-Ergo integer arithmetic *)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat ?? l'??nergie atomique et aux        *)
(*                        ??nergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
logic abs_int : int -> int

axiom abs_def : (forall x:int. ((0 <= x) -> (abs_int(x) = x)))

axiom abs_def1 : (forall x:int. ((not (0 <= x)) -> (abs_int(x) = (-x))))

axiom Abs_le :
  (forall x:int. forall y:int. ((abs_int(x) <= y) -> ((-y) <= x)))

axiom Abs_le1 : (forall x:int. forall y:int. ((abs_int(x) <= y) -> (x <= y)))

axiom Abs_le2 :
  (forall x:int. forall y:int. ((((-y) <= x) and (x <= y)) ->
  (abs_int(x) <= y)))

axiom Abs_pos : (forall x:int. (0 <= abs_int(x)))

(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat ?? l'??nergie atomique et aux        *)
(*                        ??nergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
logic safe_comp_div: int, int -> int
axiom safe_comp_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_div(x,y) = x / y
logic safe_comp_mod: int, int -> int
axiom safe_comp_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_mod(x,y) = x % y
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
(** The theory int_Abs_ must be appended to this file*)
axiom Div_bound :
  (forall x:int. forall y:int. (((0 <= x) and (0 <  y)) ->
  (0 <= safe_comp_div(x,y))))

axiom Div_bound1 :
  (forall x:int. forall y:int. (((0 <= x) and (0 <  y)) ->
  (safe_comp_div(x,y) <= x)))

axiom Div_1 : (forall x:int. (safe_comp_div(x,1) = x))

axiom Mod_1 : (forall x:int. (safe_comp_mod(x,1) = 0))

axiom Div_inf :
  (forall x:int. forall y:int. (((0 <= x) and (x <  y)) ->
  (safe_comp_div(x,y) = 0)))

axiom Mod_inf :
  (forall x:int. forall y:int. (((0 <= x) and (x <  y)) ->
  (safe_comp_mod(x,y) = x)))

axiom Div_mult :
  (forall x:int. forall y:int. forall z:int [safe_comp_div(((x * y) + z),x)].
  (((0 <  x) and ((0 <= y) and (0 <= z))) ->
  (safe_comp_div(((x * y) + z),x) = (y + safe_comp_div(z,x)))))

axiom Mod_mult :
  (forall x:int. forall y:int. forall z:int [safe_comp_mod(((x * y) + z),x)].
  (((0 <  x) and ((0 <= y) and (0 <= z))) ->
  (safe_comp_mod(((x * y) + z),x) = safe_comp_mod(z,x))))

(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat ?? l'??nergie atomique et aux        *)
(*                        ??nergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(* this is a prelude for Alt-Ergo real arithmetic *)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
axiom add_div :
  (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) ->
  (((x + y) / z) = ((x / z) + (y / z)))))

axiom sub_div :
  (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) ->
  (((x - y) / z) = ((x / z) - (y / z)))))

axiom neg_div :
  (forall x:real. forall y:real. ((not (y = 0.0)) ->
  (((-x) / y) = (-(x / y)))))

axiom assoc_mul_div :
  (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) ->
  (((x * y) / z) = (x * (y / z)))))

axiom assoc_div_mul :
  (forall x:real. forall y:real. forall z:real. (((not (y = 0.0)) and
  (not (z = 0.0))) -> (((x / y) / z) = (x / (y * z)))))

axiom assoc_div_div :
  (forall x:real. forall y:real. forall z:real. (((not (y = 0.0)) and
  (not (z = 0.0))) -> ((x / (y / z)) = ((x * z) / y))))

(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat ?? l'??nergie atomique et aux        *)
(*                        ??nergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory real_Real_ must be appended to this file*)
(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat ?? l'??nergie atomique et aux        *)
(*                        ??nergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
(** The theory real_Real_ must be appended to this file*)
logic from_int : int -> real

axiom Zero : (from_int(0) = 0.0)

axiom One : (from_int(1) = 1.0)

axiom Add :
  (forall x:int. forall y:int.
  (from_int((x + y)) = (from_int(x) + from_int(y))))

axiom Sub :
  (forall x:int. forall y:int.
  (from_int((x - y)) = (from_int(x) - from_int(y))))

axiom Mul :
  (forall x:int. forall y:int.
  (from_int((x * y)) = (from_int(x) * from_int(y))))

axiom Neg : (forall x:int. (from_int((-x)) = (-from_int(x))))

(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2014                                               *)
(*    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).            *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory bool_Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
(** The theory int_Abs_ must be appended to this file*)
(** The theory int_ComputerDivision_ must be appended to this file*)
(** The theory real_Real_ must be appended to this file*)
(** The theory real_RealInfix_ must be appended to this file*)
(** The theory real_FromInt_ must be appended to this file*)
logic ite : bool, 'a, 'a -> 'a

axiom ite1 :
  (forall p:bool. forall x:'a. forall y:'a [ite(p, x, y)]. (((p = true) and
  (ite(p, x, y) = x)) or ((p = false) and (ite(p, x, y) = y))))

logic eqb : 'a, 'a -> bool

axiom eqb1 : (forall x:'a. forall y:'a. ((eqb(x, y) = true) -> (x = y)))

axiom eqb2 : (forall x:'a. forall y:'a. ((x = y) -> (eqb(x, y) = true)))

logic neqb : 'a, 'a -> bool

axiom neqb1 :
  (forall x:'a. forall y:'a. ((neqb(x, y) = true) -> (not (x = y))))

axiom neqb2 :
  (forall x:'a. forall y:'a. ((not (x = y)) -> (neqb(x, y) = true)))

logic zlt : int, int -> bool

logic zleq : int, int -> bool

axiom zlt1 : (forall x:int. forall y:int. ((zlt(x, y) = true) -> (x <  y)))

axiom zlt2 : (forall x:int. forall y:int. ((x <  y) -> (zlt(x, y) = true)))

axiom zleq1 : (forall x:int. forall y:int. ((zleq(x, y) = true) -> (x <= y)))

axiom zleq2 : (forall x:int. forall y:int. ((x <= y) -> (zleq(x, y) = true)))

logic rlt : real, real -> bool

logic rleq : real, real -> bool

axiom rlt1 : (forall x:real. forall y:real. ((rlt(x, y) = true) -> (x <  y)))

axiom rlt2 : (forall x:real. forall y:real. ((x <  y) -> (rlt(x, y) = true)))

axiom rleq1 :
  (forall x:real. forall y:real. ((rleq(x, y) = true) -> (x <= y)))

axiom rleq2 :
  (forall x:real. forall y:real. ((x <= y) -> (rleq(x, y) = true)))

logic truncate : real -> int

function real_of_int(x: int) : real = from_int(x)

axiom truncate_of_int : (forall x:int. (truncate(real_of_int(x)) = x))

axiom c_euclidian :
  (forall n:int. forall d:int [safe_comp_div(n,d), safe_comp_mod(n,d)].
  ((not (d = 0)) -> (n = ((safe_comp_div(n,d) * d) + safe_comp_mod(n,d)))))

axiom cdiv_cases :
  (forall n:int. forall d:int [safe_comp_div(n,d)]. ((0 <= n) -> ((0 <  d) ->
  (safe_comp_div(n,d) = (n / d)))))

axiom cdiv_cases1 :
  (forall n:int. forall d:int [safe_comp_div(n,d)]. ((n <= 0) -> ((0 <  d) ->
  (safe_comp_div(n,d) = (-((-n) / d))))))

axiom cdiv_cases2 :
  (forall n:int. forall d:int [safe_comp_div(n,d)]. ((0 <= n) -> ((d <  0) ->
  (safe_comp_div(n,d) = (-(n / (-d)))))))

axiom cdiv_cases3 :
  (forall n:int. forall d:int [safe_comp_div(n,d)]. ((n <= 0) -> ((d <  0) ->
  (safe_comp_div(n,d) = ((-n) / (-d))))))

axiom cmod_cases :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((0 <  d) ->
  (safe_comp_mod(n,d) = (n % d)))))

axiom cmod_cases1 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((0 <  d) ->
  (safe_comp_mod(n,d) = (-((-n) % d))))))

axiom cmod_cases2 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((d <  0) ->
  (safe_comp_mod(n,d) = (n % (-d))))))

axiom cmod_cases3 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((d <  0) ->
  (safe_comp_mod(n,d) = (-((-n) % (-d)))))))

axiom cmod_remainder :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((0 <  d) ->
  (0 <= safe_comp_mod(n,d)))))

axiom cmod_remainder1 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((0 <  d) ->
  (safe_comp_mod(n,d) <  d))))

axiom cmod_remainder2 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((0 <  d) ->
  ((-d) <  safe_comp_mod(n,d)))))

axiom cmod_remainder3 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((0 <  d) ->
  (safe_comp_mod(n,d) <= 0))))

axiom cmod_remainder4 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((d <  0) ->
  (0 <= safe_comp_mod(n,d)))))

axiom cmod_remainder5 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((d <  0) ->
  (safe_comp_mod(n,d) <  (-d)))))

axiom cmod_remainder6 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((d <  0) ->
  (d <  safe_comp_mod(n,d)))))

axiom cmod_remainder7 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((d <  0) ->
  (safe_comp_mod(n,d) <= 0))))

axiom cdiv_neutral :
  (forall a:int [safe_comp_div(a,1)]. (safe_comp_div(a,1) = a))

axiom cdiv_inv :
  (forall a:int [safe_comp_div(a,a)]. ((not (a = 0)) ->
  (safe_comp_div(a,a) = 1)))

(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2014                                               *)
(*    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).            *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory bool_Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
(** The theory map_Map_ must be appended to this file*)
type addr = { base : int; offset : int
}

logic addr_le : addr, addr -> prop

logic addr_lt : addr, addr -> prop

logic addr_le_bool : addr, addr -> bool

logic addr_lt_bool : addr, addr -> bool

axiom addr_le_def :
  (forall p:addr. forall q:addr [addr_le(p, q)]. (((p).base = (q).base) ->
  (addr_le(p, q) -> ((p).offset <= (q).offset))))

axiom addr_le_def1 :
  (forall p:addr. forall q:addr [addr_le(p, q)]. (((p).base = (q).base) ->
  (((p).offset <= (q).offset) -> addr_le(p, q))))

axiom addr_lt_def :
  (forall p:addr. forall q:addr [addr_lt(p, q)]. (((p).base = (q).base) ->
  (addr_lt(p, q) -> ((p).offset <  (q).offset))))

axiom addr_lt_def1 :
  (forall p:addr. forall q:addr [addr_lt(p, q)]. (((p).base = (q).base) ->
  (((p).offset <  (q).offset) -> addr_lt(p, q))))

axiom addr_le_bool_def :
  (forall p:addr. forall q:addr [addr_le_bool(p, q)]. (addr_le(p, q) ->
  (addr_le_bool(p, q) = true)))

axiom addr_le_bool_def1 :
  (forall p:addr. forall q:addr [addr_le_bool(p, q)]. ((addr_le_bool(p,
  q) = true) -> addr_le(p, q)))

axiom addr_lt_bool_def :
  (forall p:addr. forall q:addr [addr_lt_bool(p, q)]. (addr_lt(p, q) ->
  (addr_lt_bool(p, q) = true)))

axiom addr_lt_bool_def1 :
  (forall p:addr. forall q:addr [addr_lt_bool(p, q)]. ((addr_lt_bool(p,
  q) = true) -> addr_lt(p, q)))

function null() : addr = { base = 0; offset = 0 }

function global(b: int) : addr = { base = b; offset = 0 }

function shift(p: addr, k: int) : addr = { base = (p).base; offset =
  ((p).offset + k) }

predicate included(p: addr, a: int, q: addr, b: int) = ((0 <  a) ->
  ((0 <= b) and (((p).base = (q).base) and (((q).offset <= (p).offset) and
  (((p).offset + a) <= ((q).offset + b))))))

predicate separated(p: addr, a: int, q: addr, b: int) = ((a <= 0) or
  ((b <= 0) or ((not ((p).base = (q).base)) or
  ((((q).offset + b) <= (p).offset) or (((p).offset + a) <= (q).offset)))))

predicate eqmem(m1: (addr,'a) farray, m2: (addr,'a) farray, p: addr,
  a1: int) =
  (forall q:addr [(m1[p])| (m2[q])]. (included(q, 1, p, a1) ->
  ((m1[q]) = (m2[q]))))

predicate havoc(m1: (addr,'a) farray, m2: (addr,'a) farray, p: addr,
  a1: int) =
  (forall q:addr [(m1[p])| (m2[q])]. (separated(q, 1, p, a1) ->
  ((m1[q]) = (m2[q]))))

predicate valid_rd(m: (int,int) farray, p: addr, n: int) = ((0 <  n) ->
  ((0 <= (p).offset) and (((p).offset + n) <= (m[(p).base]))))

predicate valid_rw(m: (int,int) farray, p: addr, n: int) = ((0 <  n) ->
  ((0 <  (p).base) and ((0 <= (p).offset) and
  (((p).offset + n) <= (m[(p).base])))))

axiom valid_rw_rd :
  (forall m:(int,int) farray.
  (forall p:addr. (forall n:int. (valid_rw(m, p, n) -> valid_rd(m, p, n)))))

axiom valid_string :
  (forall m:(int,int) farray.
  (forall p:addr. (((p).base <  0) -> (((0 <= (p).offset) and
  ((p).offset <  (m[(p).base]))) -> valid_rd(m, p, 1)))))

axiom valid_string1 :
  (forall m:(int,int) farray.
  (forall p:addr. (((p).base <  0) -> (((0 <= (p).offset) and
  ((p).offset <  (m[(p).base]))) -> (not valid_rw(m, p, 1))))))

axiom separated_1 :
  (forall p:addr. forall q:addr.
  (forall a:int. forall b:int. forall i:int. forall j:int [separated(p, a, q,
  b), { base = (p).base; offset = i }, { base = (q).base; offset = j }].
  (separated(p, a, q, b) -> ((((p).offset <= i) and
  (i <  ((p).offset + a))) -> ((((q).offset <= j) and
  (j <  ((q).offset + b))) -> (not ({ base = (p).base; offset = i } = {
  base = (q).base; offset = j })))))))

logic region : int -> int

logic linked : (int,int) farray -> prop

logic sconst : (addr,int) farray -> prop

predicate framed(m: (addr,addr) farray) =
  (forall p:addr [(m[p])]. (region(((m[p])).base) <= 0))

axiom separated_included :
  (forall p:addr. forall q:addr.
  (forall a:int. forall b:int [separated(p, a, q, b), included(p, a, q, b)].
  ((0 <  a) -> ((0 <  b) -> (separated(p, a, q, b) -> (not included(p, a, q,
  b)))))))

axiom included_trans :
  (forall p:addr. forall q:addr. forall r:addr.
  (forall a:int. forall b:int. forall c:int [included(p, a, q, b),
  included(q, b, r, c)]. (included(p, a, q, b) -> (included(q, b, r, c) ->
  included(p, a, r, c)))))

axiom separated_trans :
  (forall p:addr. forall q:addr. forall r:addr.
  (forall a:int. forall b:int. forall c:int [included(p, a, q, b),
  separated(q, b, r, c)]. (included(p, a, q, b) -> (separated(q, b, r, c) ->
  separated(p, a, r, c)))))

axiom separated_sym :
  (forall p:addr. forall q:addr.
  (forall a:int. forall b:int [separated(p, a, q, b)]. (separated(p, a, q,
  b) -> separated(q, b, p, a))))

axiom separated_sym1 :
  (forall p:addr. forall q:addr.
  (forall a:int. forall b:int [separated(p, a, q, b)]. (separated(q, b, p,
  a) -> separated(p, a, q, b))))

axiom eqmem_included :
  (forall m1:(addr,'a) farray. forall m2:(addr,'a) farray.
  (forall p:addr. forall q:addr.
  (forall a1:int. forall b:int [eqmem(m1, m2, p, a1), eqmem(m1, m2, q, b)].
  (included(p, a1, q, b) -> (eqmem(m1, m2, q, b) -> eqmem(m1, m2, p, a1))))))

axiom eqmem_sym :
  (forall m1:(addr,'a) farray. forall m2:(addr,'a) farray.
  (forall p:addr.
  (forall a1:int. (eqmem(m1, m2, p, a1) -> eqmem(m2, m1, p, a1)))))

axiom havoc_sym :
  (forall m1:(addr,'a) farray. forall m2:(addr,'a) farray.
  (forall p:addr.
  (forall a1:int. (havoc(m1, m2, p, a1) -> havoc(m2, m1, p, a1)))))

logic cast : addr -> int

axiom cast_injective :
  (forall p:addr. forall q:addr [cast(p), cast(q)]. ((cast(p) = cast(q)) ->
  (p = q)))

logic hardware : int -> int

axiom hardnull : (hardware(0) = 0)

(* ---------------------------------------------------------- *)
(* --- Post-condition (file null_pointer.c, line 12) in 'function' --- *)
(* ---------------------------------------------------------- *)

goal function_post_3:
  forall Malloc_0 : int farray.
  forall var_ptr_0 : addr.
  linked(Malloc_0) ->
  (not valid_rw(Malloc_0, var_ptr_0, 1))

-------------- next part --------------
(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat ?? l'??nergie atomique et aux        *)
(*                        ??nergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(* this is a prelude for Alt-Ergo integer arithmetic *)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat ?? l'??nergie atomique et aux        *)
(*                        ??nergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
logic abs_int : int -> int

axiom abs_def : (forall x:int. ((0 <= x) -> (abs_int(x) = x)))

axiom abs_def1 : (forall x:int. ((not (0 <= x)) -> (abs_int(x) = (-x))))

axiom Abs_le :
  (forall x:int. forall y:int. ((abs_int(x) <= y) -> ((-y) <= x)))

axiom Abs_le1 : (forall x:int. forall y:int. ((abs_int(x) <= y) -> (x <= y)))

axiom Abs_le2 :
  (forall x:int. forall y:int. ((((-y) <= x) and (x <= y)) ->
  (abs_int(x) <= y)))

axiom Abs_pos : (forall x:int. (0 <= abs_int(x)))

(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat ?? l'??nergie atomique et aux        *)
(*                        ??nergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
logic safe_comp_div: int, int -> int
axiom safe_comp_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_div(x,y) = x / y
logic safe_comp_mod: int, int -> int
axiom safe_comp_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_mod(x,y) = x % y
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
(** The theory int_Abs_ must be appended to this file*)
axiom Div_bound :
  (forall x:int. forall y:int. (((0 <= x) and (0 <  y)) ->
  (0 <= safe_comp_div(x,y))))

axiom Div_bound1 :
  (forall x:int. forall y:int. (((0 <= x) and (0 <  y)) ->
  (safe_comp_div(x,y) <= x)))

axiom Div_1 : (forall x:int. (safe_comp_div(x,1) = x))

axiom Mod_1 : (forall x:int. (safe_comp_mod(x,1) = 0))

axiom Div_inf :
  (forall x:int. forall y:int. (((0 <= x) and (x <  y)) ->
  (safe_comp_div(x,y) = 0)))

axiom Mod_inf :
  (forall x:int. forall y:int. (((0 <= x) and (x <  y)) ->
  (safe_comp_mod(x,y) = x)))

axiom Div_mult :
  (forall x:int. forall y:int. forall z:int [safe_comp_div(((x * y) + z),x)].
  (((0 <  x) and ((0 <= y) and (0 <= z))) ->
  (safe_comp_div(((x * y) + z),x) = (y + safe_comp_div(z,x)))))

axiom Mod_mult :
  (forall x:int. forall y:int. forall z:int [safe_comp_mod(((x * y) + z),x)].
  (((0 <  x) and ((0 <= y) and (0 <= z))) ->
  (safe_comp_mod(((x * y) + z),x) = safe_comp_mod(z,x))))

(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat ?? l'??nergie atomique et aux        *)
(*                        ??nergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(* this is a prelude for Alt-Ergo real arithmetic *)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
axiom add_div :
  (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) ->
  (((x + y) / z) = ((x / z) + (y / z)))))

axiom sub_div :
  (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) ->
  (((x - y) / z) = ((x / z) - (y / z)))))

axiom neg_div :
  (forall x:real. forall y:real. ((not (y = 0.0)) ->
  (((-x) / y) = (-(x / y)))))

axiom assoc_mul_div :
  (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) ->
  (((x * y) / z) = (x * (y / z)))))

axiom assoc_div_mul :
  (forall x:real. forall y:real. forall z:real. (((not (y = 0.0)) and
  (not (z = 0.0))) -> (((x / y) / z) = (x / (y * z)))))

axiom assoc_div_div :
  (forall x:real. forall y:real. forall z:real. (((not (y = 0.0)) and
  (not (z = 0.0))) -> ((x / (y / z)) = ((x * z) / y))))

(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat ?? l'??nergie atomique et aux        *)
(*                        ??nergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory real_Real_ must be appended to this file*)
(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat ?? l'??nergie atomique et aux        *)
(*                        ??nergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
(** The theory real_Real_ must be appended to this file*)
logic from_int : int -> real

axiom Zero : (from_int(0) = 0.0)

axiom One : (from_int(1) = 1.0)

axiom Add :
  (forall x:int. forall y:int.
  (from_int((x + y)) = (from_int(x) + from_int(y))))

axiom Sub :
  (forall x:int. forall y:int.
  (from_int((x - y)) = (from_int(x) - from_int(y))))

axiom Mul :
  (forall x:int. forall y:int.
  (from_int((x * y)) = (from_int(x) * from_int(y))))

axiom Neg : (forall x:int. (from_int((-x)) = (-from_int(x))))

(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2014                                               *)
(*    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).            *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory bool_Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
(** The theory int_Abs_ must be appended to this file*)
(** The theory int_ComputerDivision_ must be appended to this file*)
(** The theory real_Real_ must be appended to this file*)
(** The theory real_RealInfix_ must be appended to this file*)
(** The theory real_FromInt_ must be appended to this file*)
logic ite : bool, 'a, 'a -> 'a

axiom ite1 :
  (forall p:bool. forall x:'a. forall y:'a [ite(p, x, y)]. (((p = true) and
  (ite(p, x, y) = x)) or ((p = false) and (ite(p, x, y) = y))))

logic eqb : 'a, 'a -> bool

axiom eqb1 : (forall x:'a. forall y:'a. ((eqb(x, y) = true) -> (x = y)))

axiom eqb2 : (forall x:'a. forall y:'a. ((x = y) -> (eqb(x, y) = true)))

logic neqb : 'a, 'a -> bool

axiom neqb1 :
  (forall x:'a. forall y:'a. ((neqb(x, y) = true) -> (not (x = y))))

axiom neqb2 :
  (forall x:'a. forall y:'a. ((not (x = y)) -> (neqb(x, y) = true)))

logic zlt : int, int -> bool

logic zleq : int, int -> bool

axiom zlt1 : (forall x:int. forall y:int. ((zlt(x, y) = true) -> (x <  y)))

axiom zlt2 : (forall x:int. forall y:int. ((x <  y) -> (zlt(x, y) = true)))

axiom zleq1 : (forall x:int. forall y:int. ((zleq(x, y) = true) -> (x <= y)))

axiom zleq2 : (forall x:int. forall y:int. ((x <= y) -> (zleq(x, y) = true)))

logic rlt : real, real -> bool

logic rleq : real, real -> bool

axiom rlt1 : (forall x:real. forall y:real. ((rlt(x, y) = true) -> (x <  y)))

axiom rlt2 : (forall x:real. forall y:real. ((x <  y) -> (rlt(x, y) = true)))

axiom rleq1 :
  (forall x:real. forall y:real. ((rleq(x, y) = true) -> (x <= y)))

axiom rleq2 :
  (forall x:real. forall y:real. ((x <= y) -> (rleq(x, y) = true)))

logic truncate : real -> int

function real_of_int(x: int) : real = from_int(x)

axiom truncate_of_int : (forall x:int. (truncate(real_of_int(x)) = x))

axiom c_euclidian :
  (forall n:int. forall d:int [safe_comp_div(n,d), safe_comp_mod(n,d)].
  ((not (d = 0)) -> (n = ((safe_comp_div(n,d) * d) + safe_comp_mod(n,d)))))

axiom cdiv_cases :
  (forall n:int. forall d:int [safe_comp_div(n,d)]. ((0 <= n) -> ((0 <  d) ->
  (safe_comp_div(n,d) = (n / d)))))

axiom cdiv_cases1 :
  (forall n:int. forall d:int [safe_comp_div(n,d)]. ((n <= 0) -> ((0 <  d) ->
  (safe_comp_div(n,d) = (-((-n) / d))))))

axiom cdiv_cases2 :
  (forall n:int. forall d:int [safe_comp_div(n,d)]. ((0 <= n) -> ((d <  0) ->
  (safe_comp_div(n,d) = (-(n / (-d)))))))

axiom cdiv_cases3 :
  (forall n:int. forall d:int [safe_comp_div(n,d)]. ((n <= 0) -> ((d <  0) ->
  (safe_comp_div(n,d) = ((-n) / (-d))))))

axiom cmod_cases :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((0 <  d) ->
  (safe_comp_mod(n,d) = (n % d)))))

axiom cmod_cases1 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((0 <  d) ->
  (safe_comp_mod(n,d) = (-((-n) % d))))))

axiom cmod_cases2 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((d <  0) ->
  (safe_comp_mod(n,d) = (n % (-d))))))

axiom cmod_cases3 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((d <  0) ->
  (safe_comp_mod(n,d) = (-((-n) % (-d)))))))

axiom cmod_remainder :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((0 <  d) ->
  (0 <= safe_comp_mod(n,d)))))

axiom cmod_remainder1 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((0 <  d) ->
  (safe_comp_mod(n,d) <  d))))

axiom cmod_remainder2 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((0 <  d) ->
  ((-d) <  safe_comp_mod(n,d)))))

axiom cmod_remainder3 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((0 <  d) ->
  (safe_comp_mod(n,d) <= 0))))

axiom cmod_remainder4 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((d <  0) ->
  (0 <= safe_comp_mod(n,d)))))

axiom cmod_remainder5 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((d <  0) ->
  (safe_comp_mod(n,d) <  (-d)))))

axiom cmod_remainder6 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((d <  0) ->
  (d <  safe_comp_mod(n,d)))))

axiom cmod_remainder7 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((d <  0) ->
  (safe_comp_mod(n,d) <= 0))))

axiom cdiv_neutral :
  (forall a:int [safe_comp_div(a,1)]. (safe_comp_div(a,1) = a))

axiom cdiv_inv :
  (forall a:int [safe_comp_div(a,a)]. ((not (a = 0)) ->
  (safe_comp_div(a,a) = 1)))

(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2014                                               *)
(*    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).            *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory bool_Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
(** The theory map_Map_ must be appended to this file*)
type addr = { base : int; offset : int
}

logic addr_le : addr, addr -> prop

logic addr_lt : addr, addr -> prop

logic addr_le_bool : addr, addr -> bool

logic addr_lt_bool : addr, addr -> bool

axiom addr_le_def :
  (forall p:addr. forall q:addr [addr_le(p, q)]. (((p).base = (q).base) ->
  (addr_le(p, q) -> ((p).offset <= (q).offset))))

axiom addr_le_def1 :
  (forall p:addr. forall q:addr [addr_le(p, q)]. (((p).base = (q).base) ->
  (((p).offset <= (q).offset) -> addr_le(p, q))))

axiom addr_lt_def :
  (forall p:addr. forall q:addr [addr_lt(p, q)]. (((p).base = (q).base) ->
  (addr_lt(p, q) -> ((p).offset <  (q).offset))))

axiom addr_lt_def1 :
  (forall p:addr. forall q:addr [addr_lt(p, q)]. (((p).base = (q).base) ->
  (((p).offset <  (q).offset) -> addr_lt(p, q))))

axiom addr_le_bool_def :
  (forall p:addr. forall q:addr [addr_le_bool(p, q)]. (addr_le(p, q) ->
  (addr_le_bool(p, q) = true)))

axiom addr_le_bool_def1 :
  (forall p:addr. forall q:addr [addr_le_bool(p, q)]. ((addr_le_bool(p,
  q) = true) -> addr_le(p, q)))

axiom addr_lt_bool_def :
  (forall p:addr. forall q:addr [addr_lt_bool(p, q)]. (addr_lt(p, q) ->
  (addr_lt_bool(p, q) = true)))

axiom addr_lt_bool_def1 :
  (forall p:addr. forall q:addr [addr_lt_bool(p, q)]. ((addr_lt_bool(p,
  q) = true) -> addr_lt(p, q)))

function null() : addr = { base = 0; offset = 0 }

function global(b: int) : addr = { base = b; offset = 0 }

function shift(p: addr, k: int) : addr = { base = (p).base; offset =
  ((p).offset + k) }

predicate included(p: addr, a: int, q: addr, b: int) = ((0 <  a) ->
  ((0 <= b) and (((p).base = (q).base) and (((q).offset <= (p).offset) and
  (((p).offset + a) <= ((q).offset + b))))))

predicate separated(p: addr, a: int, q: addr, b: int) = ((a <= 0) or
  ((b <= 0) or ((not ((p).base = (q).base)) or
  ((((q).offset + b) <= (p).offset) or (((p).offset + a) <= (q).offset)))))

predicate eqmem(m1: (addr,'a) farray, m2: (addr,'a) farray, p: addr,
  a1: int) =
  (forall q:addr [(m1[p])| (m2[q])]. (included(q, 1, p, a1) ->
  ((m1[q]) = (m2[q]))))

predicate havoc(m1: (addr,'a) farray, m2: (addr,'a) farray, p: addr,
  a1: int) =
  (forall q:addr [(m1[p])| (m2[q])]. (separated(q, 1, p, a1) ->
  ((m1[q]) = (m2[q]))))

predicate valid_rd(m: (int,int) farray, p: addr, n: int) = ((0 <  n) ->
  ((0 <= (p).offset) and (((p).offset + n) <= (m[(p).base]))))

predicate valid_rw(m: (int,int) farray, p: addr, n: int) = ((0 <  n) ->
  ((0 <  (p).base) and ((0 <= (p).offset) and
  (((p).offset + n) <= (m[(p).base])))))

axiom valid_rw_rd :
  (forall m:(int,int) farray.
  (forall p:addr. (forall n:int. (valid_rw(m, p, n) -> valid_rd(m, p, n)))))

axiom valid_string :
  (forall m:(int,int) farray.
  (forall p:addr. (((p).base <  0) -> (((0 <= (p).offset) and
  ((p).offset <  (m[(p).base]))) -> valid_rd(m, p, 1)))))

axiom valid_string1 :
  (forall m:(int,int) farray.
  (forall p:addr. (((p).base <  0) -> (((0 <= (p).offset) and
  ((p).offset <  (m[(p).base]))) -> (not valid_rw(m, p, 1))))))

axiom separated_1 :
  (forall p:addr. forall q:addr.
  (forall a:int. forall b:int. forall i:int. forall j:int [separated(p, a, q,
  b), { base = (p).base; offset = i }, { base = (q).base; offset = j }].
  (separated(p, a, q, b) -> ((((p).offset <= i) and
  (i <  ((p).offset + a))) -> ((((q).offset <= j) and
  (j <  ((q).offset + b))) -> (not ({ base = (p).base; offset = i } = {
  base = (q).base; offset = j })))))))

logic region : int -> int

logic linked : (int,int) farray -> prop

logic sconst : (addr,int) farray -> prop

predicate framed(m: (addr,addr) farray) =
  (forall p:addr [(m[p])]. (region(((m[p])).base) <= 0))

axiom separated_included :
  (forall p:addr. forall q:addr.
  (forall a:int. forall b:int [separated(p, a, q, b), included(p, a, q, b)].
  ((0 <  a) -> ((0 <  b) -> (separated(p, a, q, b) -> (not included(p, a, q,
  b)))))))

axiom included_trans :
  (forall p:addr. forall q:addr. forall r:addr.
  (forall a:int. forall b:int. forall c:int [included(p, a, q, b),
  included(q, b, r, c)]. (included(p, a, q, b) -> (included(q, b, r, c) ->
  included(p, a, r, c)))))

axiom separated_trans :
  (forall p:addr. forall q:addr. forall r:addr.
  (forall a:int. forall b:int. forall c:int [included(p, a, q, b),
  separated(q, b, r, c)]. (included(p, a, q, b) -> (separated(q, b, r, c) ->
  separated(p, a, r, c)))))

axiom separated_sym :
  (forall p:addr. forall q:addr.
  (forall a:int. forall b:int [separated(p, a, q, b)]. (separated(p, a, q,
  b) -> separated(q, b, p, a))))

axiom separated_sym1 :
  (forall p:addr. forall q:addr.
  (forall a:int. forall b:int [separated(p, a, q, b)]. (separated(q, b, p,
  a) -> separated(p, a, q, b))))

axiom eqmem_included :
  (forall m1:(addr,'a) farray. forall m2:(addr,'a) farray.
  (forall p:addr. forall q:addr.
  (forall a1:int. forall b:int [eqmem(m1, m2, p, a1), eqmem(m1, m2, q, b)].
  (included(p, a1, q, b) -> (eqmem(m1, m2, q, b) -> eqmem(m1, m2, p, a1))))))

axiom eqmem_sym :
  (forall m1:(addr,'a) farray. forall m2:(addr,'a) farray.
  (forall p:addr.
  (forall a1:int. (eqmem(m1, m2, p, a1) -> eqmem(m2, m1, p, a1)))))

axiom havoc_sym :
  (forall m1:(addr,'a) farray. forall m2:(addr,'a) farray.
  (forall p:addr.
  (forall a1:int. (havoc(m1, m2, p, a1) -> havoc(m2, m1, p, a1)))))

logic cast : addr -> int

axiom cast_injective :
  (forall p:addr. forall q:addr [cast(p), cast(q)]. ((cast(p) = cast(q)) ->
  (p = q)))

logic hardware : int -> int

axiom hardnull : (hardware(0) = 0)

(* ---------------------------------------------------------- *)
(* --- Post-condition (file null_pointer.c, line 10) in 'function' --- *)
(* ---------------------------------------------------------- *)

goal function_post: forall Malloc_0 : int farray. not linked(Malloc_0)

-------------- next part --------------
/*
 * Unexpected results shown below are obtained by running -wp
*/
#include <stddef.h>

int *var_ptr;

/*@
    assigns var_ptr;            // Valid
    ensures var_ptr == NULL;    // Unknown
    ensures var_ptr == \null;   // Unknown
    ensures !\valid(var_ptr);   // Unknown
*/
void function(){
    var_ptr = NULL;
}

void main(){
    function();
}