(*
 *	Copyright (c) 2002 by Laboratoire Spécification et Vérification (LSV),
 *	CNRS UMR 8643 & ENS Cachan.
 *	Written by Jean Goubault-Larrecq.  Not derived from licensed software.
 *
 *	Permission is granted to anyone to use this software for any
 *	purpose on any computer system, and to redistribute it freely,
 *	subject to the following restrictions:
 *
 *	1. Neither the author nor its employer is responsible for the consequences of use of
 *		this software, no matter how awful, even if they arise
 *		from defects in it.
 *
 *	2. The origin of this software must not be misrepresented, either
 *		by explicit claim or by omission.
 *
 *	3. Altered versions must be plainly marked as such, and must not
 *		be misrepresented as being the original software.
 *
 *	4. This software is restricted to non-commercial use only.  Commercial
 *		use is subject to a specific license, obtainable from LSV.
 *)

open Cparse
open Control
open Glue

val ae_bnot : string -> loc_ppoint option -> abs_env -> var -> abs_value -> q_ctype -> abs_effect
	(* ae_bnot func ctx ae x v qtyp
	effectue x := ~v, la negation bit a bit de v, dans l'environnement ae;
	le nom de la fonction courante est func et son
	contexte d'appel est ctx.
	Voir glue.mli pour la definition de abs_effect (l'effet d'une instruction). *)
val ae_minus : string -> loc_ppoint option -> abs_env -> var -> abs_value -> q_ctype -> abs_effect
	(* ae_minus func ctx ae x v qtyp
	effectue x := -v, l'oppose de v, dans l'environnement ae;
	le nom de la fonction courante est func et son
	contexte d'appel est ctx. *)
val ae_mul : string -> loc_ppoint option -> abs_env -> var -> abs_value -> abs_value -> q_ctype -> abs_effect
	(* ae_mul func ctx ae x v1 v2 qtyp
	effectue x := v1*v2 dans l'environnement ae;
	le nom de la fonction courante est func et son
	contexte d'appel est ctx. *)
val ae_div : string -> loc_ppoint option -> abs_env -> var -> abs_value -> abs_value -> q_ctype -> abs_effect
	(* ae_div func ctx ae x v1 v2 qtyp
	effectue x := v1/v2 dans l'environnement ae (division entiere si qtyp est un type
	entier, division flottante si qtyp est un type flottant);
	le nom de la fonction courante est func et son
	contexte d'appel est ctx. *)
val ae_mod : string -> loc_ppoint option -> abs_env -> var -> abs_value -> abs_value -> q_ctype -> abs_effect
	(* ae_mod func ctx ae x v1 v2 qtyp
	effectue x := v1%v2 dans l'environnement ae (division entiere si qtyp est un type
	entier; ca ne peut pas etre un type flottant);
	le nom de la fonction courante est func et son
	contexte d'appel est ctx. *)
val ae_add : string -> loc_ppoint option -> abs_env -> var -> abs_value -> abs_value -> q_ctype -> abs_effect
	(* ae_add func ctx ae x v1 v2 qtyp
	effectue x := v1+v2 dans l'environnement ae;
	le nom de la fonction courante est func et son
	contexte d'appel est ctx. *)

val ae_left : string -> loc_ppoint option -> abs_env -> var -> abs_value -> abs_value -> q_ctype -> abs_effect
	(* ae_add func ctx ae x v1 v2 qtyp
	effectue x := v1<<v2 dans l'environnement ae;
	le nom de la fonction courante est func et son
	contexte d'appel est ctx. *)
val ae_right : string -> loc_ppoint option -> abs_env -> var -> abs_value -> abs_value -> q_ctype -> abs_effect
	(* ae_add func ctx ae x v1 v2 qtyp
	effectue x := v1>>v2 dans l'environnement ae;
	le nom de la fonction courante est func et son
	contexte d'appel est ctx. *)
val ae_and : string -> loc_ppoint option -> abs_env -> var -> abs_value -> abs_value -> q_ctype -> abs_effect
	(* ae_and func ctx ae x v1 v2 qtyp
	effectue x := v1 & v2, le et bit a bit, dans l'environnement ae;
	le nom de la fonction courante est func et son
	contexte d'appel est ctx. *)
val ae_xor : string -> loc_ppoint option -> abs_env -> var -> abs_value -> abs_value -> q_ctype -> abs_effect
	(* ae_and func ctx ae x v1 v2 qtyp
	effectue x := v1 ^ v2, le ou exclusif bit a bit, dans l'environnement ae;
	le nom de la fonction courante est func et son
	contexte d'appel est ctx. *)
val ae_or : string -> loc_ppoint option -> abs_env -> var -> abs_value -> abs_value -> q_ctype -> abs_effect
	(* ae_or func ctx ae x v1 v2 qtyp
	effectue x := v1 | v2, le ou bit a bit, dans l'environnement ae;
	le nom de la fonction courante est func et son
	contexte d'appel est ctx. *)

val ae_eq : string -> loc_ppoint option -> abs_env -> var -> abs_value -> abs_value -> q_ctype -> abs_effect
	(* ae_eq func ctx ae x v1 v2 qtyp
	effectue x := (v1 = v2), le test d'egalite, dans l'environnement ae;
	le nom de la fonction courante est func et son
	contexte d'appel est ctx. *)
val ae_le : string -> loc_ppoint option -> abs_env -> var -> abs_value -> abs_value -> q_ctype -> abs_effect
	(* ae_eq func ctx ae x v1 v2 qtyp
	effectue x := (v1 <= v2) dans l'environnement ae;
	le nom de la fonction courante est func et son
	contexte d'appel est ctx. *)
val ae_lt : string -> loc_ppoint option -> abs_env -> var -> abs_value -> abs_value -> q_ctype -> abs_effect
	(* ae_eq func ctx ae x v1 v2 qtyp
	effectue x := (v1 < v2) dans l'environnement ae;
	le nom de la fonction courante est func et son
	contexte d'appel est ctx. *)
val ae_test_true : abs_value -> bool
	(* ae_test_true v est vrai si et seulement s'il est possible
	que v s'evalue en un booleen vrai (entier non nul). *)
val ae_test_false : abs_value -> bool
	(* ae_test_false v est vrai si et seulement s'il est possible
	que v s'evalue en un booleen faux (entier nul). *)