(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2010                                               *)
(*    CEA   (Commissariat  l'nergie atomique et aux nergies            *)
(*           alternatives)                                                *)
(*    INRIA (Institut National de Recherche en Informatique et en         *)
(*           Automatique)                                                 *)
(*                                                                        *)
(*  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 v2.1                *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)


logic dummy_prop : prop

(**************************************************************************)
(*** Specification of Identifiers                                       ***)
(**************************************************************************)

type name

logic mk_name : int -> name
axiom uniq_name : 
 forall i,j:int. mk_name(i)=mk_name(j) <-> i=j

(* Alternative specification *)
(*
type name 
type id 
logic get_name_id : name -> id

axiom same_name: 
 forall i,j: int. 
 get_name_id(x) = get_name_id(y) -> x = y

axiom neq_name: 
 forall i,j: int. 
 get_name_id(x) <> get_name_id(y) -> x <> y
*)


(**************************************************************************)
(*** Specification of Set as First Class Value                          ***)
(**************************************************************************)
(* From Figure 2.6 in ACSL:ANSI/ISO C Specification Language *)


type 'a set

logic empty : 'a set
logic singleton : 'a -> 'a set
logic range : int,int -> int set
logic union : 'a set , 'a set -> 'a set
logic inter : 'a set , 'a set -> 'a set
logic plus_int : int set, int set -> int set
logic subset : 'a set,'a set -> prop
logic range_inf: int -> int set
logic range_sup:int->int set
logic integers_set : int set
logic equiv : 'a set ,'a set -> prop
logic member : 'a,'a set -> prop 

axiom singleton_def :  
 forall x:'a. member (x, singleton(x))  

axiom singleton_eq: 
      forall x,y:'a. member(x,singleton(y)) -> x=y

axiom union_member : 
 forall x:'a. forall s1,s2:'a set. 
  member(x, union(s1,s2)) <-> member(x,s1) or member(x,s2)

axiom union_of_empty : 
 forall x:'a set. union(x,empty) = x 

axiom inter_of_empty : 
 forall x:'a set. inter(x,empty) = empty

axiom union_comm : 
 forall x,y:'a set. union(x,y) = union(y,x)

axiom inter_comm : 
 forall x,y:'a set. inter(x,y) = inter(y,x) 

axiom inter_member : 
 forall x:'a. forall s1,s2:'a set. 
  member(x,inter(s1,s2)) <-> member(x,s1) and member(x,s2)

axiom plus_int_member_1: 
  forall sa,sb:int set. 
  (forall a,b:int.
        member(a,sa) and member(b,sb) -> member((a+b), plus_int(sa,sb)))

axiom plus_int_member_2: 
  forall sa,sb:int set.
  (forall c:int. 
      member(c,plus_int(sa,sb)) -> 
       exists a:int. exists b:int. 
        member(a,sa) and member(b,sb) and c=a+b) 

axiom subset_empty : 
 forall sa:'a set. subset(empty,sa)

axiom subset_sym: 
 forall sa:'a set. subset(sa,sa)

axiom subset_trans : 
 forall sa,sb,sc: 'a set. 
    subset(sa,sb) -> 
    subset(sb,sc) ->
    subset(sa,sc)

axiom subset_def: 
 forall sa,sb:'a set. 
  (forall a:'a. member(a,sa) -> member(a,sb)) <-> subset(sa,sb) 

axiom range_def: 
 forall i,j:int.
   forall k: int. i <= k<= j -> member (k,range(i,j)) 

axiom range_inf_def: (* range_inf(i) is [ i .. ] *)
 forall i: int. 
   forall k: int. i <= k -> member (k,range_inf(i))

axiom range_sup_def: (* range_sup(j) is [ .. j ] *)
 forall j: int. 
   forall k: int. k <= j -> member (k,range_sup(j))

axiom integers_set_def: 
 forall k:int. k >= 0 -> member(k,integers_set) 

axiom equiv_def: 
 forall s1,s2:'a set. (
 (forall a:'a. member(a,s1) -> member(a,s2)) and
   (forall b:'a. member(b,s2) -> member(b,s1))) <->
 equiv(s1,s2)

axiom equiv_refl: 
 forall s:'a set. equiv(s,s) 

axiom equiv_sym: 
 forall s1,s2:'a set. equiv(s1,s2) -> equiv(s2,s1)

axiom equiv_trans: 
 forall s1,s2,s3:'a set. 
  equiv(s1,s2) -> equiv(s2,s3) -> equiv(s1,s3)



(**************************************************************************)
(*** Specification of Record as First Class Value                       ***)
(**************************************************************************)

type record
type urecord
type pointer
type 'a format

logic int_format: int format
logic real_format : real format
logic record_format : name -> record format
logic union_format : name -> urecord format
logic array_format : int , 'a format -> 'a farray format
logic pointer_format : pointer format

logic data_get_field: record,name,'a format -> 'a 
logic data_set_field: record,name,'a format,'a -> record
logic eq_struct: name,record,record -> prop
logic eq_struct_bool:name,record,record -> bool
logic eq_union: name,urecord,urecord -> prop
logic eq_union_bool:name,urecord,urecord -> bool

logic data_get_ufield: urecord,name,'a format -> 'a 
logic data_set_ufield: urecord,name,'a format,'a -> urecord

axiom eq_struct_refl: 
 forall s:name.
 forall r:record. eq_struct(s,r,r) 

axiom eq_struct_trans: 
 forall r1,r2,r3:record. 
  forall s:name.
   eq_struct(s,r1,r2) ->
   eq_struct(s,r2,r3) ->
   eq_struct(s,r1,r3)

axiom eq_struct_bool_refl: 
 forall s:name.
 forall r:record. eq_struct_bool(s,r,r)=true 

axiom eq_struct_bool_trans: 
 forall r1,r2,r3:record. 
  forall s:name.
   eq_struct_bool(s,r1,r2) = true ->
   eq_struct_bool(s,r2,r3) = true ->
   eq_struct_bool(s,r1,r3) = true

axiom eq_struct_bool_eq_struct: 
 forall s:name. forall r,r':record. 
   eq_struct_bool(s,r,r')=true <-> eq_struct(s,r,r')


axiom eq_union_trans: 
 forall r1,r2,r3:urecord. 
  forall s:name.
   eq_union(s,r1,r2) ->
   eq_union(s,r2,r3) ->
   eq_union(s,r1,r3)

axiom eq_union_bool_refl: 
 forall s:name.
 forall r:urecord. eq_union_bool(s,r,r)=true 

axiom eq_union_bool_trans: 
 forall r1,r2,r3:urecord. 
  forall s:name.
   eq_union_bool(s,r1,r2) = true ->
   eq_union_bool(s,r2,r3) = true ->
   eq_union_bool(s,r1,r3) = true

axiom eq_union_bool_eq_struct: 
 forall s:name. forall r,r':urecord. 
   eq_union_bool(s,r,r')=true <-> eq_union(s,r,r')

axiom get_set_record_same: 
 forall r: record. 
  forall f:name. forall dt :'a format.
   forall v:'a.
    data_get_field(data_set_field(r,f,dt,v),f,dt) = v



axiom get_set_record_other: 
 forall r: record. 
  forall f1: name. forall dt1: 'a format. 
  forall f2: name. forall dt2: 'b format.
    forall v:'a.
    f1<>f2 ->
    data_get_field(data_set_field(r,f1,dt1,v),f2,dt2) = 
    data_get_field(r,f2,dt2)

axiom get_set_urecord_same: 
  forall u: urecord.  forall f:name. forall dt :'a format. forall v:'a.
    data_get_ufield(data_set_ufield(u, f,dt,v),f,dt) = v
 
(**************************************************************************)
(*** Specification of Array as First Class Value-                       ***)
(*** -Additional to arrays.why                                          ***)
(**************************************************************************)

logic eq_array:'a farray,'a farray, int ->prop
logic eq_array_bool:'a farray,'a farray, int ->bool

axiom eq_array_def: 
 forall t1,t2:'a farray. 
  forall dim:int. 
   eq_array(t1,t2,dim) <->
    (forall i:int. 0<=i<dim -> access(t1,i)=access(t2,i))

axiom eq_arra_bool_eq_array: 
 forall t1,t2 : 'a farray. 
  forall dim:int. 
   eq_array(t1,t2,dim) <-> eq_array_bool(t1,t2,dim)=true


logic get_range_index: 'a farray , int set -> 'a set
logic set_range_index: 'a farray , int set -> 'a farray

axiom get_range_def : 
 forall t: 'a farray. 
  forall rg: int set. 
    forall i: int. 
    member (i,rg) <-> member(access(t,i),(get_range_index(t,rg))) 

axiom set_range_def :
 forall t: 'a farray. 
  forall rg: int set. 
     forall i:int. not (member(i,rg)) <-> 
     access(set_range_index(t,rg),i) = access(t,i)


(**************************************************************************)
(*** Integer Cast into Machine                                          ***)
(**************************************************************************) 

(** Is a mutiple cf Zdivide of Coq Std lib*)
logic is_mult : int,int -> prop

axiom is_mult_def: 
 forall x,y: int. is_mult(x,y) <-> exists z:int. y = x*z

axiom is_mult_refl: 
 forall x:int. is_mult(x,x)

axiom is_mult_one: 
 forall x:int. is_mult(1,x)

axiom is_mult_zero: 
 forall x:int. is_mult(x,0)

axiom is_mult_mult_left: 
 forall a,b,c:int. 
  is_mult(a,b) -> is_mult (c*a,c*b)

axiom is_mult_right: 
 forall a,b,c:int. 
  is_mult(a,b) -> is_mult(a*c,b*c)

axiom is_mult_plus_right: 
 forall a,b,c:int. 
 is_mult(a,b) -> is_mult(a,c) -> is_mult(a,b+c)

axiom is_mult_opp_right: 
 forall a,b: int. is_mult(a,b) <-> is_mult(a,-b)

axiom is_mult_opp_left: 
 forall a,b: int. is_mult(a,b) <-> is_mult(-a,b)

axiom is_mult_fact_r: 
 forall a,b:int. is_mult(a,a*b)

axiom is_mult_fact_l: 
 forall a,b:int. is_mult(a,b*a)

axiom is_mult_antisym: 
 forall a,b:int. 
    is_mult(a,b) -> is_mult(b,a) -> a=b or a=-b

axiom is_mult_trans: 
 forall a,b,c:int. 
    is_mult(a,b) -> is_mult(b,c) -> is_mult(a,c)

axiom is_mult_mod: 
 forall a,b:int. 
    b>0 -> is_mult(b,a) -> a%b = 0

axiom is_mult_le: 
 forall a,b:int. 
    0 <= a -> 0 < b -> is_mult(a,b) -> a <= b 

axiom is_mult_div_lt_pos: 
  forall a,b:int. 
    1 < a -> 0 < b -> is_mult(a,b) -> 0< b/a < b 

axiom is_mult_div_mod: 
  forall n,m,a:int. 0 < n -> 0 < m -> is_mult(n,m) -> a % m = (a%m)%n

axiom is_mod_mult_minus: 
  forall a,b,c:int. 0<b -> a%b =c -> is_mult(b, a-c)

axiom is_mod_minus : 
  forall a,b,c: int. 0 <= c <b -> is_mult(b,a-c) -> a%b=c

(**************************************************************)
 (** eq_modulo from Compcert Integer.v *)
  
logic eqmod: int,int,int -> prop

axiom eqmod_def: 
 forall m,a,b:int. 0<m -> eqmod(m,a,b) <-> exists k:int. a= k* m+b

axiom eqmod_refl: forall m,x:int. 0<m -> eqmod(m,x,x)
axiom eqmod_refl2: forall m,x,y:int. 0<m -> x=y -> eqmod(m,x,y)
axiom eqmod_sym: forall m,x,y:int. 0<m -> eqmod(m,x,y) -> eqmod(m,y,x)
axiom eqmod_small_eq:
 forall m,x,y:int. 
   0<m -> eqmod(m,x,y) -> 
   0<= x < m ->
   0<= y < m ->
   x=y
axiom eqmod_mod_eq: forall m,x,y:int. 0<m -> eqmod(m,x,y) -> x%m = y%m
axiom eqmod_mod: forall m,x:int. 0<m -> eqmod(m,x,x%m)
axiom eqmod_add: 
 forall m,a,b,c,d:int. 
  0<m ->eqmod(m,a,b) -> eqmod(m,c,d)->  eqmod(m,a+c,b+d)   
axiom eqmod_neg: forall m,x,y:int. 0<m -> eqmod(m,x,y) ->  eqmod(m,-x,-y)
axiom eqmod_sub: 
 forall m,a,b,c,d:int. 
 0<m -> eqmod(m,a,b) -> eqmod(m,c,d)-> eqmod(m,a-c,b-d)   
axiom eqmod_mult: 
 forall m,a,b,c,d:int. 
  0<m ->eqmod(m,a,b) -> eqmod(m,c,d)-> eqmod(m,a*c,b*d)

axiom eqmod_is_mult: 
 forall m,n,x,y:int. 
  0<n ->eqmod(n,x,y) -> is_mult(m,n) -> eqmod(m,x,y)  
(***************************************************************)
logic unsigned : int,int -> int 
logic signed : int,int -> int 

axiom unsigned_def: 
 forall max,i:int. 0 <= unsigned(max,i) < max

axiom signed_def_inf : 
 forall max,i: int.
  2 * unsigned(max,i) < max -> signed(max,i) =unsigned(max,i)  

axiom signed_def_sup: 
  forall max,i: int.
  2 * unsigned(max,i) > max -> signed(max,i) = unsigned(max,i) - max  

axiom unsigned_in : 
 forall max,i:int. 0<= i < max -> unsigned(max,i) = i

axiom signed_in : 
 forall max,i:int. -max <= 2*i < max -> signed(max,i) = i 
(*
axiom unsigned_in_bis : 
 forall max,i,n:int. 0<= i < max -> unsigned(max,i+n*max) = i
*)

(****************************************************************)

axiom eqmod_unsigned: 
 forall m,x:int.  0<m -> eqmod(m,x,unsigned(m,x))

axiom eqmod_unsigned_left: 
 forall m,a,b:int. 
 0 < m -> eqmod(m,a,b) -> eqmod(m,unsigned(m,a),b)
axiom eqmod_unsigned_right: 
 forall m,a,b:int. 
 0 < m -> eqmod(m,a,b) -> eqmod(m,a,unsigned(m,b))
axiom eqmod_signed_unsigned: 
 forall m,x:int. 0<m -> eqmod(m,signed(m,x),unsigned(m,x)) 
(*****************************************************************)

logic modu8 : int -> int 
logic mods8 : int -> int 
logic modu16: int -> int 
logic mods16: int -> int 
logic modu32: int -> int 
logic mods32: int -> int 
logic modu64: int -> int 
logic mods64: int -> int 


axiom modu8_def :
 forall x:int. modu8(x) = unsigned(256,x)
axiom mods8_def : 
 forall x:int. mods8(x) = signed(256,x)

axiom modu16_def :
 forall x:int. modu16(x) = unsigned(65536,x)
axiom mods16_def : 
 forall x:int. mods16(x) = signed(65536,x)

axiom modu32_def :
 forall x:int. modu32(x) = unsigned(4294967296,x)
axiom mods32_def : 
 forall x:int. mods32(x) = signed(4294967296,x)