← Back to branch summary

~ubuntu-branches/debian/sid/frama-c/sid

« back to all changes in this revision

Viewing changes to share/fluctuat.h

  • Committer: Bazaar Package Importer
  • Author(s): Mehdi Dogguy
  • Date: 2009-06-03 08:19:25 UTC
  • Revision ID: james.westby@ubuntu.com-20090603081925-kihvxvt0wy3zc4ar
Tags: upstream-20081201.dfsg
Import upstream version 20081201.dfsg

Show diffs side-by-side

added added

removed removed

Lines of Context:
share/fluctuat.h
 
1
/**************************************************************************/
 
2
/*                                                                        */
 
3
/*  This file is part of Frama-C.                                         */
 
4
/*                                                                        */
 
5
/*  Copyright (C) 2007-2008                                               */
 
6
/*    CEA (Commissariat � l'�nergie Atomique)                             */
 
7
/*                                                                        */
 
8
/*  you can redistribute it and/or modify it under the terms of the GNU   */
 
9
/*  Lesser General Public License as published by the Free Software       */
 
10
/*  Foundation, version 2.1.                                              */
 
11
/*                                                                        */
 
12
/*  It is distributed in the hope that it will be useful,                 */
 
13
/*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
 
14
/*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         */
 
15
/*  GNU Lesser General Public License for more details.                   */
 
16
/*                                                                        */
 
17
/*  See the GNU Lesser General Public License version 2.1                 */
 
18
/*  for more details (enclosed in the file licenses/LGPLv2.1).            */
 
19
/*                                                                        */
 
20
/**************************************************************************/
 
21
 
 
22
// Fluctuat emulation layer to be used with -imacros fluctuat.h
 
23
 
 
24
#define __BUILTIN_DAED_LIMIT(lv,min,max) lv=Frama_C_float_interval(min,max)
 
25
#define __BUILTIN_DAED_DBETWEEN(min,max) Frama_C_float_interval(min,max)
 
26
#define __BUILTIN_DAED_IBETWEEN(min,max) Frama_C_interval(min,max)
 
27